From 28a3cf9a6cc394316b79bbbdd868e605ee9d8784 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Thu, 6 Nov 2025 07:52:28 +1100
Subject: [PATCH] chore: grind attributes for `Prod` (#11085)

---
 src/Init/Core.lean      | 2 ++
 src/Init/Data/Prod.lean | 2 ++
 2 files changed, 4 insertions(+)

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]