refactor: review the simps projections of OneHom, Mulhom, `Mono…

…idHom`

Make `simps` generate `coe_concreteHom` rather than`concreteHom_apply`.

From FLT

Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean

@@ -194,7 +194,7 @@ theorem prod_map_div : (m.map fun i => f i / g i).prod = (m.map f).prod / (m.map
 @[to_additive]
 theorem prod_map_zpow {n : ℤ} : (m.map fun i => f i ^ n).prod = (m.map f).prod ^ n := by
   convert (m.map f).prod_hom (zpowGroupHom n : α →* α)
-  simp only [map_map, Function.comp_apply, zpowGroupHom_apply]
+  simp [map_map, Function.comp_apply]
 
 end DivisionCommMonoid
 

Mathlib/Algebra/Group/Hom/Defs.lean

@@ -489,68 +489,94 @@ section Coes
 
 /-! Bundled morphisms can be down-cast to weaker bundlings -/
 
-attribute [coe] MonoidHom.toOneHom
-attribute [coe] AddMonoidHom.toZeroHom
+namespace OneHom
+variable [One M] [One N]
 
-/-- `MonoidHom` down-cast to a `OneHom`, forgetting the multiplicative property. -/
-@[to_additive "`AddMonoidHom` down-cast to a `ZeroHom`, forgetting the additive property"]
-instance MonoidHom.coeToOneHom [MulOneClass M] [MulOneClass N] :
-  Coe (M →* N) (OneHom M N) := ⟨MonoidHom.toOneHom⟩
+/-- See Note [custom simps projection]. We want to generate
+`coe_concreteHom : ⇑concreteHom = unbundledFun` rather than
+`concreteHom_apply a : ⇑concreteHom a = unbundledFun a`. -/
+@[to_additive
+"/-- See Note [custom simps projection]. We want to generate
+`coe_concreteHom : ⇑concreteHom = unbundledFun` rather than
+`concreteHom_apply a : ⇑concreteHom a = unbundledFun a`. -/"]
+def Simps.coe (f : OneHom M N) : M → N := f
 
-attribute [coe] MonoidHom.toMulHom
-attribute [coe] AddMonoidHom.toAddHom
+initialize_simps_projections OneHom (toFun → coe, as_prefix coe)
+initialize_simps_projections ZeroHom (toFun → coe, as_prefix coe)
 
-/-- `MonoidHom` down-cast to a `MulHom`, forgetting the 1-preserving property. -/
-@[to_additive "`AddMonoidHom` down-cast to an `AddHom`, forgetting the 0-preserving property."]
-instance MonoidHom.coeToMulHom [MulOneClass M] [MulOneClass N] :
-  Coe (M →* N) (M →ₙ* N) := ⟨MonoidHom.toMulHom⟩
+@[to_additive (attr := simp)] lemma toFun_eq_coe (f : OneHom M N) : f.toFun = f := rfl
+@[to_additive (attr := simp)] lemma coe_mk (f : M → N) (hone) : (mk f hone : M → N) = f := rfl
+@[to_additive (attr := simp)] lemma mk_coe (f : OneHom M N) : mk f f.map_one' = f := rfl
 
--- 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 := ext)]
+lemma ext ⦃f g : OneHom M N⦄ (h : ∀ x, f x = g x) : f = g := DFunLike.ext _ _ h
 
-@[to_additive (attr := simp)]
-theorem OneHom.coe_mk [One M] [One N] (f : M → N) (h1) : (OneHom.mk f h1 : M → N) = f := rfl
+end OneHom
 
-@[to_additive (attr := simp)]
-theorem OneHom.toFun_eq_coe [One M] [One N] (f : OneHom M N) : f.toFun = f := rfl
+namespace MulHom
+variable [Mul M] [Mul N]
 
