diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 8e4959e959..f7d355fe3b 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -1468,6 +1468,8 @@ def Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂
 
 @[simp] theorem Prod.map_apply (f : α → β) (g : γ → δ) (x) (y) :
     Prod.map f g (x, y) = (f x, g y) := rfl
+
+-- We add `@[grind =]` to these in `Init.Data.Prod`.
 @[simp] theorem Prod.map_fst (f : α → β) (g : γ → δ) (x) : (Prod.map f g x).1 = f x.1 := rfl
 @[simp] theorem Prod.map_snd (f : α → β) (g : γ → δ) (x) : (Prod.map f g x).2 = g x.2 := rfl
 
diff --git a/src/Init/Data/Prod.lean b/src/Init/Data/Prod.lean
index 6a48bb664b..8baac8d8a8 100644
--- a/src/Init/Data/Prod.lean
+++ b/src/Init/Data/Prod.lean
@@ -12,6 +12,8 @@ public section
 
 namespace Prod
 
+attribute [grind =] Prod.map_fst Prod.map_snd
+
 instance [BEq α] [BEq β] [ReflBEq α] [ReflBEq β] : ReflBEq (α × β) where
   rfl {a} := by cases a; simp [BEq.beq]