refactor(data/prod): add map_fst, map_snd

Author: johoelzl

data/prod.lean

@@ -7,8 +7,7 @@ Extends theory on products
 -/
 import tactic.ext
 
-universes u v
-variables {α : Type u} {β : Type v}
+variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
 
 @[simp] theorem prod.forall {p : α × β → Prop} : (∀ x, p x) ↔ (∀ a b, p (a, b)) :=
 ⟨assume h a b, h (a, b), assume h ⟨a, b⟩, h a b⟩
@@ -20,6 +19,12 @@ namespace prod
 
 attribute [simp] prod.map
 
+@[simp] lemma map_fst (f : α → γ) (g : β → δ) : ∀(p : α × β), (map f g p).1 = f (p.1)
+| ⟨a, b⟩ := rfl
+
+@[simp] lemma map_snd (f : α → γ) (g : β → δ) : ∀(p : α × β), (map f g p).2 = g (p.2)
+| ⟨a, b⟩ := rfl
+
 @[simp] theorem mk.inj_iff {a₁ a₂ : α} {b₁ b₂ : β} : (a₁, b₁) = (a₂, b₂) ↔ (a₁ = a₂ ∧ b₁ = b₂) :=
 ⟨prod.mk.inj, by cc⟩