-@[to_additive (attr := simp)]
-theorem MulHom.coe_mk [Mul M] [Mul N] (f : M → N) (hmul) : (MulHom.mk f hmul : M → N) = f := rfl
+/-- See Note [custom simps projection]. We want to generate
+`coe_concreteHom : ⇑concreteHom = unbundledFun` rather than
+`concreteHom_apply a : ⇑concreteHom a = unbundledFun a`. -/
+@[to_additive
+"/-- See Note [custom simps projection]. We want to generate
+`coe_concreteHom : ⇑concreteHom = unbundledFun` rather than
+`concreteHom_apply a : ⇑concreteHom a = unbundledFun a`. -/"]
+def Simps.coe (f : M →ₙ* N) : M → N := f
 
-@[to_additive (attr := simp)]
-theorem MulHom.toFun_eq_coe [Mul M] [Mul N] (f : M →ₙ* N) : f.toFun = f := rfl
+initialize_simps_projections MulHom (toFun → coe, as_prefix coe)
+initialize_simps_projections AddHom (toFun → coe, as_prefix coe)
 
-@[to_additive (attr := simp)]
-theorem MonoidHom.coe_mk [MulOneClass M] [MulOneClass N] (f hmul) :
-    (MonoidHom.mk f hmul : M → N) = f := rfl
+@[to_additive (attr := simp)] lemma toFun_eq_coe (f : M →ₙ* N) : f.toFun = f := rfl
+@[to_additive (attr := simp)] lemma coe_mk (f : M → N) (hmul) : (mk f hmul : M → N) = f := rfl
+@[to_additive (attr := simp)] lemma mk_coe (f : M →ₙ* N) : mk f f.map_mul' = f := rfl
 
-@[to_additive (attr := simp)]
-theorem MonoidHom.toOneHom_coe [MulOneClass M] [MulOneClass N] (f : M →* N) :
-    (f.toOneHom : M → N) = f := rfl
+@[to_additive (attr := ext)]
+lemma ext ⦃f g : M →ₙ* N⦄ (h : ∀ x, f x = g x) : f = g := DFunLike.ext _ _ h
 
-@[to_additive (attr := simp)]
-theorem MonoidHom.toMulHom_coe [MulOneClass M] [MulOneClass N] (f : M →* N) :
-    f.toMulHom.toFun = f := rfl
+end MulHom
 
-@[to_additive]
-theorem MonoidHom.toFun_eq_coe [MulOneClass M] [MulOneClass N] (f : M →* N) : f.toFun = f := rfl
+namespace MonoidHom
+variable [MulOneClass M] [MulOneClass N]
 
-@[to_additive (attr := ext)]
-theorem OneHom.ext [One M] [One N] ⦃f g : OneHom M N⦄ (h : ∀ x, f x = g x) : f = g :=
-  DFunLike.ext _ _ h
+attribute [coe] MonoidHom.toOneHom
+attribute [coe] AddMonoidHom.toZeroHom
+attribute [coe] MonoidHom.toMulHom
+attribute [coe] AddMonoidHom.toAddHom
 
-@[to_additive (attr := ext)]
-theorem MulHom.ext [Mul M] [Mul N] ⦃f g : M →ₙ* N⦄ (h : ∀ x, f x = g x) : f = g :=
-  DFunLike.ext _ _ h
+/-- `MonoidHom` down-cast to a `OneHom`, forgetting the multiplicative property. -/
+@[to_additive "`AddMonoidHom` down-cast to a `ZeroHom`, forgetting the additive property"]
+instance coeToOneHom : Coe (M →* N) (OneHom M N) := ⟨MonoidHom.toOneHom⟩
+
+/-- `MonoidHom` down-cast to a `MulHom`, forgetting the 1-preserving property. -/
+@[to_additive "`AddMonoidHom` down-cast to an `AddHom`, forgetting the 0-preserving property."]
+instance coeToMulHom : Coe (M →* N) (M →ₙ* N) := ⟨MonoidHom.toMulHom⟩
+
+/-- See Note [custom simps projection]. We want to generate
+`coe_concreteHom : ⇑concreteHom = unbundledFun` rather than
+`concreteHom_apply a : ⇑concreteHom a = unbundledFun a`. -/
+@[to_additive
+"/-- See Note [custom simps projection]. We want to generate
+`coe_concreteHom : ⇑concreteHom = unbundledFun` rather than
+`concreteHom_apply a : ⇑concreteHom a = unbundledFun a`. -/"]
+def Simps.coe (f : M →* N) : M → N := f
+
+initialize_simps_projections MonoidHom (toFun → coe, as_prefix coe)
+initialize_simps_projections AddMonoidHom (toFun → coe, as_prefix coe)
+
+@[to_additive (attr := simp)] lemma coe_toOneHom (f : M →* N) : f.toOneHom = f := rfl
+@[to_additive (attr := simp)] lemma coe_toMulHom (f : M →* N) : f.toMulHom = f := rfl
+@[to_additive (attr := simp)] lemma coe_mk (f hmul) : (mk f hmul : M → N) = f := rfl
+@[to_additive (attr := simp)] lemma mk_coe (f : M →* N) : mk f f.map_mul' = f := rfl
+
+@[to_additive] lemma toFun_eq_coe (f : M →* N) : f.toFun = f := rfl
 
 @[to_additive (attr := ext)]
-theorem MonoidHom.ext [MulOneClass M] [MulOneClass N] ⦃f g : M →* N⦄ (h : ∀ x, f x = g x) : f = g :=
-  DFunLike.ext _ _ h
+lemma ext ⦃f g : M →* N⦄ (h : ∀ x, f x = g x) : f = g := DFunLike.ext _ _ h
+
+end MonoidHom
+end Coes
 
 namespace MonoidHom
 
@@ -567,78 +593,45 @@ def mk' (f : M → G) (map_mul : ∀ a b : M, f (a * b) = f a * f b) : M →* G
 
 end MonoidHom
 
-section Deprecated
-
-end Deprecated
-
-@[to_additive (attr := simp)]
-theorem OneHom.mk_coe [One M] [One N] (f : OneHom M N) (h1) : OneHom.mk f h1 = f :=
-  OneHom.ext fun _ => rfl
-
-@[to_additive (attr := simp)]
-theorem MulHom.mk_coe [Mul M] [Mul N] (f : M →ₙ* N) (hmul) : MulHom.mk f hmul = f :=
-  MulHom.ext fun _ => rfl
-
-@[to_additive (attr := simp)]
-theorem MonoidHom.mk_coe [MulOneClass M] [MulOneClass N] (f : M →* N) (hmul) :
-    MonoidHom.mk f hmul = f := MonoidHom.ext fun _ => rfl
-
-end Coes
-
 /-- Copy of a `OneHom` with a new `toFun` equal to the old one. Useful to fix definitional
 equalities. -/
-@[to_additive
+@[to_additive (attr := simps (config := .asFn))
   "Copy of a `ZeroHom` with a new `toFun` equal to the old one. Useful to fix
   definitional equalities."]
 protected def OneHom.copy [One M] [One N] (f : OneHom M N) (f' : M → N) (h : f' = f) :
     OneHom M N where
   toFun := f'
   map_one' := h.symm ▸ f.map_one'
 
-@[to_additive (attr := simp)]
-theorem OneHom.coe_copy {_ : One M} {_ : One N} (f : OneHom M N) (f' : M → N) (h : f' = f) :
-    (f.copy f' h) = f' :=
-  rfl
-
 @[to_additive]
 theorem OneHom.coe_copy_eq {_ : One M} {_ : One N} (f : OneHom M N) (f' : M → N) (h : f' = f) :
     f.copy f' h = f :=
   DFunLike.ext' h
 
 /-- Copy of a `MulHom` with a new `toFun` equal to the old one. Useful to fix definitional
 equalities. -/
-@[to_additive
+@[to_additive (attr := simps (config := .asFn))
   "Copy of an `AddHom` with a new `toFun` equal to the old one. Useful to fix
   definitional equalities."]
 protected def MulHom.copy [Mul M] [Mul N] (f : M →ₙ* N) (f' : M → N) (h : f' = f) :
     M →ₙ* N where
   toFun := f'
   map_mul' := h.symm ▸ f.map_mul'
 
-@[to_additive (attr := simp)]
-theorem MulHom.coe_copy {_ : Mul M} {_ : Mul N} (f : M →ₙ* N) (f' : M → N) (h : f' = f) :
-    (f.copy f' h) = f' :=
-  rfl
-
 @[to_additive]
 theorem MulHom.coe_copy_eq {_ : Mul M} {_ : Mul N} (f : M →ₙ* N) (f' : M → N) (h : f' = f) :
     f.copy f' h = f :=
   DFunLike.ext' h
 
 /-- Copy of a `MonoidHom` with a new `toFun` equal to the old one. Useful to fix
 definitional equalities. -/
-@[to_additive
+@[to_additive (attr := simps! (config := .asFn))
   "Copy of an `AddMonoidHom` with a new `toFun` equal to the old one. Useful to fix
   definitional equalities."]
 protected def MonoidHom.copy [MulOneClass M] [MulOneClass N] (f : M →* N) (f' : M → N)
     (h : f' = f) : M →* N :=
   { f.toOneHom.copy f' h, f.toMulHom.copy f' h with }
 
-@[to_additive (attr := simp)]
-theorem MonoidHom.coe_copy {_ : MulOneClass M} {_ : MulOneClass N} (f : M →* N) (f' : M → N)
-    (h : f' = f) : (f.copy f' h) = f' :=
-  rfl
-
 @[to_additive]
 theorem MonoidHom.copy_eq {_ : MulOneClass M} {_ : MulOneClass N} (f : M →* N) (f' : M → N)
     (h : f' = f) : f.copy f' h = f :=
@@ -688,19 +681,22 @@ theorem map_exists_left_inv (f : F) {x : M} (hx : ∃ y, y * x = 1) : ∃ y, y *
 end MonoidHom
 
 /-- The identity map from a type with 1 to itself. -/
-@[to_additive (attr := simps) "The identity map from a type with zero to itself."]
+@[to_additive (attr := simps (config := .asFn))
+"The identity map from a type with zero to itself."]
 def OneHom.id (M : Type*) [One M] : OneHom M M where
   toFun x := x
   map_one' := rfl
 
 /-- The identity map from a type with multiplication to itself. -/
-@[to_additive (attr := simps) "The identity map from a type with addition to itself."]
+@[to_additive (attr := simps (config := .asFn))
+"The identity map from a type with addition to itself."]
 def MulHom.id (M : Type*) [Mul M] : M →ₙ* M where
   toFun x := x
   map_mul' _ _ := rfl
 
 /-- The identity map from a monoid to itself. -/
-@[to_additive (attr := simps) "The identity map from an additive monoid to itself."]
+@[to_additive (attr := simps (config := .asFn))
+"The identity map from an additive monoid to itself."]
 def MonoidHom.id (M : Type*) [MulOneClass M] : M →* M where
   toFun x := x
   map_one' := rfl
@@ -716,37 +712,28 @@ lemma MulHom.coe_id {M : Type*} [Mul M] : (MulHom.id M : M → M) = _root_.id :=
 lemma MonoidHom.coe_id {M : Type*} [MulOneClass M] : (MonoidHom.id M : M → M) = _root_.id := rfl
 
 /-- Composition of `OneHom`s as a `OneHom`. -/
-@[to_additive "Composition of `ZeroHom`s as a `ZeroHom`."]
+@[to_additive (attr := simps (config := .asFn))
+"Composition of `ZeroHom`s as a `ZeroHom`."]
 def OneHom.comp [One M] [One N] [One P] (hnp : OneHom N P) (hmn : OneHom M N) : OneHom M P where
   toFun := hnp ∘ hmn
   map_one' := by simp
 
 /-- Composition of `MulHom`s as a `MulHom`. -/
-@[to_additive "Composition of `AddHom`s as an `AddHom`."]
+@[to_additive (attr := simps (config := .asFn))
+"Composition of `AddHom`s as an `AddHom`."]
 def MulHom.comp [Mul M] [Mul N] [Mul P] (hnp : N →ₙ* P) (hmn : M →ₙ* N) : M →ₙ* P where
   toFun := hnp ∘ hmn
   map_mul' x y := by simp
 
 /-- Composition of monoid morphisms as a monoid morphism. -/
-@[to_additive "Composition of additive monoid morphisms as an additive monoid morphism."]
+@[to_additive (attr := simps (config := .asFn))
+"Composition of additive monoid morphisms as an additive monoid morphism."]
 def MonoidHom.comp [MulOneClass M] [MulOneClass N] [MulOneClass P] (hnp : N →* P) (hmn : M →* N) :
     M →* P where
   toFun := hnp ∘ hmn
   map_one' := by simp
   map_mul' := by simp
 
-@[to_additive (attr := simp)]
-theorem OneHom.coe_comp [One M] [One N] [One P] (g : OneHom N P) (f : OneHom M N) :
-    ↑(g.comp f) = g ∘ f := rfl
-
-@[to_additive (attr := simp)]
-theorem MulHom.coe_comp [Mul M] [Mul N] [Mul P] (g : N →ₙ* P) (f : M →ₙ* N) :
-    ↑(g.comp f) = g ∘ f := rfl
-
-@[to_additive (attr := simp)]
-theorem MonoidHom.coe_comp [MulOneClass M] [MulOneClass N] [MulOneClass P]
-    (g : N →* P) (f : M →* N) : ↑(g.comp f) = g ∘ f := rfl
-
 @[to_additive]
 theorem OneHom.comp_apply [One M] [One N] [One P] (g : OneHom N P) (f : OneHom M N) (x : M) :
     g.comp f x = g (f x) := rfl
@@ -856,7 +843,7 @@ protected theorem MonoidHom.map_zpow' [DivInvMonoid M] [DivInvMonoid N] (f : M 
     f (a ^ n) = f a ^ n := map_zpow' f hf a n
 
 /-- Makes a `OneHom` inverse from the bijective inverse of a `OneHom` -/
-@[to_additive (attr := simps)
+@[to_additive (attr := simps (config := .asFn))
   "Make a `ZeroHom` inverse from the bijective inverse of a `ZeroHom`"]
 def OneHom.inverse [One M] [One N]
     (f : OneHom M N) (g : N → M)
@@ -866,7 +853,7 @@ def OneHom.inverse [One M] [One N]
     map_one' := by rw [← f.map_one, h₁] }
 
 /-- Makes a multiplicative inverse from a bijection which preserves multiplication. -/
-@[to_additive (attr := simps)
+@[to_additive (attr := simps (config := .asFn))
   "Makes an additive inverse from a bijection which preserves addition."]
 def MulHom.inverse [Mul M] [Mul N] (f : M →ₙ* N) (g : N → M)
     (h₁ : Function.LeftInverse g f)
@@ -879,7 +866,7 @@ def MulHom.inverse [Mul M] [Mul N] (f : M →ₙ* N) (g : N → M)
       _ = g x * g y := h₁ _
 
 /-- The inverse of a bijective `MonoidHom` is a `MonoidHom`. -/
-@[to_additive (attr := simps)
+@[to_additive (attr := simps (config := .asFn))
   "The inverse of a bijective `AddMonoidHom` is an `AddMonoidHom`."]
 def MonoidHom.inverse {A B : Type*} [Monoid A] [Monoid B] (f : A →* B) (g : B → A)
     (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) : B →* A :=

Mathlib/Algebra/Group/Subgroup/Defs.lean

@@ -189,14 +189,13 @@ instance (priority := 75) toCommGroup {G : Type*} [CommGroup G] [SetLike S G] [S
     (fun _ _ => rfl) fun _ _ => rfl
 
 /-- The natural group hom from a subgroup of group `G` to `G`. -/
-@[to_additive (attr := coe)
+@[to_additive (attr := simps (config := .asFn))
   "The natural group hom from an additive subgroup of `AddGroup` `G` to `G`."]
 protected def subtype : H →* G where
   toFun := ((↑) : H → G); map_one' := rfl; map_mul' := fun _ _ => rfl
 
-@[to_additive (attr := simp)]
-theorem coeSubtype : (SubgroupClass.subtype H : H → G) = ((↑) : H → G) := by
-  rfl
+@[to_additive (attr := deprecated coe_subtype (since := "2024-12-10"))]
+alias coeSubtype := coe_subtype
 
 variable {H}
 
@@ -234,15 +233,13 @@ theorem inclusion_inclusion {L : S} (hHK : H ≤ K) (hKL : K ≤ L) (x : H) :
   rfl
 
 @[to_additive (attr := simp)]
-theorem coe_inclusion {H K : S} {h : H ≤ K} (a : H) : (inclusion h a : G) = a := by
-  cases a
-  simp only [inclusion, MonoidHom.mk'_apply]
+theorem coe_inclusion {H K : S} {h : H ≤ K} (a : H) : (inclusion h a : G) = a := rfl
 
 @[to_additive (attr := simp)]
 theorem subtype_comp_inclusion {H K : S} (hH : H ≤ K) :
     (SubgroupClass.subtype K).comp (inclusion hH) = SubgroupClass.subtype H := by
   ext
-  simp only [MonoidHom.comp_apply, coeSubtype, coe_inclusion]
+  simp only [MonoidHom.comp_apply, coe_subtype, coe_inclusion]
 
 end SubgroupClass
 
@@ -534,9 +531,7 @@ def inclusion {H K : Subgroup G} (h : H ≤ K) : H →* K :=
   MonoidHom.mk' (fun x => ⟨x, h x.2⟩) fun _ _ => rfl
 
 @[to_additive (attr := simp)]
-theorem coe_inclusion {H K : Subgroup G} {h : H ≤ K} (a : H) : (inclusion h a : G) = a := by
-  cases a
-  simp only [inclusion, coe_mk, MonoidHom.mk'_apply]
+theorem coe_inclusion {H K : Subgroup G} {h : H ≤ K} (a : H) : (inclusion h a : G) = a := rfl
 
 @[to_additive]
 theorem inclusion_injective {H K : Subgroup G} (h : H ≤ K) : Function.Injective <| inclusion h :=

Mathlib/Algebra/Group/Submonoid/Operations.lean

@@ -694,7 +694,7 @@ theorem restrict_mrange (f : M →* N) : mrange (f.restrict S) = S.map f := by
   simp [SetLike.ext_iff]
 
 /-- Restriction of a monoid hom to a submonoid of the codomain. -/
-@[to_additive (attr := simps apply)
+@[to_additive (attr := simps (config := .asFn))
   "Restriction of an `AddMonoid` hom to an `AddSubmonoid` of the codomain."]
 def codRestrict {S} [SetLike S N] [SubmonoidClass S N] (f : M →* N) (s : S) (h : ∀ x, f x ∈ s) :
     M →* s where

Mathlib/Algebra/Group/WithOne/Basic.lean

@@ -40,7 +40,7 @@ section
 -- workaround: we make `WithOne`/`WithZero` irreducible for this definition, otherwise `simps`
 -- will unfold it in the statement of the lemma it generates.
 /-- `WithOne.coe` as a bundled morphism -/
-@[to_additive (attr := simps apply) "`WithZero.coe` as a bundled morphism"]
+@[to_additive (attr := simps) "`WithZero.coe` as a bundled morphism"]
 def coeMulHom [Mul α] : α →ₙ* WithOne α where
   toFun := coe
   map_mul' _ _ := rfl