chore: fix explicitness of Prod.map lemmas (#4533)

leanprover · Jun 22, 2024 · d7da45c · d7da45c
1 parent 24d51b9
commit d7da45c
Showing 1 changed file with 4 additions and 3 deletions.
diff --git a/src/Init/Core.lean b/src/Init/Core.lean
@@ -1191,9 +1191,10 @@ def Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂
     (f : α₁ → α₂) (g : β₁ → β₂) : α₁ × β₁ → α₂ × β₂
   | (a, b) => (f a, g b)
 
-@[simp] theorem Prod.map_apply : Prod.map f g (x, y) = (f x, g y) := rfl
-@[simp] theorem Prod.map_fst : (Prod.map f g x).1 = f x.1 := rfl
-@[simp] theorem Prod.map_snd : (Prod.map f g x).2 = g x.2 := rfl
+@[simp] theorem Prod.map_apply (f : α → β) (g : γ → δ) (x) (y) :
+    Prod.map f g (x, y) = (f x, g y) := rfl
+@[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
 
 /-! # Dependent products -/