From a8e1e42677a0e71b6265254343377fabd4711db0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Tue, 10 Dec 2024 11:00:21 +0000 Subject: [PATCH] refactor: review the `simps` projections of `OneHom`, `Mulhom`, `MonoidHom` Make `simps` generate `coe_concreteHom` rather than`concreteHom_apply`. From FLT --- .../BigOperators/Group/Multiset/Basic.lean | 2 +- Mathlib/Algebra/Group/Hom/Defs.lean | 193 ++++++++---------- Mathlib/Algebra/Group/Subgroup/Defs.lean | 17 +- .../Algebra/Group/Submonoid/Operations.lean | 2 +- Mathlib/Algebra/Group/WithOne/Basic.lean | 2 +- Mathlib/Algebra/GroupWithZero/WithZero.lean | 4 +- Mathlib/Algebra/Module/End.lean | 2 +- Mathlib/GroupTheory/NoncommCoprod.lean | 3 +- 8 files changed, 103 insertions(+), 122 deletions(-) diff --git a/Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean b/Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean index 930c2689951fa..8053c844e7d3f 100644 --- a/Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean +++ b/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 diff --git a/Mathlib/Algebra/Group/Hom/Defs.lean b/Mathlib/Algebra/Group/Hom/Defs.lean index 08c5149911c7e..e7e61bcb02d3a 100644 --- a/Mathlib/Algebra/Group/Hom/Defs.lean +++ b/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,27 +593,9 @@ 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) : @@ -595,11 +603,6 @@ protected def OneHom.copy [One M] [One N] (f : OneHom M N) (f' : M → N) (h : f 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 := @@ -607,7 +610,7 @@ theorem OneHom.coe_copy_eq {_ : One M} {_ : One N} (f : OneHom M N) (f' : M → /-- 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) : @@ -615,11 +618,6 @@ protected def MulHom.copy [Mul M] [Mul N] (f : M →ₙ* N) (f' : M → N) (h : 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 := @@ -627,18 +625,13 @@ theorem MulHom.coe_copy_eq {_ : Mul M} {_ : Mul N} (f : M →ₙ* N) (f' : M → /-- 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 := diff --git a/Mathlib/Algebra/Group/Subgroup/Defs.lean b/Mathlib/Algebra/Group/Subgroup/Defs.lean index a97477f0b4657..cc3fc69cced7e 100644 --- a/Mathlib/Algebra/Group/Subgroup/Defs.lean +++ b/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 := diff --git a/Mathlib/Algebra/Group/Submonoid/Operations.lean b/Mathlib/Algebra/Group/Submonoid/Operations.lean index a997c5650f854..b42ded813eafc 100644 --- a/Mathlib/Algebra/Group/Submonoid/Operations.lean +++ b/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 diff --git a/Mathlib/Algebra/Group/WithOne/Basic.lean b/Mathlib/Algebra/Group/WithOne/Basic.lean index 5382fd1d0651a..cce6d90266ad5 100644 --- a/Mathlib/Algebra/Group/WithOne/Basic.lean +++ b/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 diff --git a/Mathlib/Algebra/GroupWithZero/WithZero.lean b/Mathlib/Algebra/GroupWithZero/WithZero.lean index 9ad955134228e..ec103c7682510 100644 --- a/Mathlib/Algebra/GroupWithZero/WithZero.lean +++ b/Mathlib/Algebra/GroupWithZero/WithZero.lean @@ -71,7 +71,7 @@ instance mulZeroOneClass [MulOneClass α] : MulZeroOneClass (WithZero α) where mul_one := Option.map₂_right_identity mul_one /-- Coercion as a monoid hom. -/ -@[simps apply] +@[simps (config := .asFn)] def coeMonoidHom : α →* WithZero α where toFun := (↑) map_one' := rfl @@ -90,7 +90,7 @@ theorem monoidWithZeroHom_ext ⦃f g : WithZero α →*₀ β⦄ | (g : α) => DFunLike.congr_fun h g /-- The (multiplicative) universal property of `WithZero`. -/ -@[simps! symm_apply_apply] +@[simps! (config := .asFn)] noncomputable nonrec def lift' : (α →* β) ≃ (WithZero α →*₀ β) where toFun f := { toFun := fun diff --git a/Mathlib/Algebra/Module/End.lean b/Mathlib/Algebra/Module/End.lean index a0a9057609f45..746e2fced1170 100644 --- a/Mathlib/Algebra/Module/End.lean +++ b/Mathlib/Algebra/Module/End.lean @@ -35,7 +35,7 @@ variable (R M) /-- `(•)` as an `AddMonoidHom`. This is a stronger version of `DistribMulAction.toAddMonoidEnd` -/ -@[simps! apply_apply] +@[simps!] def Module.toAddMonoidEnd : R →+* AddMonoid.End M := { DistribMulAction.toAddMonoidEnd R M with -- Porting note: the two `show`s weren't needed in mathlib3. diff --git a/Mathlib/GroupTheory/NoncommCoprod.lean b/Mathlib/GroupTheory/NoncommCoprod.lean index 8bb21af12efde..9023e9d072664 100644 --- a/Mathlib/GroupTheory/NoncommCoprod.lean +++ b/Mathlib/GroupTheory/NoncommCoprod.lean @@ -88,8 +88,7 @@ def noncommCoprod : M × N →* P where @[to_additive "Variant of `AddMonoidHom.noncomCoprod_apply` with the sum written in the other direction"] theorem noncommCoprod_apply' (comm) (mn : M × N) : - (f.noncommCoprod g comm) mn = g mn.2 * f mn.1 := by - rw [← comm, MonoidHom.noncommCoprod_apply] + (f.noncommCoprod g comm) mn = g mn.2 * f mn.1 := by simp [(comm _ _).eq] @[to_additive (attr := simp)] theorem noncommCoprod_comp_inl : (f.noncommCoprod g comm).comp (inl M N) = f :=