chore: get rid of generic hom coercions

Author: YaelDillies

Mathlib/Algebra/Group/Equiv/Basic.lean

@@ -35,9 +35,18 @@ end EmbeddingLike
 
 variable [EquivLike F α β]
 
+/-- Turn an element of a type `F` satisfying `MulEquivClass F α β` into an actual
+`MulEquiv`. This is declared as the default coercion from `F` to `α ≃* β`. -/
+@[to_additive (attr := simps!)
+"Turn an element of a type `F` satisfying `AddEquivClass F α β` into an actual
+`AddEquiv`. This is declared as the default coercion from `F` to `α ≃+ β`."]
+def MulEquiv.ofClass [Mul α] [Mul β] [MulEquivClass F α β] (f : F) : α ≃* β where
+  __ : α ≃ β := .ofClass f
+  __ : α →ₙ* β := .ofClass f
+
 @[to_additive]
-theorem MulEquivClass.toMulEquiv_injective [Mul α] [Mul β] [MulEquivClass F α β] :
-    Function.Injective ((↑) : F → α ≃* β) :=
+theorem MulEquiv.ofClass_injective [Mul α] [Mul β] [MulEquivClass F α β] :
+    Function.Injective (.ofClass : F → α ≃* β) :=
   fun _ _ e ↦ DFunLike.ext _ _ fun a ↦ congr_arg (fun e : α ≃* β ↦ e.toFun a) e
 
 @[to_additive] theorem MulEquivClass.isDedekindFiniteMonoid_iff [MulOne α] [MulOne β]

Mathlib/Algebra/Group/Equiv/Defs.lean

@@ -143,7 +143,7 @@ variable [EquivLike F α β]
 /-- Turn an element of a type `F` satisfying `AddEquivClass F α β` into an actual
 `AddEquiv`. This is declared as the default coercion from `F` to `α ≃+ β`. -/]
 def MulEquivClass.toMulEquiv [Mul α] [Mul β] [MulEquivClass F α β] (f : F) : α ≃* β :=
-  { (f : α ≃ β), (f : α →ₙ* β) with }
+  { (.ofClass f : α ≃ β), (.ofClass f : α →ₙ* β) with }
 
 /-- Any type satisfying `MulEquivClass` can be cast into `MulEquiv` via
 `MulEquivClass.toMulEquiv`. -/
