Feat: add Sigma.map_mk (#1905)

`simp [Sigma.map_mk]` has the same effect in Lean 4 as `simp [sigma.map]` has in Lean 3. OTOH, `simp [Sigma.map]` unfolds non-applied `Sigma.map`s too.
leanprover-community · Jan 31, 2023 · 4809cc9 · 4809cc9
1 parent ebfc908
commit 4809cc9
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/Mathlib/Data/Sigma/Basic.lean b/Mathlib/Data/Sigma/Basic.lean
@@ -102,6 +102,8 @@ def map (f₁ : α₁ → α₂) (f₂ : ∀ a, β₁ a → β₂ (f₁ a)) (x :
   ⟨f₁ x.1, f₂ x.1 x.2⟩
 #align sigma.map Sigma.map
 
+lemma map_mk (f₁ : α₁ → α₂) (f₂ : ∀ a, β₁ a → β₂ (f₁ a)) (x : α₁) (y : β₁ x) :
+    map f₁ f₂ ⟨x, y⟩ = ⟨f₁ x, f₂ x y⟩ := rfl
 end Sigma
 
 theorem sigma_mk_injective {i : α} : Function.Injective (@Sigma.mk α β i)