fix

Mathlib/Algebra/BigOperators/Group/Multiset.lean

@@ -271,7 +271,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/Submonoid/Operations.lean

@@ -693,7 +693,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

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

Mathlib/Algebra/Module/End.lean

@@ -38,7 +38,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.

Mathlib/GroupTheory/NoncommCoprod.lean

@@ -50,9 +50,7 @@ def noncommCoprod (comm : ∀ m n, Commute (f m) (g n)) : M × N →ₙ* P where
 @[to_additive
   "Variant of `AddHom.noncommCoprod_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, noncommCoprod_apply]
-
+    (f.noncommCoprod g comm) mn = g mn.2 * f mn.1 := by simp [(comm _ _).eq]
 
 @[to_additive]
 theorem comp_noncommCoprod {Q : Type*} [Semigroup Q] (h : P →ₙ* Q)
@@ -86,8 +84,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 :=