@@ -201,20 +201,20 @@ theorem mk_coe (e : M ≃* N) (e' h₁ h₂ h₃) : (⟨⟨e, e', h₁, h₂⟩,
   ext fun _ => rfl
 
 @[to_additive (attr := simp)]
-theorem toEquiv_eq_coe (f : M ≃* N) : f.toEquiv = f :=
+theorem toEquiv_eq_ofClass (f : M ≃* N) : f.toEquiv = .ofClass f :=
   rfl
 
 /-- The `simp`-normal form to turn something into a `MulHom` is via `MulHomClass.toMulHom`. -/
 @[to_additive (attr := simp)]
-theorem toMulHom_eq_coe (f : M ≃* N) : f.toMulHom = ↑f :=
+theorem toMulHom_eq_ofClass (f : M ≃* N) : f.toMulHom = .ofClass f :=
   rfl
 
 @[to_additive]
 theorem toFun_eq_coe (f : M ≃* N) : f.toFun = f := rfl
 
 /-- `simp`-normal form of `toFun_eq_coe`. -/
 @[to_additive (attr := simp)]
-theorem coe_toEquiv (f : M ≃* N) : ⇑(f : M ≃ N) = f := rfl
+theorem coe_toEquiv (f : M ≃* N) : ⇑(.ofClass f : M ≃ N) = f := rfl
 
 @[to_additive (attr := simp)]
 theorem coe_toMulHom {f : M ≃* N} : (f.toMulHom : M → N) = f := rfl
@@ -292,13 +292,13 @@ theorem invFun_eq_symm {f : M ≃* N} : f.invFun = f.symm := rfl
 
 /-- `simp`-normal form of `invFun_eq_symm`. -/
 @[to_additive (attr := simp)]
-theorem coe_toEquiv_symm (f : M ≃* N) : ((f : M ≃ N).symm : N → M) = f.symm := rfl
+theorem symm_ofClass (f : M ≃* N) : ((.ofClass f : M ≃ N).symm : N → M) = f.symm := rfl
 
 @[to_additive (attr := simp)]
 theorem equivLike_inv_eq_symm (f : M ≃* N) : EquivLike.inv f = f.symm := rfl
 
 @[to_additive (attr := simp)]
-theorem toEquiv_symm (f : M ≃* N) : (f.symm : N ≃ M) = (f : M ≃ N).symm := rfl
+theorem ofClass_symm (f : M ≃* N) : (.ofClass f.symm : N ≃ M) = (.ofClass f : M ≃ N).symm := rfl
 
 @[to_additive (attr := simp)]
 theorem symm_symm (f : M ≃* N) : f.symm.symm = f := rfl
@@ -458,29 +458,6 @@ protected def cast {ι : Type*} {M : ι → Type*} [∀ i, Mul (M i)] {i j : ι}
 section MulOneClass
 variable [MulOneClass M] [MulOneClass N] [MulOneClass P]
 
-@[to_additive (attr := simp)]
-theorem coe_monoidHom_refl : (refl M : M →* M) = MonoidHom.id M := rfl
-
-@[to_additive (attr := simp)]
-lemma coe_monoidHom_trans (e₁ : M ≃* N) (e₂ : N ≃* P) :
-    (e₁.trans e₂ : M →* P) = (e₂ : N →* P).comp ↑e₁ := rfl
-
-@[to_additive (attr := simp)]
-lemma coe_monoidHom_comp_coe_monoidHom_symm (e : M ≃* N) :
-    (e : M →* N).comp e.symm = MonoidHom.id _ := by ext; simp
-
-@[to_additive (attr := simp)]
-lemma coe_monoidHom_symm_comp_coe_monoidHom (e : M ≃* N) :
-    (e.symm : N →* M).comp e = MonoidHom.id _ := by ext; simp
-
-@[to_additive]
-lemma comp_left_injective (e : M ≃* N) : Injective fun f : N →* P ↦ f.comp (e : M →* N) :=
-  LeftInverse.injective (g := fun f ↦ f.comp e.symm) fun f ↦ by simp [MonoidHom.comp_assoc]
-
-@[to_additive]
-lemma comp_right_injective (e : M ≃* N) : Injective fun f : P →* M ↦ (e : M →* N).comp f :=
-  LeftInverse.injective (g := (e.symm : N →* M).comp) fun f ↦ by simp [← MonoidHom.comp_assoc]
-
 /-- A multiplicative isomorphism of monoids sends `1` to `1` (and is hence a monoid isomorphism). -/
 @[to_additive
   /-- An additive isomorphism of additive monoids sends `0` to `0`
@@ -514,17 +491,41 @@ as a multiplication-preserving function.
 def toMonoidHom (h : M ≃* N) : M →* N :=
   { h with map_one' := h.map_one }
 
+instance : Coe (M ≃* N) (M →* N) := ⟨toMonoidHom⟩
+
 @[to_additive (attr := simp)]
 theorem coe_toMonoidHom (e : M ≃* N) : ⇑e.toMonoidHom = e := rfl
 
-@[to_additive (attr := simp)]
-theorem toMonoidHom_eq_coe (f : M ≃* N) : f.toMonoidHom = (f : M →* N) :=
-  rfl
+@[to_additive (attr := deprecated "No replacement" (since := "2025-04-14"))]
+theorem toMonoidHom_eq_ofClass (f : M ≃* N) : f.toMonoidHom = (.ofClass f : M →* N) := rfl
 
 @[to_additive]
 theorem toMonoidHom_injective : Injective (toMonoidHom : M ≃* N → M →* N) :=
   Injective.of_comp (f := DFunLike.coe) DFunLike.coe_injective
 
+@[to_additive (attr := simp)]
+theorem refl_toMonoidHom : (refl M).toMonoidHom = .id M := rfl
+
+@[to_additive (attr := simp)]
+lemma trans_toMonoidHom (e₁ : M ≃* N) (e₂ : N ≃* P) :
+    (e₁.trans e₂).toMonoidHom = e₂.toMonoidHom.comp e₁.toMonoidHom := rfl
+
+@[to_additive (attr := simp)]
+lemma toMonoidHom_comp_toMonoidHom_symm (e : M ≃* N) : e.toMonoidHom.comp e.symm = .id _ := by
+  ext; simp
+
+@[to_additive (attr := simp)]
+lemma toMonoidHom_symm_comp_toMonoidHom (e : M ≃* N) : e.symm.toMonoidHom.comp e = .id _ := by
+  ext; simp
+
+@[to_additive]
+lemma comp_left_injective (e : M ≃* N) : Injective fun f : N →* P ↦ f.comp (e : M →* N) :=
+  LeftInverse.injective (g := fun f ↦ f.comp e.symm) fun f ↦ by simp [MonoidHom.comp_assoc]
+
+@[to_additive]
+lemma comp_right_injective (e : M ≃* N) : Injective fun f : P →* M ↦ (e : M →* N).comp f :=
+  LeftInverse.injective (g := (e.symm : N →* M).comp) fun f ↦ by simp [← MonoidHom.comp_assoc]
+
 end MulOneClass
 
 /-!

Mathlib/Algebra/Group/Hom/Defs.lean

@@ -10,6 +10,7 @@ public import Mathlib.Algebra.Group.Defs
 public import Mathlib.Algebra.Notation.Pi.Defs
 public import Mathlib.Data.FunLike.Basic
 public import Mathlib.Logic.Function.Iterate
+public import Mathlib.Tactic.Spread
 
 /-!
 # Monoid and group homomorphisms
@@ -257,24 +258,20 @@ theorem map_ne_one_iff {R S F : Type*} [One R] [One S] [FunLike F R S] [OneHomCl
 theorem ne_one_of_map {R S F : Type*} [One R] [One S] [FunLike F R S] [OneHomClass F R S]
     {f : F} {x : R} (hx : f x ≠ 1) : x ≠ 1 := ne_of_apply_ne f <| (by rwa [(map_one f)])
 
+initialize_simps_projections ZeroHom (toFun → apply)
+initialize_simps_projections OneHom (toFun → apply)
+
 /-- Turn an element of a type `F` satisfying `OneHomClass F M N` into an actual
 `OneHom`. This is declared as the default coercion from `F` to `OneHom M N`. -/
-@[to_additive (attr := coe)
+@[to_additive (attr := simps)
 /-- Turn an element of a type `F` satisfying `ZeroHomClass F M N` into an actual
 `ZeroHom`. This is declared as the default coercion from `F` to `ZeroHom M N`. -/]
-def OneHomClass.toOneHom [OneHomClass F M N] (f : F) : OneHom M N where
+def OneHom.ofClass [OneHomClass F M N] (f : F) : OneHom M N where
   toFun := f
   map_one' := map_one f
 
-/-- Any type satisfying `OneHomClass` can be cast into `OneHom` via `OneHomClass.toOneHom`. -/
-@[to_additive /-- Any type satisfying `ZeroHomClass` can be cast into `ZeroHom` via
-`ZeroHomClass.toZeroHom`. -/]
-instance [OneHomClass F M N] : CoeTC F (OneHom M N) :=
-  ⟨OneHomClass.toOneHom⟩
-
 @[to_additive (attr := simp)]
-theorem OneHom.coe_coe [OneHomClass F M N] (f : F) :
-    ((f : OneHom M N) : M → N) = f := rfl
+lemma OneHom.coe_ofClass [OneHomClass F M N] (f : F) : ⇑(ofClass f) = f := rfl
 
 end One
 
@@ -330,23 +327,20 @@ theorem map_mul [MulHomClass F M N] (f : F) (x y : M) : f (x * y) = f x * f y :=
 lemma map_comp_mul [MulHomClass F M N] (f : F) (g h : ι → M) : f ∘ (g * h) = f ∘ g * f ∘ h := by
   ext; simp
 
+initialize_simps_projections AddHom (toFun → apply)
+initialize_simps_projections MulHom (toFun → apply)
+
 /-- Turn an element of a type `F` satisfying `MulHomClass F M N` into an actual
 `MulHom`. This is declared as the default coercion from `F` to `M →ₙ* N`. -/
-@[to_additive (attr := coe)
+@[to_additive (attr := simps)
 /-- Turn an element of a type `F` satisfying `AddHomClass F M N` into an actual
 `AddHom`. This is declared as the default coercion from `F` to `M →ₙ+ N`. -/]
-def MulHomClass.toMulHom [MulHomClass F M N] (f : F) : M →ₙ* N where
+def MulHom.ofClass [MulHomClass F M N] (f : F) : M →ₙ* N where
   toFun := f
   map_mul' := map_mul f
 
-/-- Any type satisfying `MulHomClass` can be cast into `MulHom` via `MulHomClass.toMulHom`. -/
-@[to_additive /-- Any type satisfying `AddHomClass` can be cast into `AddHom` via
-`AddHomClass.toAddHom`. -/]
-instance [MulHomClass F M N] : CoeTC F (M →ₙ* N) :=
-  ⟨MulHomClass.toMulHom⟩
-
 @[to_additive (attr := simp)]
-theorem MulHom.coe_coe [MulHomClass F M N] (f : F) : ((f : MulHom M N) : M → N) = f := rfl
+lemma MulHom.coe_ofClass [MulHomClass F M N] (f : F) : (ofClass f : M → N) = f := rfl
 
 end Mul
 
@@ -398,23 +392,13 @@ instance MonoidHom.instMonoidHomClass : MonoidHomClass (M →* N) M N where
 
 variable [FunLike F M N]
 
-/-- Turn an element of a type `F` satisfying `MonoidHomClass F M N` into an actual
-`MonoidHom`. This is declared as the default coercion from `F` to `M →* N`. -/
+/-- Turn an element of a type `F` satisfying `MonoidHomClass F M N` into an actual `MonoidHom`. -/
 @[to_additive (attr := coe)
 /-- Turn an element of a type `F` satisfying `AddMonoidHomClass F M N` into an
-actual `MonoidHom`. This is declared as the default coercion from `F` to `M →+ N`. -/]
-def MonoidHomClass.toMonoidHom [MonoidHomClass F M N] (f : F) : M →* N :=
-  { (f : M →ₙ* N), (f : OneHom M N) with }
-
-/-- Any type satisfying `MonoidHomClass` can be cast into `MonoidHom` via
-`MonoidHomClass.toMonoidHom`. -/
-@[to_additive /-- Any type satisfying `AddMonoidHomClass` can be cast into `AddMonoidHom` via
-`AddMonoidHomClass.toAddMonoidHom`. -/]
-instance [MonoidHomClass F M N] : CoeTC F (M →* N) :=
-  ⟨MonoidHomClass.toMonoidHom⟩
-
-@[to_additive (attr := simp)]
-theorem MonoidHom.coe_coe [MonoidHomClass F M N] (f : F) : ((f : M →* N) : M → N) = f := rfl
+actual `AddMonoidHom`. -/]
+def MonoidHom.ofClass [MonoidHomClass F M N] (f : F) : M →* N where
+  __ : M →ₙ* N := .ofClass f
+  __ : OneHom M N := .ofClass f
 
 @[to_additive]
 theorem map_mul_eq_one [MonoidHomClass F M N] (f : F) {a b : M} (h : a * b = 1) :
@@ -532,11 +516,7 @@ instance MonoidHom.coeToMulHom [MulOne M] [MulOne N] : Coe (M →* N) (M →ₙ*
   ⟨MonoidHom.toMulHom⟩
 
 -- these must come after the coe_toFun definitions
-initialize_simps_projections ZeroHom (toFun → apply)
-initialize_simps_projections AddHom (toFun → apply)
 initialize_simps_projections AddMonoidHom (toFun → apply)
-initialize_simps_projections OneHom (toFun → apply)
-initialize_simps_projections MulHom (toFun → apply)
 initialize_simps_projections MonoidHom (toFun → apply)
 
 @[to_additive (attr := simp)]

Mathlib/Algebra/Group/Subgroup/Map.lean

@@ -191,10 +191,8 @@ theorem comap_equiv_eq_map_symm' (f : N ≃* G) (K : Subgroup G) :
 theorem map_symm_eq_iff_map_eq {H : Subgroup N} {e : G ≃* N} :
     H.map ↑e.symm = K ↔ K.map ↑e = H := by
   constructor <;> rintro rfl
-  · rw [map_map, ← MulEquiv.coe_monoidHom_trans, MulEquiv.symm_trans_self,
-      MulEquiv.coe_monoidHom_refl, map_id]
-  · rw [map_map, ← MulEquiv.coe_monoidHom_trans, MulEquiv.self_trans_symm,
-      MulEquiv.coe_monoidHom_refl, map_id]
+  · rw [map_map, MulEquiv.toMonoidHom_comp_toMonoidHom_symm, map_id]
+  · rw [map_map, MulEquiv.toMonoidHom_symm_comp_toMonoidHom, map_id]
 
 @[to_additive]
 theorem map_le_iff_le_comap {f : G →* N} {K : Subgroup G} {H : Subgroup N} :

Mathlib/Algebra/Group/Units/Hom.lean

@@ -127,7 +127,7 @@ theorem val_zpow_eq_zpow_val : ∀ (u : αˣ) (n : ℤ), ((u ^ n : αˣ) : α) =
 @[to_additive (attr := simp)]
 theorem _root_.map_units_inv {F : Type*} [FunLike F M α] [MonoidHomClass F M α]
     (f : F) (u : Units M) :
-    f ↑u⁻¹ = (f u)⁻¹ := ((f : M →* α).comp (Units.coeHom M)).map_inv u
+    f ↑u⁻¹ = (f u)⁻¹ := ((.ofClass f : M →* α).comp (Units.coeHom M)).map_inv u
 
 end DivisionMonoid
 
@@ -203,7 +203,7 @@ variable [Monoid M] [Monoid N]
 
 @[to_additive]
 theorem map [MonoidHomClass F M N] (f : F) {x : M} (h : IsUnit x) : IsUnit (f x) := by
-  rcases h with ⟨y, rfl⟩; exact (Units.map (f : M →* N) y).isUnit
+  obtain ⟨y, rfl⟩ := h; exact (y.map <| .ofClass f).isUnit
 
 @[to_additive]
 theorem of_leftInverse [MonoidHomClass G N M] {f : F} {x : M} (g : G)
@@ -276,10 +276,12 @@ theorem MonoidHom.isLocalHom_comp (g : S →* T) (f : R →* S) [IsLocalHom g]
 
 -- see note [lower instance priority]
 @[instance 100]
-theorem isLocalHom_toMonoidHom (f : F) [IsLocalHom f] :
-    IsLocalHom (f : R →* S) :=
+theorem isLocalHom_monoidHomOfClass (f : F) [IsLocalHom f] : IsLocalHom (.ofClass f : R →* S) :=
   ⟨IsLocalHom.map_nonunit (f := f)⟩
 
+@[deprecated (since := "2024-10-10")]
+alias isLocalRingHom_toMonoidHom := isLocalHom_monoidHomOfClass
+
 theorem MonoidHom.isLocalHom_of_comp (f : R →* S) (g : S →* T) [IsLocalHom (g.comp f)] :
     IsLocalHom f :=
   ⟨fun _ ha => (isUnit_map_iff (g.comp f) _).mp (ha.map g)⟩

Mathlib/Algebra/GroupWithZero/Hom.lean

@@ -80,7 +80,7 @@ infixr:25 " →*₀ " => MonoidWithZeroHom
 `MonoidWithZeroHom`. This is declared as the default coercion from `F` to `α →*₀ β`. -/
 @[coe]
 def MonoidWithZeroHomClass.toMonoidWithZeroHom [FunLike F α β] [MonoidWithZeroHomClass F α β]
-    (f : F) : α →*₀ β := { (f : α →* β), (f : ZeroHom α β) with }
+    (f : F) : α →*₀ β := { (.ofClass f : α →* β), (.ofClass f : ZeroHom α β) with }
 
 /-- Any type satisfying `MonoidWithZeroHomClass` can be cast into `MonoidWithZeroHom` via
 `MonoidWithZeroHomClass.toMonoidWithZeroHom`. -/

Mathlib/Algebra/Order/Hom/Monoid.lean

@@ -130,7 +130,7 @@ into an actual `OrderMonoidHom`. This is declared as the default coercion from `
   This is declared as the default coercion from `F` to `α →+o β`. -/]
 def OrderMonoidHomClass.toOrderMonoidHom [OrderHomClass F α β] [MonoidHomClass F α β] (f : F) :
     α →*o β :=
-  { (f : α →* β) with monotone' := OrderHomClass.monotone f }
+  { (.ofClass f : α →* β) with monotone' := OrderHomClass.monotone f }
 
 /-- Any type satisfying `OrderMonoidHomClass` can be cast into `OrderMonoidHom` via
   `OrderMonoidHomClass.toOrderMonoidHom`. -/
@@ -265,6 +265,8 @@ instance : MonoidHomClass (α →*o β) α β where
   map_mul f := f.map_mul'
   map_one f := f.map_one'
 
+@[to_additive] instance : Coe (α →*o β) (α →* β) := ⟨toMonoidHom⟩
+
 -- Other lemmas should be accessed through the `FunLike` API
 @[to_additive (attr := ext)]
 theorem ext (h : ∀ a, f a = g a) : f = g :=
@@ -442,10 +444,6 @@ section OrderedCommMonoid
 
 variable {_ : Preorder α} {_ : Preorder β} {_ : MulOneClass α} {_ : MulOneClass β}
 
-@[to_additive (attr := simp)]
-theorem toMonoidHom_eq_coe (f : α →*o β) : f.toMonoidHom = f :=
-  rfl
-
 @[to_additive (attr := simp)]
 theorem toOrderHom_eq_coe (f : α →*o β) : f.toOrderHom = f :=
   rfl
@@ -509,6 +507,8 @@ theorem coe_mk (f : α ≃* β) (h) : (OrderMonoidIso.mk f h : α → β) = f :=
 @[to_additive (attr := simp)]
 theorem mk_coe (f : α ≃*o β) (h) : OrderMonoidIso.mk (f : α ≃* β) h = f := rfl
 
+@[to_additive (attr := simp)] lemma coe_toMulEquiv (f : α ≃*o β) : ⇑f.toMulEquiv = f := rfl
+
 /-- Reinterpret an ordered monoid isomorphism as an order isomorphism. -/
 @[to_additive
 /-- Reinterpret an ordered additive monoid isomomorphism as an order isomomorphism. -/]
@@ -562,12 +562,12 @@ theorem coe_trans (f : α ≃*o β) (g : β ≃*o γ) : (f.trans g : α → γ)
 theorem trans_apply (f : α ≃*o β) (g : β ≃*o γ) (a : α) : (f.trans g) a = g (f a) :=
   rfl
 
-@[to_additive]
+@[to_additive (attr := simp, norm_cast)]
 theorem coe_trans_mulEquiv (f : α ≃*o β) (g : β ≃*o γ) :
     (f.trans g : α ≃* γ) = (f : α ≃* β).trans g :=
   rfl
 
-@[to_additive]
+@[to_additive (attr := simp, norm_cast)]
 theorem coe_trans_orderIso (f : α ≃*o β) (g : β ≃*o γ) :
     (f.trans g : α ≃o γ) = (f : α ≃o β).trans g :=
   rfl
@@ -624,15 +624,17 @@ initialize_simps_projections OrderMonoidIso (toFun → apply, invFun → symm_ap
 @[to_additive]
 theorem invFun_eq_symm {f : α ≃*o β} : f.invFun = f.symm := rfl
 
-/-- `simp`-normal form of `invFun_eq_symm`. -/
 @[to_additive (attr := simp)]
-theorem coe_toEquiv_symm (f : α ≃*o β) : ((f : α ≃ β).symm : β → α) = f.symm := rfl
+theorem symm_toEquiv (f : α ≃*o β) : f.toEquiv.symm = f.symm.toEquiv := rfl
 
 @[to_additive (attr := simp)]
-theorem equivLike_inv_eq_symm (f : α ≃*o β) : EquivLike.inv f = f.symm := rfl
+lemma symm_toOrderIso (f : α ≃*o β) : f.toOrderIso.symm = f.symm.toOrderIso := rfl
 
 @[to_additive (attr := simp)]
-theorem toEquiv_symm (f : α ≃*o β) : (f.symm : β ≃ α) = (f : α ≃ β).symm := rfl
+lemma symm_toOrderIso (f : α ≃*o β) : f.toOrderIso.symm = f.symm.toOrderIso := rfl
+
+@[to_additive (attr := simp)]
+theorem equivLike_inv_eq_symm (f : α ≃*o β) : EquivLike.inv f = f.symm := rfl
 
 @[to_additive (attr := simp)]
 theorem symm_symm (f : α ≃*o β) : f.symm.symm = f := rfl