chore(algebra/group/hom): Add mk_coe lemmas (#5812)

These are the counterparts to the `coe_mk` lemmas.

Author: eric-wieser

src/algebra/algebra/basic.lean

@@ -436,6 +436,9 @@ coe_fn_inj $ funext H
 theorem ext_iff {φ₁ φ₂ : A →ₐ[R] B} : φ₁ = φ₂ ↔ ∀ x, φ₁ x = φ₂ x :=
 ⟨alg_hom.congr_fun, ext⟩
 
+@[simp] theorem mk_coe {f : A →ₐ[R] B} (h₁ h₂ h₃ h₄ h₅) :
+  (⟨f, h₁, h₂, h₃, h₄, h₅⟩ : A →ₐ[R] B) = f := ext $ λ _, rfl
+
 @[simp]
 theorem commutes (r : R) : φ (algebra_map R A r) = algebra_map R B r := φ.commutes' r
 

src/algebra/group/hom.lean

@@ -276,6 +276,23 @@ lemma monoid_with_zero_hom.ext_iff [monoid_with_zero M] [monoid_with_zero N]
   {f g : monoid_with_zero_hom M N} : f = g ↔ ∀ x, f x = g x :=
 ⟨λ h x, h ▸ rfl, λ h, monoid_with_zero_hom.ext h⟩
 
+@[simp, to_additive]
+lemma one_hom.mk_coe [has_one M] [has_one N]
+  (f : one_hom M N) (h1) : one_hom.mk f h1 = f :=
+one_hom.ext $ λ _, rfl
+@[simp, to_additive]
+lemma mul_hom.mk_coe [has_mul M] [has_mul N]
+  (f : mul_hom M N) (hmul) : mul_hom.mk f hmul = f :=
+mul_hom.ext $ λ _, rfl
+@[simp, to_additive]
+lemma monoid_hom.mk_coe [monoid M] [monoid N]
+  (f : M →* N) (h1 hmul) : monoid_hom.mk f h1 hmul = f :=
+monoid_hom.ext $ λ _, rfl
+@[simp]
+lemma monoid_with_zero_hom.mk_coe [monoid_with_zero M] [monoid_with_zero N]
+  (f : monoid_with_zero_hom M N) (h0 h1 hmul) : monoid_with_zero_hom.mk f h0 h1 hmul = f :=
+monoid_with_zero_hom.ext $ λ _, rfl
+
 end coes
 
 @[simp, to_additive]

src/algebra/module/linear_map.lean

@@ -117,6 +117,9 @@ protected lemma congr_fun (h : f = g) (x : M) : f x = g x := h ▸ rfl
 theorem ext_iff : f = g ↔ ∀ x, f x = g x :=
 ⟨by { rintro rfl x, refl }, ext⟩
 
+@[simp] lemma mk_coe (f : M →ₗ[R] M₂) (h₁ h₂) :
+  (linear_map.mk f h₁ h₂ : M →ₗ[R] M₂) = f := ext $ λ _, rfl
+
 variables (f g)
 
 @[simp] lemma map_add (x y : M) : f (x + y) = f x + f y := f.map_add' x y

src/algebra/ring/basic.lean

@@ -285,6 +285,9 @@ coe_inj (funext h)
 theorem ext_iff {f g : α →+* β} : f = g ↔ ∀ x, f x = g x :=
 ⟨λ h x, h ▸ rfl, λ h, ext h⟩
 
+@[simp] lemma mk_coe (f : α →+* β) (h₁ h₂ h₃ h₄) : ring_hom.mk f h₁ h₂ h₃ h₄ = f :=
+ext $ λ _, rfl
+
 theorem coe_add_monoid_hom_injective : function.injective (coe : (α →+* β) → (α →+ β)) :=
 λ f g h, ext (λ x, add_monoid_hom.congr_fun h x)