diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index e41df385b800..38c6f0a37075 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -1192,6 +1192,8 @@ def Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂
   | (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
 
 /-! # Dependent products -/