diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean
index 22817938353332..ff296fa1ca57c9 100644
--- a/Mathlib/Algebra/Colimit/DirectLimit.lean
+++ b/Mathlib/Algebra/Colimit/DirectLimit.lean
@@ -128,8 +128,12 @@ variable [∀ i, Monoid (G i)] [∀ i j h, MonoidHomClass (T h) (G i) (G j)]
   one_mul := one_mul
   mul_one := mul_one
   npow n := map _ _ (fun _ ↦ (· ^ n)) fun _ _ _ x ↦ map_pow _ x n
-  npow_zero := DirectLimit.induction _ fun i _ ↦ by simp_rw [map_def, pow_zero, one_def i]
-  npow_succ n := DirectLimit.induction _ fun i _ ↦ by simp_rw [map_def, pow_succ, mul_def]
+  npow_zero := DirectLimit.induction _ fun i _ ↦ by
+    simp_rw [HPow.hPow, Pow.pow]
+    simp_rw [map_def, pow_zero, one_def i]
+  npow_succ n := DirectLimit.induction _ fun i _ ↦ by
+    simp_rw [HPow.hPow, Pow.pow]
+    simp_rw [map_def, pow_succ, mul_def]
 
 @[to_additive] theorem npow_def (i x) (n : ℕ) : ⟦⟨i, x⟩⟧ ^ n = (⟦⟨i, x ^ n⟩⟧ : DirectLimit G f) :=
   rfl
@@ -149,11 +153,12 @@ variable [∀ i, Group (G i)] [∀ i j h, MonoidHomClass (T h) (G i) (G j)]
   zpow n := map _ _ (fun _ ↦ (· ^ n)) fun _ _ _ x ↦ map_zpow _ x n
   div_eq_mul_inv := DirectLimit.induction₂ _ fun i _ _ ↦ show map₂ .. = _ * map .. by
     simp_rw [map₂_def, map_def, div_eq_mul_inv, mul_def]
-  zpow_zero' := DirectLimit.induction _ fun i _ ↦ by simp_rw [map_def, zpow_zero, one_def i]
+  zpow_zero' := DirectLimit.induction _ fun i _ ↦ by
+    simp_rw [HPow.hPow, Pow.pow, map_def, zpow_zero, one_def i]
   zpow_succ' n := DirectLimit.induction _ fun i x ↦ by
-    simp_rw [map_def, mul_def]; congr; apply DivInvMonoid.zpow_succ'
+    simp_rw [HPow.hPow, Pow.pow, map_def, mul_def]; congr; apply DivInvMonoid.zpow_succ'
   zpow_neg' n := DirectLimit.induction _ fun i x ↦ by
-    simp_rw +instances [map_def]; congr; apply DivInvMonoid.zpow_neg'
+    simp_rw [HPow.hPow, Pow.pow, map_def]; congr; apply DivInvMonoid.zpow_neg'
   inv_mul_cancel := DirectLimit.induction _ fun i _ ↦ by
     simp_rw [map_def, mul_def, inv_mul_cancel, one_def i]
 
@@ -216,11 +221,12 @@ instance : GroupWithZero (DirectLimit G f) where
   zpow n := map _ _ (fun _ ↦ (· ^ n)) fun _ _ _ x ↦ map_zpow₀ _ x n
   div_eq_mul_inv := DirectLimit.induction₂ _ fun i _ _ ↦ show map₂ .. = _ * map .. by
     simp_rw [map₂_def, map_def, div_eq_mul_inv, mul_def]
-  zpow_zero' := DirectLimit.induction _ fun i _ ↦ by simp_rw [map_def, zpow_zero, one_def i]
+  zpow_zero' := DirectLimit.induction _ fun i _ ↦ by
+    simp_rw [HPow.hPow, Pow.pow, map_def, zpow_zero, one_def i]
   zpow_succ' n := DirectLimit.induction _ fun i x ↦ by
-    simp_rw [map_def, mul_def]; congr; apply DivInvMonoid.zpow_succ'
+    simp_rw [HPow.hPow, Pow.pow, map_def, mul_def]; congr; apply DivInvMonoid.zpow_succ'
   zpow_neg' n := DirectLimit.induction _ fun i x ↦ by
-    simp_rw [map_def]; congr; apply DivInvMonoid.zpow_neg'
+    simp_rw [HPow.hPow, Pow.pow, map_def]; congr; apply DivInvMonoid.zpow_neg'
   inv_zero := show ⟦_⟧ = ⟦_⟧ by simp_rw [inv_zero]
   mul_inv_cancel := DirectLimit.induction _ fun i x ne ↦ by
     have : x ≠ 0 := by rintro rfl; exact ne (zero_def i).symm
diff --git a/Mathlib/Algebra/FreeAlgebra.lean b/Mathlib/Algebra/FreeAlgebra.lean
index bd1c13602d3b76..27d2e2e302880c 100644
--- a/Mathlib/Algebra/FreeAlgebra.lean
+++ b/Mathlib/Algebra/FreeAlgebra.lean
@@ -201,7 +201,6 @@ instance instMonoidWithZero : MonoidWithZero (FreeAlgebra R X) where
   mul_assoc := by
     rintro ⟨⟩ ⟨⟩ ⟨⟩
     exact Quot.sound Rel.mul_assoc
-  one := Quot.mk _ 1
   one_mul := by
     rintro ⟨⟩
     exact Quot.sound Rel.one_mul
@@ -237,7 +236,6 @@ instance instAddCommMonoid : AddCommMonoid (FreeAlgebra R X) where
   add_comm := by
     rintro ⟨⟩ ⟨⟩
     exact Quot.sound Rel.add_comm
-  nsmul := (· • ·)
   nsmul_zero := by
     rintro ⟨⟩
     change Quot.mk _ (_ * _) = _
@@ -245,7 +243,7 @@ instance instAddCommMonoid : AddCommMonoid (FreeAlgebra R X) where
     exact Quot.sound Rel.zero_mul
   nsmul_succ n := by
     rintro ⟨a⟩
-    dsimp +instances only [HSMul.hSMul, instSMul, Quot.map]
+    dsimp only [HSMul.hSMul, SMul.smul, NSMul.nsmul, Quot.map]
     rw [map_add, map_one, mk_mul, mk_mul, ← add_one_mul (_ : FreeAlgebra R X)]
     congr 1
     exact Quot.sound Rel.add_scalar
diff --git a/Mathlib/Algebra/Group/Action/Opposite.lean b/Mathlib/Algebra/Group/Action/Opposite.lean
index 10a71bb733c0fc..e9d24ae3a10599 100644
--- a/Mathlib/Algebra/Group/Action/Opposite.lean
+++ b/Mathlib/Algebra/Group/Action/Opposite.lean
@@ -15,7 +15,7 @@ This file defines the actions on the opposite type `SMul R Mᵐᵒᵖ`, and acti
 type, `SMul Rᵐᵒᵖ M`.
 
 Note that `MulOpposite.smul` is provided in an earlier file as it is needed to
-provide the `AddMonoid.nsmul` and `AddCommGroup.zsmul` fields.
+provide the `NSMul.nsmul` and `AddCommGroup.zsmul` fields.
 
 ## Notation
 
diff --git a/Mathlib/Algebra/Group/Defs.lean b/Mathlib/Algebra/Group/Defs.lean
index 336bd292f3eb31..24601211f17311 100644
--- a/Mathlib/Algebra/Group/Defs.lean
+++ b/Mathlib/Algebra/Group/Defs.lean
@@ -634,38 +634,51 @@ theorem npowRec_eq_npowBinRec : @npowRecAuto = @npowBinRecAuto := by
   iterate 2 rw [← npowBinRecAuto, ← npowRec_eq_npowBinRec]
   rfl
 
-/-- An `AddMonoid` is an `AddSemigroup` with an element `0` such that `0 + a = a + 0 = a`. -/
-class AddMonoid (M : Type u) extends AddSemigroup M, AddZeroClass M where
+/-- `NSMul` is an implementation detail of `AddMonoid`. It is necessary because it is not
+possible to extend `SMUl ℕ M` and `SMul ℤ M` at the same time. -/
+class NSMul (M : Type u) where
   /-- Multiplication by a natural number.
   Set this to `nsmulRec` unless `Module` diamonds are possible. -/
   protected nsmul : ℕ → M → M
+
+/-- `NPow` is an implementation detail of `Monoid`. It is necessary because it is not
+possible to extend `Pow M ℕ` and `Pow M ℤ` at the same time. -/
+@[to_additive]
+class NPow (M : Type u) where
+  /-- Raising to the power of a natural number. -/
+  protected npow : ℕ → M → M
+
+@[default_instance high, to_additive toSMul]
+instance NPow.toPow {M : Type*} [NPow M] : Pow M ℕ :=
+  ⟨fun x n ↦ NPow.npow n x⟩
+
+@[to_additive ofSMul]
+instance NPow.ofPow {M : Type*} [Pow M ℕ] : NPow M := ⟨fun n x ↦ Pow.pow x n⟩
+
+/-- An `AddMonoid` is an `AddSemigroup` with an element `0` such that `0 + a = a + 0 = a`. -/
+class AddMonoid (M : Type u) extends AddSemigroup M, AddZeroClass M, NSMul M where
   /-- Multiplication by `(0 : ℕ)` gives `0`. -/
-  protected nsmul_zero : ∀ x, nsmul 0 x = 0 := by intros; rfl
+  protected nsmul_zero (x : M) : 0 • x = 0 := by intros; rfl
   /-- Multiplication by `(n + 1 : ℕ)` behaves as expected. -/
-  protected nsmul_succ : ∀ (n : ℕ) (x), nsmul (n + 1) x = nsmul n x + x := by intros; rfl
+  protected nsmul_succ (n : ℕ) (x : M) : (n + 1) • x = n • x + x := by intros; rfl
 
 attribute [instance 150] AddSemigroup.toAdd
 attribute [instance 50] AddZero.toAdd
 
 /-- A `Monoid` is a `Semigroup` with an element `1` such that `1 * a = a * 1 = a`. -/
 @[to_additive]
-class Monoid (M : Type u) extends Semigroup M, MulOneClass M where
-  /-- Raising to the power of a natural number. -/
-  protected npow : ℕ → M → M := npowRecAuto
+class Monoid (M : Type u) extends Semigroup M, MulOneClass M, NPow M where
+  npow := npowRecAuto
   /-- Raising to the power `(0 : ℕ)` gives `1`. -/
-  protected npow_zero : ∀ x, npow 0 x = 1 := by intros; rfl
+  protected npow_zero (x : M) : x ^ 0 = 1 := by intros; rfl
   /-- Raising to the power `(n + 1 : ℕ)` behaves as expected. -/
-  protected npow_succ : ∀ (n : ℕ) (x), npow (n + 1) x = npow n x * x := by intros; rfl
-
-@[default_instance high, to_additive]
-instance Monoid.toPow {M : Type*} [Monoid M] : Pow M ℕ :=
-  ⟨fun x n ↦ Monoid.npow n x⟩
+  protected npow_succ (n : ℕ) (x : M) : x ^ (n + 1) = x ^ n * x := by intros; rfl
 
 section Monoid
 variable {M : Type*} [Monoid M] {a b c : M}
 
 @[to_additive (attr := simp) nsmul_eq_smul]
-theorem npow_eq_pow (n : ℕ) (x : M) : Monoid.npow n x = x ^ n :=
+theorem npow_eq_pow (n : ℕ) (x : M) : NPow.npow n x = x ^ n :=
   rfl
 
 @[to_additive] lemma left_inv_eq_right_inv (hba : b * a = 1) (hac : a * c = 1) : b = c := by
@@ -936,6 +949,27 @@ field of individual `DivInvMonoid`s constructed using that default value will no
 `.instance` transparency. -/
 def DivInvMonoid.div' {G : Type u} [Monoid G] [Inv G] (a b : G) : G := a * b⁻¹
 
+/-- `NSMul` is an implementation detail of `SubNegMonoid`. It is necessary because it is not
+possible to extend `SMUl ℕ M` and `SMul ℤ M` at the same time. -/
+class ZSMul (G : Type u) where
+  /-- Multiplication by an integer.
+  Set this to `zsmulRec` unless `Module` diamonds are possible. -/
+  protected zsmul : ℤ → G → G
+
+/-- `NPow` is an implementation detail of `SubNegMonoid`. It is necessary because it is not
+possible to extend `Pow M ℕ` and `Pow M ℤ` at the same time. -/
+@[to_additive]
+class ZPow (G : Type u) where
+  /-- The power operation: `a ^ n = a * ··· * a`; `a ^ (-n) = a⁻¹ * ··· a⁻¹` (`n` times) -/
+  protected zpow : ℤ → G → G
+
+@[to_additive toSMul]
+instance ZPow.toPow {M : Type*} [ZPow M] : Pow M ℤ :=
+  ⟨fun x n ↦ ZPow.zpow n x⟩
+
+@[to_additive ofSMul]
+instance ZPow.ofPow {M : Type*} [Pow M ℤ] : ZPow M := ⟨fun n x ↦ Pow.pow x n⟩
+
 /-- A `DivInvMonoid` is a `Monoid` with operations `/` and `⁻¹` satisfying
 `div_eq_mul_inv : ∀ a b, a / b = a * b⁻¹`.
 
@@ -954,19 +988,18 @@ In the same way, adding a `zpow` field makes it possible to avoid definitional f
 in diamonds. See the definition of `Monoid` and Note [forgetful inheritance] for more
 explanations on this.
 -/
-class DivInvMonoid (G : Type u) extends Monoid G, Inv G, Div G where
+class DivInvMonoid (G : Type u) extends Monoid G, Inv G, Div G, ZPow G where
   protected div := DivInvMonoid.div'
   /-- `a / b := a * b⁻¹` -/
   protected div_eq_mul_inv : ∀ a b : G, a / b = a * b⁻¹ := by intros; rfl
-  /-- The power operation: `a ^ n = a * ··· * a`; `a ^ (-n) = a⁻¹ * ··· a⁻¹` (`n` times) -/
-  protected zpow : ℤ → G → G := zpowRec npowRec
+  zpow := zpowRec npowRec
   /-- `a ^ 0 = 1` -/
-  protected zpow_zero' : ∀ a : G, zpow 0 a = 1 := by intros; rfl
+  protected zpow_zero' (a : G) : a ^ (0 : ℤ) = 1 := by intros; rfl
   /-- `a ^ (n + 1) = a ^ n * a` -/
-  protected zpow_succ' (n : ℕ) (a : G) : zpow n.succ a = zpow n a * a := by
+  protected zpow_succ' (n : ℕ) (a : G) : a ^ (n.succ : ℤ) = a ^ (n : ℤ) * a := by
     intros; rfl
   /-- `a ^ -(n + 1) = (a ^ (n + 1))⁻¹` -/
-  protected zpow_neg' (n : ℕ) (a : G) : zpow (Int.negSucc n) a = (zpow n.succ a)⁻¹ := by intros; rfl
+  protected zpow_neg' (n : ℕ) (a : G) : a ^ Int.negSucc n = (a ^ (n.succ : ℤ))⁻¹ := by intros; rfl
 
 /-- In a class equipped with instances of both `AddMonoid` and `Neg`, this definition records what
 the default definition for `Sub` would be: `a + -b`.  This is later provided as the default value
@@ -996,29 +1029,18 @@ In the same way, adding a `zsmul` field makes it possible to avoid definitional
 in diamonds. See the definition of `AddMonoid` and Note [forgetful inheritance] for more
 explanations on this.
 -/
-class SubNegMonoid (G : Type u) extends AddMonoid G, Neg G, Sub G where
+class SubNegMonoid (G : Type u) extends AddMonoid G, Neg G, Sub G, ZSMul G where
   protected sub := SubNegMonoid.sub'
   protected sub_eq_add_neg : ∀ a b : G, a - b = a + -b := by intros; rfl
-  /-- Multiplication by an integer.
-  Set this to `zsmulRec` unless `Module` diamonds are possible. -/
-  protected zsmul : ℤ → G → G
-  protected zsmul_zero' : ∀ a : G, zsmul 0 a = 0 := by intros; rfl
+  protected zsmul_zero' (a : G) : (0 : ℤ) • a = 0 := by intros; rfl
   protected zsmul_succ' (n : ℕ) (a : G) :
-      zsmul n.succ a = zsmul n a + a := by
+      (n.succ : ℤ) • a = (n : ℤ) • a + a := by
     intros; rfl
-  protected zsmul_neg' (n : ℕ) (a : G) : zsmul (Int.negSucc n) a = -zsmul n.succ a := by
+  protected zsmul_neg' (n : ℕ) (a : G) : (Int.negSucc n) • a = -((n.succ : ℤ) • a) := by
     intros; rfl
 
 attribute [to_additive SubNegMonoid] DivInvMonoid
 
-instance DivInvMonoid.toZPow {M} [DivInvMonoid M] : Pow M ℤ :=
-  ⟨fun x n ↦ DivInvMonoid.zpow n x⟩
-
-instance SubNegMonoid.toZSMul {M} [SubNegMonoid M] : SMul ℤ M :=
-  ⟨SubNegMonoid.zsmul⟩
-
-attribute [to_additive existing] DivInvMonoid.toZPow
-
 /-- A group is called *cyclic* if it is generated by a single element. -/
 class IsAddCyclic (G : Type u) [SMul ℤ G] : Prop where
   protected exists_zsmul_surjective : ∃ g : G, Function.Surjective (· • g : ℤ → G)
@@ -1038,7 +1060,7 @@ section DivInvMonoid
 variable [DivInvMonoid G]
 
 @[to_additive (attr := simp) zsmul_eq_smul] theorem zpow_eq_pow (n : ℤ) (x : G) :
-    DivInvMonoid.zpow n x = x ^ n :=
+    ZPow.zpow n x = x ^ n :=
   rfl
 
 @[to_additive (attr := simp) zero_zsmul] theorem zpow_zero (a : G) : a ^ (0 : ℤ) = 1 :=
diff --git a/Mathlib/Algebra/Group/Ext.lean b/Mathlib/Algebra/Group/Ext.lean
index 4de2994db58ed2..cbd55e357253ff 100644
--- a/Mathlib/Algebra/Group/Ext.lean
+++ b/Mathlib/Algebra/Group/Ext.lean
@@ -47,7 +47,7 @@ theorem Monoid.ext {M : Type u} ⦃m₁ m₂ : Monoid M⦄
   have : m₁.npow = m₂.npow := by
     ext n x
     exact @MonoidHom.map_pow M M m₁ m₂ f x n
-  rcases m₁ with @⟨@⟨⟨_⟩⟩, ⟨_⟩⟩
+  rcases m₁ with @⟨@⟨⟨_⟩⟩, ⟨_⟩, _, _, ⟨_⟩⟩
   congr
 
 @[to_additive]
@@ -138,7 +138,7 @@ theorem DivInvMonoid.ext {M : Type*} ⦃m₁ m₂ : DivInvMonoid M⦄
     exact (@div_eq_mul_inv _ m₁ a b).trans
       (((congr_fun (congr_fun h_mul a) _).trans
         (congr_arg _ (congr_fun h_inv b))).trans (@div_eq_mul_inv _ m₂ a b).symm)
-  rcases m₁ with @⟨_, ⟨_⟩, ⟨_⟩⟩
+  rcases m₁ with @⟨_, ⟨_⟩, ⟨_⟩, ⟨_⟩⟩
   congr
 
 @[to_additive]
diff --git a/Mathlib/Algebra/Group/Int/Defs.lean b/Mathlib/Algebra/Group/Int/Defs.lean
index c412cb212fefe9..7d035c9945ced4 100644
--- a/Mathlib/Algebra/Group/Int/Defs.lean
+++ b/Mathlib/Algebra/Group/Int/Defs.lean
@@ -47,8 +47,8 @@ instance instAddCommGroup : AddCommGroup ℤ where
   zsmul := (· * ·)
   zsmul_zero' := Int.zero_mul
   zsmul_succ' m n := by
-    simp only [natCast_succ, Int.add_mul, Int.add_comm, Int.one_mul]
-  zsmul_neg' m n := by simp only [negSucc_eq, natCast_succ, Int.neg_mul]
+    simp only [HSMul.hSMul, SMul.smul, natCast_succ, Int.add_mul, Int.add_comm, Int.one_mul]
+  zsmul_neg' m n := by simp only [HSMul.hSMul, SMul.smul, negSucc_eq, natCast_succ, Int.neg_mul]
   sub_eq_add_neg _ _ := Int.sub_eq_add_neg
 
 -- This instance can also be found from the `LinearOrderedCommMonoidWithZero ℤ` instance by
diff --git a/Mathlib/Algebra/Group/Opposite.lean b/Mathlib/Algebra/Group/Opposite.lean
index 93209d10f7fa4c..10dd573bb05bbe 100644
--- a/Mathlib/Algebra/Group/Opposite.lean
+++ b/Mathlib/Algebra/Group/Opposite.lean
@@ -142,6 +142,7 @@ instance instDivInvMonoid [DivInvMonoid α] : DivInvMonoid αᵐᵒᵖ where
   zpow n a := op <| a.unop ^ n
   zpow_zero' _ := unop_injective <| zpow_zero _
   zpow_succ' _ _ := unop_injective <| by
+    simp_rw [HPow.hPow, Pow.pow]
     rw [unop_op, zpow_natCast, pow_succ', unop_mul, unop_op, zpow_natCast]
   zpow_neg' _ _ := unop_injective <| DivInvMonoid.zpow_neg' _ _
 
diff --git a/Mathlib/Algebra/Group/Prod.lean b/Mathlib/Algebra/Group/Prod.lean
index 7b6de8812c6ba1..3182815a8420e5 100644
--- a/Mathlib/Algebra/Group/Prod.lean
+++ b/Mathlib/Algebra/Group/Prod.lean
@@ -79,7 +79,7 @@ instance instMulOneClass [MulOneClass M] [MulOneClass N] : MulOneClass (M × N)
 
 @[to_additive]
 instance instMonoid [Monoid M] [Monoid N] : Monoid (M × N) :=
-  { npow := fun z a => ⟨Monoid.npow z a.1, Monoid.npow z a.2⟩,
+  { npow := fun z a => ⟨NPow.npow z a.1, NPow.npow z a.2⟩,
     npow_zero := fun _ => Prod.ext (Monoid.npow_zero _) (Monoid.npow_zero _),
     npow_succ := fun _ _ => Prod.ext (Monoid.npow_succ _ _) (Monoid.npow_succ _ _),
     one_mul := by simp,
@@ -94,7 +94,7 @@ instance instIsMulTorsionFree [Monoid M] [Monoid N] [IsMulTorsionFree M] [IsMulT
 @[to_additive Prod.subNegMonoid]
 instance [DivInvMonoid G] [DivInvMonoid H] : DivInvMonoid (G × H) where
   div_eq_mul_inv _ _ := by ext <;> exact div_eq_mul_inv ..
-  zpow z a := ⟨DivInvMonoid.zpow z a.1, DivInvMonoid.zpow z a.2⟩
+  zpow z a := ⟨ZPow.zpow z a.1, ZPow.zpow z a.2⟩
   zpow_zero' _ := by ext <;> exact DivInvMonoid.zpow_zero' _
   zpow_succ' _ _ := by ext <;> exact DivInvMonoid.zpow_succ' ..
   zpow_neg' _ _ := by ext <;> exact DivInvMonoid.zpow_neg' ..
diff --git a/Mathlib/Algebra/Group/Submonoid/Membership.lean b/Mathlib/Algebra/Group/Submonoid/Membership.lean
index bcc6536f60a1c7..dc59293e5fb8b4 100644
--- a/Mathlib/Algebra/Group/Submonoid/Membership.lean
+++ b/Mathlib/Algebra/Group/Submonoid/Membership.lean
@@ -354,8 +354,12 @@ abbrev groupPowers {x : M} {n : ℕ} (hpos : 0 < n) (hx : x ^ n = 1) : Group (po
     simp only [coe_one, coe_mul, SubmonoidClass.coe_pow]
     rw [← pow_succ, Nat.sub_add_cancel hpos, ← pow_mul, mul_comm, pow_mul, hx, one_pow]
   zpow z x := x ^ z.natMod n
-  zpow_zero' z := by simp only [Int.natMod, Int.zero_emod, Int.toNat_zero, pow_zero]
-  zpow_neg' m x := Subtype.ext <| by
+  zpow_zero' z := by
+    simp_rw [HPow.hPow, Pow.pow]
+    simp only [Int.natMod, Int.zero_emod, Int.toNat_zero, pow_zero]
+  zpow_neg' m x := by
+    change x ^ (Int.natMod _ n) = (x ^ (Int.natMod _ n)) ^ (n - 1)
+    ext
     obtain ⟨_, k, rfl⟩ := x
     simp only [← pow_mul, Int.natMod, SubmonoidClass.coe_pow]
     rw [Int.negSucc_eq, ← Int.natCast_succ, ← Int.add_mul_emod_self_right (b := (m + 1 : ℕ))]
@@ -365,6 +369,7 @@ abbrev groupPowers {x : M} {n : ℕ} (hpos : 0 < n) (hx : x ^ n = 1) : Group (po
     rw [mul_comm, pow_mul, ← pow_eq_pow_mod _ hx, mul_comm k, mul_assoc, pow_mul _ (_ % _),
       ← pow_eq_pow_mod _ hx, pow_mul, pow_mul]
   zpow_succ' m x := Subtype.ext <| by
+    simp_rw [HPow.hPow, Pow.pow]
     obtain ⟨_, k, rfl⟩ := x
     simp only [← pow_mul, Int.natMod, SubmonoidClass.coe_pow, coe_mul]
     norm_cast
diff --git a/Mathlib/Algebra/Group/TypeTags/Basic.lean b/Mathlib/Algebra/Group/TypeTags/Basic.lean
index 07c87018aaf344..a07b3ee9363195 100644
--- a/Mathlib/Algebra/Group/TypeTags/Basic.lean
+++ b/Mathlib/Algebra/Group/TypeTags/Basic.lean
@@ -261,17 +261,15 @@ instance Multiplicative.mulOneClass [AddZeroClass α] : MulOneClass (Multiplicat
   one_mul := @zero_add α _
   mul_one := @add_zero α _
 
-instance Additive.addMonoid [h : Monoid α] : AddMonoid (Additive α) :=
-  { Additive.addZeroClass, Additive.addSemigroup with
-    nsmul := @Monoid.npow α h
-    nsmul_zero := @Monoid.npow_zero α h
-    nsmul_succ := @Monoid.npow_succ α h }
+instance Additive.addMonoid [h : Monoid α] : AddMonoid (Additive α) where
+  nsmul := h.npow
+  nsmul_zero := h.npow_zero
+  nsmul_succ := h.npow_succ
 
-instance Multiplicative.monoid [h : AddMonoid α] : Monoid (Multiplicative α) :=
-  { Multiplicative.mulOneClass, Multiplicative.semigroup with
-    npow := @AddMonoid.nsmul α h
-    npow_zero := @AddMonoid.nsmul_zero α h
-    npow_succ := @AddMonoid.nsmul_succ α h }
+instance Multiplicative.monoid [h : AddMonoid α] : Monoid (Multiplicative α) where
+  npow := h.nsmul
+  npow_zero := h.nsmul_zero
+  npow_succ := h.nsmul_succ
 
 @[simp]
 theorem ofMul_pow [Monoid α] (n : ℕ) (a : α) : ofMul (a ^ n) = n • ofMul a :=
@@ -415,21 +413,19 @@ instance Additive.involutiveNeg [InvolutiveInv α] : InvolutiveNeg (Additive α)
 instance Multiplicative.involutiveInv [InvolutiveNeg α] : InvolutiveInv (Multiplicative α) :=
   { Multiplicative.inv with inv_inv := @neg_neg α _ }
 
-instance Additive.subNegMonoid [DivInvMonoid α] : SubNegMonoid (Additive α) :=
-  { Additive.neg, Additive.sub, Additive.addMonoid with
-    sub_eq_add_neg := @div_eq_mul_inv α _
-    zsmul := @DivInvMonoid.zpow α _
-    zsmul_zero' := @DivInvMonoid.zpow_zero' α _
-    zsmul_succ' := @DivInvMonoid.zpow_succ' α _
-    zsmul_neg' := @DivInvMonoid.zpow_neg' α _ }
-
-instance Multiplicative.divInvMonoid [SubNegMonoid α] : DivInvMonoid (Multiplicative α) :=
-  { Multiplicative.inv, Multiplicative.div, Multiplicative.monoid with
-    div_eq_mul_inv := @sub_eq_add_neg α _
-    zpow := @SubNegMonoid.zsmul α _
-    zpow_zero' := @SubNegMonoid.zsmul_zero' α _
-    zpow_succ' := @SubNegMonoid.zsmul_succ' α _
-    zpow_neg' := @SubNegMonoid.zsmul_neg' α _ }
+instance Additive.subNegMonoid [h : DivInvMonoid α] : SubNegMonoid (Additive α) where
+  sub_eq_add_neg := h.div_eq_mul_inv
+  zsmul := h.zpow
+  zsmul_zero' := h.zpow_zero'
+  zsmul_succ' := h.zpow_succ'
+  zsmul_neg' := h.zpow_neg'
+
+instance Multiplicative.divInvMonoid [h : SubNegMonoid α] : DivInvMonoid (Multiplicative α) where
+  div_eq_mul_inv := h.sub_eq_add_neg
+  zpow := h.zsmul
+  zpow_zero' := h.zsmul_zero'
+  zpow_succ' := h.zsmul_succ'
+  zpow_neg' := h.zsmul_neg'
 
 @[simp]
 theorem ofMul_zpow [DivInvMonoid α] (z : ℤ) (a : α) : ofMul (a ^ z) = z • ofMul a :=
diff --git a/Mathlib/Algebra/Group/Units/Defs.lean b/Mathlib/Algebra/Group/Units/Defs.lean
index 977d47af6bbe98..31d9bd54c577d5 100644
--- a/Mathlib/Algebra/Group/Units/Defs.lean
+++ b/Mathlib/Algebra/Group/Units/Defs.lean
@@ -233,8 +233,8 @@ instance instMonoid : Monoid αˣ :=
         inv := a⁻¹ ^ n
         val_inv := by rw [← a.commute_coe_inv.mul_pow]; simp
         inv_val := by rw [← a.commute_inv_coe.mul_pow]; simp }
-    npow_zero := fun a ↦ by ext; simp
-    npow_succ := fun n a ↦ by ext; simp [pow_succ] }
+    npow_zero := fun a ↦ by simp only [HPow.hPow, Pow.pow]; ext; simp
+    npow_succ := fun n a ↦ by simp only [HPow.hPow, Pow.pow]; ext; simp [pow_succ] }
 
 /-- Units of a monoid have division -/
 @[to_additive /-- Additive units of an additive monoid have subtraction. -/]
@@ -251,9 +251,9 @@ instance instDivInvMonoid : DivInvMonoid αˣ where
   zpow := fun n a ↦ match n, a with
     | Int.ofNat n, a => a ^ n
     | Int.negSucc n, a => (a ^ n.succ)⁻¹
-  zpow_zero' := fun a ↦ by simp
-  zpow_succ' := fun n a ↦ by simp [pow_succ]
-  zpow_neg' := fun n a ↦ by simp
+  zpow_zero' := fun a ↦ by simp only [HPow.hPow, Pow.pow]; simp
+  zpow_succ' := fun n a ↦ by simp only [HPow.hPow, Pow.pow]; simp [pow_succ]
+  zpow_neg' := fun n a ↦ rfl
 
 /-- Units of a monoid form a group. -/
 @[to_additive /-- Additive units of an additive monoid form an additive group. -/]
diff --git a/Mathlib/Algebra/GroupWithZero/Action/Opposite.lean b/Mathlib/Algebra/GroupWithZero/Action/Opposite.lean
index 7fafdc6ad3ec1e..de0b0b6458cb3d 100644
--- a/Mathlib/Algebra/GroupWithZero/Action/Opposite.lean
+++ b/Mathlib/Algebra/GroupWithZero/Action/Opposite.lean
@@ -17,7 +17,7 @@ This file defines the actions on the opposite type `SMul R Mᵐᵒᵖ`, and acti
 type, `SMul Rᵐᵒᵖ M`.
 
 Note that `MulOpposite.smul` is provided in an earlier file as it is needed to
-provide the `AddMonoid.nsmul` and `AddCommGroup.zsmul` fields.
+provide the `NSMul.nsmul` and `AddCommGroup.zsmul` fields.
 
 ## Notation
 
diff --git a/Mathlib/Algebra/Module/NatInt.lean b/Mathlib/Algebra/Module/NatInt.lean
index 3ef0af81898905..09edacce30fa38 100644
--- a/Mathlib/Algebra/Module/NatInt.lean
+++ b/Mathlib/Algebra/Module/NatInt.lean
@@ -90,17 +90,18 @@ variable (R) in
 structure.
 See note [reducible non-instances]. -/
 abbrev Module.addCommMonoidToAddCommGroup
-    [Ring R] [AddCommMonoid M] [Module R M] : AddCommGroup M :=
-  { (inferInstance : AddCommMonoid M) with
-    neg := fun a => (-1 : R) • a
-    neg_add_cancel := fun a =>
-      show (-1 : R) • a + a = 0 by
-        nth_rw 2 [← one_smul R a]
-        rw [← add_smul, neg_add_cancel, zero_smul]
-    zsmul := fun z a => (z : R) • a
-    zsmul_zero' := fun a => by simpa only [Int.cast_zero] using zero_smul R a
-    zsmul_succ' := fun z a => by simp [add_comm, add_smul]
-    zsmul_neg' := fun z a => by simp [← smul_assoc] }
+    [Ring R] [AddCommMonoid M] [Module R M] : AddCommGroup M where
+  neg := fun a => (-1 : R) • a
+  neg_add_cancel := fun a =>
+    show (-1 : R) • a + a = 0 by
+      nth_rw 2 [← one_smul R a]
+      rw [← add_smul, neg_add_cancel, zero_smul]
+  zsmul z a := (z : R) • a
+  zsmul_zero' a := by simp_rw [HSMul.hSMul, SMul.smul, Int.cast_zero]; exact zero_smul R a
+  zsmul_succ' z a := by simp_rw [HSMul.hSMul, SMul.smul]; simp [add_comm, add_smul]
+  zsmul_neg' z a := by
+    change (Int.negSucc z : R) • a = -1 • ((z.succ : ℤ) : R) • a
+    simp [← smul_assoc]
 
 section AddCommMonoid
 
diff --git a/Mathlib/Algebra/MonoidAlgebra/Defs.lean b/Mathlib/Algebra/MonoidAlgebra/Defs.lean
index 937a70cab75586..7e856a420eb160 100644
--- a/Mathlib/Algebra/MonoidAlgebra/Defs.lean
+++ b/Mathlib/Algebra/MonoidAlgebra/Defs.lean
@@ -156,9 +156,12 @@ lemma ofCoeff_inj {x y : M →₀ R} : ofCoeff x = ofCoeff y ↔ x = y := ofCoef
   inferInstanceAs <| DecidableEq <| M →₀ R
 
 -- TODO: this instance abuses definitional equality with `Finsupp.mapRange`
+@[to_additive (dont_translate := A)]
+instance {A : Type*} [SMulZeroClass A R] : SMul A R[M] where
+  smul a x := x.mapRange (a • ·) (smul_zero _)
+
 @[to_additive] instance addCommMonoid : AddCommMonoid R[M] :=
-  fast_instance% { (inferInstance : AddCommMonoid <| M →₀ R) with
-    nsmul n x := x.mapRange (n • ·) (smul_zero _) }
+  inferInstanceAs <| AddCommMonoid <| M →₀ R
 
 @[to_additive] instance instIsCancelAdd [IsCancelAdd R] : IsCancelAdd R[M] :=
   inferInstanceAs <| IsCancelAdd <| M →₀ R
@@ -260,15 +263,13 @@ Further results on scalar multiplication can be found in
 
 variable {A : Type*} [SMulZeroClass A R]
 
--- TODO: this instance abuses definitional equality with `Finsupp.mapRange`
 @[to_additive (dont_translate := A) smulZeroClass]
 instance smulZeroClass : SMulZeroClass A R[M] :=
-  fast_instance% { (inferInstance : SMulZeroClass A (M →₀ R)) with
-    smul a x := x.mapRange (a • ·) (smul_zero _) }
+  inferInstanceAs <| SMulZeroClass A (M →₀ R)
 
 section
 -- Ensure that the different smul instances do not create a diamond.
-example : (smulZeroClass (A := ℕ) (R := R) (M := M)).toSMul = addCommMonoid.toNSMul := by
+example : (smulZeroClass (A := ℕ) (R := R) (M := M)).toSMul = addCommMonoid.toSMul := by
   with_reducible_and_instances rfl
 
 -- Ensure that smul has good defeq properties
diff --git a/Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean b/Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
index 95d6f49545ba63..a91c2dbf825867 100644
--- a/Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
+++ b/Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
@@ -260,8 +260,10 @@ instance addMonoid : AddMonoid (WithTop α) where
     | (a : α), n => ↑(n • a)
     | ⊤, 0 => 0
     | ⊤, _n + 1 => ⊤
-  nsmul_zero a := by cases a <;> simp [zero_nsmul]
-  nsmul_succ n a := by cases a <;> cases n <;> simp [succ_nsmul, coe_add]
+  nsmul_zero a := by simp_rw [HSMul.hSMul, SMul.smul]; cases a <;> simp [zero_nsmul]
+  nsmul_succ n a := by
+    simp_rw [HSMul.hSMul, SMul.smul]
+    cases a <;> cases n <;> simp [succ_nsmul, coe_add]
 
 @[simp, norm_cast] lemma coe_nsmul (a : α) (n : ℕ) : ↑(n • a) = n • (a : WithTop α) := rfl
 
diff --git a/Mathlib/Algebra/Order/Positive/Field.lean b/Mathlib/Algebra/Order/Positive/Field.lean
index 911c748941afc9..c7c266f7bb4ef7 100644
--- a/Mathlib/Algebra/Order/Positive/Field.lean
+++ b/Mathlib/Algebra/Order/Positive/Field.lean
@@ -35,8 +35,10 @@ instance : Pow { x : K // 0 < x } ℤ :=
 theorem coe_zpow (x : { x : K // 0 < x }) (n : ℤ) : ↑(x ^ n) = (x : K) ^ n :=
   rfl
 
-instance : CommGroup { x : K // 0 < x } :=
-  { Positive.commMonoid with
-    inv_mul_cancel := fun a => Subtype.ext <| inv_mul_cancel₀ a.2.ne' }
+instance : CommGroup { x : K // 0 < x } where
+  inv_mul_cancel a := Subtype.ext <| inv_mul_cancel₀ a.2.ne'
+  zpow_zero' x := Subtype.ext <| zpow_zero _
+  zpow_succ' n x := Subtype.ext <| DivInvMonoid.zpow_succ' _ _
+  zpow_neg' n x := Subtype.ext <| DivInvMonoid.zpow_neg' _ _
 
 end Positive
diff --git a/Mathlib/Algebra/Order/Ring/Archimedean.lean b/Mathlib/Algebra/Order/Ring/Archimedean.lean
index f85be72d328284..a422ab19ec5977 100644
--- a/Mathlib/Algebra/Order/Ring/Archimedean.lean
+++ b/Mathlib/Algebra/Order/Ring/Archimedean.lean
@@ -101,7 +101,6 @@ instance : AddCommMonoid (ArchimedeanClass R) where
   add_assoc := private add_assoc'
   zero_add := private zero_add'
   add_zero x := private add_comm x _ ▸ zero_add' x
-  nsmul n x := n • x
   nsmul_zero x := by induction x with | mk x => rw [← mk_pow, pow_zero, mk_one]
   nsmul_succ n x := by induction x with | mk x => rw [← mk_pow, pow_succ, mk_mul, mk_pow]
 
@@ -308,7 +307,6 @@ noncomputable instance : LinearOrderedAddCommGroupWithTop (ArchimedeanClass R) w
   add_neg_cancel_of_ne_top x h := by
     induction x with | mk x
     simp [← mk_inv, ← mk_mul, mul_inv_cancel₀ (mk_eq_top_iff.not.1 h)]
-  zsmul n x := n • x
   zsmul_zero' x := by induction x with | mk x => rw [← mk_zpow, zpow_zero, mk_one]
   zsmul_succ' := by exact zsmul_succ'
   zsmul_neg' n x := by
diff --git a/Mathlib/Algebra/Order/Ring/WithTop.lean b/Mathlib/Algebra/Order/Ring/WithTop.lean
index 6d665befaa45d7..f00c28d3bec3ee 100644
--- a/Mathlib/Algebra/Order/Ring/WithTop.lean
+++ b/Mathlib/Algebra/Order/Ring/WithTop.lean
@@ -173,8 +173,8 @@ instance instMonoidWithZero : MonoidWithZero (WithTop α) where
     | (a : α), n => ↑(a ^ n)
     | ⊤, 0 => 1
     | ⊤, _n + 1 => ⊤
-  npow_zero a := by cases a <;> simp
-  npow_succ n a := by cases n <;> cases a <;> simp [pow_succ]
+  npow_zero a := by simp_rw [HPow.hPow, Pow.pow]; cases a <;> simp
+  npow_succ n a := by simp_rw [HPow.hPow, Pow.pow]; cases n <;> cases a <;> simp [pow_succ]
 
 @[simp, norm_cast] lemma coe_pow (a : α) (n : ℕ) : (↑(a ^ n) : WithTop α) = a ^ n := rfl
 
diff --git a/Mathlib/Algebra/Ring/MinimalAxioms.lean b/Mathlib/Algebra/Ring/MinimalAxioms.lean
index 29e7416c385766..e405db78da4688 100644
--- a/Mathlib/Algebra/Ring/MinimalAxioms.lean
+++ b/Mathlib/Algebra/Ring/MinimalAxioms.lean
@@ -69,8 +69,7 @@ abbrev Ring.ofMinimalAxioms {R : Type u}
     mul_assoc := mul_assoc
     one_mul := one_mul
     mul_one := mul_one
-    neg_add_cancel := neg_add_cancel
-    zsmul := (· • ·) }
+    neg_add_cancel := neg_add_cancel }
 
 /-- Define a `CommRing` structure on a Type by proving a minimized set of axioms.
 Note that this uses the default definitions for `npow`, `nsmul`, `zsmul` and `sub`
diff --git a/Mathlib/Algebra/RingQuot.lean b/Mathlib/Algebra/RingQuot.lean
index 1cc20547c57ba4..741769569e35ba 100644
--- a/Mathlib/Algebra/RingQuot.lean
+++ b/Mathlib/Algebra/RingQuot.lean
@@ -302,7 +302,6 @@ instance instRing {R : Type uR} [Ring R] (r : R → R → Prop) : Ring (RingQuot
   sub_eq_add_neg := by
     rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩
     simp [neg_quot, sub_quot, add_quot, sub_eq_add_neg]
-  zsmul := (· • ·)
   zsmul_zero' := by
     rintro ⟨⟨⟩⟩
     simp [smul_quot, ← zero_quot]
diff --git a/Mathlib/CategoryTheory/Preadditive/EilenbergMoore.lean b/Mathlib/CategoryTheory/Preadditive/EilenbergMoore.lean
index df97c18ee5a1b5..cfc0db8619eedf 100644
--- a/Mathlib/CategoryTheory/Preadditive/EilenbergMoore.lean
+++ b/Mathlib/CategoryTheory/Preadditive/EilenbergMoore.lean
@@ -51,59 +51,19 @@ instance Monad.algebraPreadditive : Preadditive (Monad.Algebra T) where
       zsmul := fun r α =>
         { f := r • α.f
           h := by rw [Functor.map_zsmul, zsmul_comp, Monad.Algebra.Hom.h, comp_zsmul] }
-      add_assoc := by
-        intros
-        ext
-        apply add_assoc
-      zero_add := by
-        intros
-        ext
-        apply zero_add
-      add_zero := by
-        intros
-        ext
-        apply add_zero
-      nsmul_zero := by
-        intros
-        ext
-        apply zero_smul
-      nsmul_succ := by
-        intros
-        ext
-        apply succ_nsmul
-      sub_eq_add_neg := by
-        intros
-        ext
-        apply sub_eq_add_neg
-      zsmul_zero' := by
-        intros
-        ext
-        apply zero_smul
-      zsmul_succ' := by
-        intros
-        ext
-        simp only [natCast_zsmul, succ_nsmul]
-        rfl
-      zsmul_neg' := by
-        intros
-        ext
-        simp only [negSucc_zsmul, ← Nat.cast_smul_eq_nsmul ℤ]
-      neg_add_cancel := by
-        intros
-        ext
-        apply neg_add_cancel
-      add_comm := by
-        intros
-        ext
-        apply add_comm }
-  add_comp := by
-    intros
-    ext
-    apply add_comp
-  comp_add := by
-    intros
-    ext
-    apply comp_add
+      add_assoc _ _ _ := Algebra.Hom.ext <| add_assoc _ _ _
+      zero_add _ := Algebra.Hom.ext <| zero_add _
+      add_zero _ := Algebra.Hom.ext <| add_zero _
+      nsmul_zero _ := Algebra.Hom.ext <| zero_nsmul _
+      nsmul_succ _ _ := Algebra.Hom.ext <| succ_nsmul _ _
+      sub_eq_add_neg _ _ := Algebra.Hom.ext <| sub_eq_add_neg _ _
+      zsmul_zero' _ := Algebra.Hom.ext <| zero_zsmul _
+      zsmul_succ' _ _ := Algebra.Hom.ext <| SubNegMonoid.zsmul_succ' _ _
+      zsmul_neg' _ _ := Algebra.Hom.ext <| SubNegMonoid.zsmul_neg' _ _
+      neg_add_cancel _ := Algebra.Hom.ext <| neg_add_cancel _
+      add_comm _ _ := Algebra.Hom.ext <| add_comm _ _ }
+  add_comp _ _ _ _ _ _ := Algebra.Hom.ext <| add_comp _ _ _ _ _ _
+  comp_add _ _ _ _ _ _ := Algebra.Hom.ext <| comp_add _ _ _ _ _ _
 
 instance Monad.forget_additive : (Monad.forget T).Additive where
 
@@ -131,59 +91,19 @@ instance Comonad.coalgebraPreadditive : Preadditive (Comonad.Coalgebra U) where
       zsmul := fun r α =>
         { f := r • α.f
           h := by rw [Functor.map_zsmul, comp_zsmul, Comonad.Coalgebra.Hom.h, zsmul_comp] }
-      add_assoc := by
-        intros
-        ext
-        apply add_assoc
-      zero_add := by
-        intros
-        ext
-        apply zero_add
-      add_zero := by
-        intros
-        ext
-        apply add_zero
-      nsmul_zero := by
-        intros
-        ext
-        apply zero_smul
-      nsmul_succ := by
-        intros
-        ext
-        apply succ_nsmul
-      sub_eq_add_neg := by
-        intros
-        ext
-        apply sub_eq_add_neg
-      zsmul_zero' := by
-        intros
-        ext
-        apply zero_smul
-      zsmul_succ' := by
-        intros
-        ext
-        simp only [natCast_zsmul, succ_nsmul]
-        rfl
-      zsmul_neg' := by
-        intros
-        ext
-        simp only [negSucc_zsmul, ← Nat.cast_smul_eq_nsmul ℤ]
-      neg_add_cancel := by
-        intros
-        ext
-        apply neg_add_cancel
-      add_comm := by
-        intros
-        ext
-        apply add_comm }
-  add_comp := by
-    intros
-    ext
-    apply add_comp
-  comp_add := by
-    intros
-    ext
-    apply comp_add
+      add_assoc _ _ _ := Coalgebra.Hom.ext <| add_assoc _ _ _
+      zero_add _ := Coalgebra.Hom.ext <| zero_add _
+      add_zero _ := Coalgebra.Hom.ext <| add_zero _
+      nsmul_zero _ := Coalgebra.Hom.ext <| zero_nsmul _
+      nsmul_succ _ _ := Coalgebra.Hom.ext <| succ_nsmul _ _
+      sub_eq_add_neg _ _ := Coalgebra.Hom.ext <| sub_eq_add_neg _ _
+      zsmul_zero' _ := Coalgebra.Hom.ext <| zero_zsmul _
+      zsmul_succ' _ _ := Coalgebra.Hom.ext <| SubNegMonoid.zsmul_succ' _ _
+      zsmul_neg' _ _ := Coalgebra.Hom.ext <| SubNegMonoid.zsmul_neg' _ _
+      neg_add_cancel _ := Coalgebra.Hom.ext <| neg_add_cancel _
+      add_comm _ _ := Coalgebra.Hom.ext <| add_comm _ _ }
+  add_comp _ _ _ _ _ _ := Coalgebra.Hom.ext <| add_comp _ _ _ _ _ _
+  comp_add _ _ _ _ _ _ := Coalgebra.Hom.ext <| comp_add _ _ _ _ _ _
 
 instance Comonad.forget_additive : (Comonad.forget U).Additive where
 
diff --git a/Mathlib/CategoryTheory/Preadditive/EndoFunctor.lean b/Mathlib/CategoryTheory/Preadditive/EndoFunctor.lean
index 8023be602238e5..a5525c5405a122 100644
--- a/Mathlib/CategoryTheory/Preadditive/EndoFunctor.lean
+++ b/Mathlib/CategoryTheory/Preadditive/EndoFunctor.lean
@@ -51,59 +51,19 @@ instance Endofunctor.algebraPreadditive : Preadditive (Endofunctor.Algebra F) wh
       zsmul := fun r α =>
         { f := r • α.f
           h := by rw [comp_zsmul, Functor.map_zsmul, zsmul_comp, Endofunctor.Algebra.Hom.h] }
-      add_assoc := by
-        intros
-        apply Algebra.Hom.ext
-        apply add_assoc
-      zero_add := by
-        intros
-        apply Algebra.Hom.ext
-        apply zero_add
-      add_zero := by
-        intros
-        apply Algebra.Hom.ext
-        apply add_zero
-      nsmul_zero := by
-        intros
-        apply Algebra.Hom.ext
-        apply zero_smul
-      nsmul_succ := by
-        intros
-        apply Algebra.Hom.ext
-        apply succ_nsmul
-      sub_eq_add_neg := by
-        intros
-        apply Algebra.Hom.ext
-        apply sub_eq_add_neg
-      zsmul_zero' := by
-        intros
-        apply Algebra.Hom.ext
-        apply zero_smul
-      zsmul_succ' := by
-        intros
-        apply Algebra.Hom.ext
-        simp only [natCast_zsmul, succ_nsmul]
-        rfl
-      zsmul_neg' := by
-        intros
-        apply Algebra.Hom.ext
-        simp only [negSucc_zsmul, ← Nat.cast_smul_eq_nsmul ℤ]
-      neg_add_cancel := by
-        intros
-        apply Algebra.Hom.ext
-        apply neg_add_cancel
-      add_comm := by
-        intros
-        apply Algebra.Hom.ext
-        apply add_comm }
-  add_comp := by
-    intros
-    apply Algebra.Hom.ext
-    apply add_comp
-  comp_add := by
-    intros
-    apply Algebra.Hom.ext
-    apply comp_add
+      add_assoc _ _ _ := Algebra.Hom.ext <| add_assoc _ _ _
+      zero_add _ := Algebra.Hom.ext <| zero_add _
+      add_zero _ := Algebra.Hom.ext <| add_zero _
+      nsmul_zero _ := Algebra.Hom.ext <| zero_nsmul _
+      nsmul_succ _ _ := Algebra.Hom.ext <| succ_nsmul _ _
+      sub_eq_add_neg _ _ := Algebra.Hom.ext <| sub_eq_add_neg _ _
+      zsmul_zero' _ := Algebra.Hom.ext <| zero_zsmul _
+      zsmul_succ' _ _ := Algebra.Hom.ext <| SubNegMonoid.zsmul_succ' _ _
+      zsmul_neg' _ _ := Algebra.Hom.ext <| SubNegMonoid.zsmul_neg' _ _
+      neg_add_cancel _ := Algebra.Hom.ext <| neg_add_cancel _
+      add_comm _ _ :=  Algebra.Hom.ext <| add_comm _ _ }
+  add_comp _ _ _ _ _ _ := Algebra.Hom.ext <| add_comp _ _ _ _ _ _
+  comp_add _ _ _ _ _ _ := Algebra.Hom.ext <| comp_add _ _ _ _ _ _
 
 instance Algebra.forget_additive : (Endofunctor.Algebra.forget F).Additive where
 
@@ -128,59 +88,19 @@ instance Endofunctor.coalgebraPreadditive : Preadditive (Endofunctor.Coalgebra F
       zsmul := fun r α =>
         { f := r • α.f
           h := by rw [Functor.map_zsmul, comp_zsmul, Endofunctor.Coalgebra.Hom.h, zsmul_comp] }
-      add_assoc := by
-        intros
-        apply Coalgebra.Hom.ext
-        apply add_assoc
-      zero_add := by
-        intros
-        apply Coalgebra.Hom.ext
-        apply zero_add
-      add_zero := by
-        intros
-        apply Coalgebra.Hom.ext
-        apply add_zero
-      nsmul_zero := by
-        intros
-        apply Coalgebra.Hom.ext
-        apply zero_smul
-      nsmul_succ := by
-        intros
-        apply Coalgebra.Hom.ext
-        apply succ_nsmul
-      sub_eq_add_neg := by
-        intros
-        apply Coalgebra.Hom.ext
-        apply sub_eq_add_neg
-      zsmul_zero' := by
-        intros
-        apply Coalgebra.Hom.ext
-        apply zero_smul
-      zsmul_succ' := by
-        intros
-        apply Coalgebra.Hom.ext
-        simp only [natCast_zsmul, succ_nsmul]
-        rfl
-      zsmul_neg' := by
-        intros
-        apply Coalgebra.Hom.ext
-        simp only [negSucc_zsmul, ← Nat.cast_smul_eq_nsmul ℤ]
-      neg_add_cancel := by
-        intros
-        apply Coalgebra.Hom.ext
-        apply neg_add_cancel
-      add_comm := by
-        intros
-        apply Coalgebra.Hom.ext
-        apply add_comm }
-  add_comp := by
-    intros
-    apply Coalgebra.Hom.ext
-    apply add_comp
-  comp_add := by
-    intros
-    apply Coalgebra.Hom.ext
-    apply comp_add
+      add_assoc _ _ _ := Coalgebra.Hom.ext <| add_assoc _ _ _
+      zero_add _ := Coalgebra.Hom.ext <| zero_add _
+      add_zero _ := Coalgebra.Hom.ext <| add_zero _
+      nsmul_zero _ := Coalgebra.Hom.ext <| zero_nsmul _
+      nsmul_succ _ _ := Coalgebra.Hom.ext <| succ_nsmul _ _
+      sub_eq_add_neg _ _ := Coalgebra.Hom.ext <| sub_eq_add_neg _ _
+      zsmul_zero' _ := Coalgebra.Hom.ext <| zero_zsmul _
+      zsmul_succ' _ _ := Coalgebra.Hom.ext <| SubNegMonoid.zsmul_succ' _ _
+      zsmul_neg' _ _ := Coalgebra.Hom.ext <| SubNegMonoid.zsmul_neg' _ _
+      neg_add_cancel _ := Coalgebra.Hom.ext <| neg_add_cancel _
+      add_comm _ _ := Coalgebra.Hom.ext <| add_comm _ _ }
+  add_comp _ _ _ _ _ _ := Coalgebra.Hom.ext <| add_comp _ _ _ _ _ _
+  comp_add _ _ _ _ _ _ := Coalgebra.Hom.ext <| comp_add _ _ _ _ _ _
 
 instance Coalgebra.forget_additive : (Endofunctor.Coalgebra.forget F).Additive where
 
diff --git a/Mathlib/CategoryTheory/Triangulated/Basic.lean b/Mathlib/CategoryTheory/Triangulated/Basic.lean
index 39faa86c2eeb1f..ac60e76a655830 100644
--- a/Mathlib/CategoryTheory/Triangulated/Basic.lean
+++ b/Mathlib/CategoryTheory/Triangulated/Basic.lean
@@ -292,10 +292,8 @@ instance : AddCommGroup (T₁ ⟶ T₂) where
   add_comm f g := by ext <;> apply add_comm
   neg_add_cancel f := by ext <;> apply neg_add_cancel
   sub_eq_add_neg f g := by ext <;> apply sub_eq_add_neg
-  nsmul n f := n • f
   nsmul_zero f := by cat_disch
   nsmul_succ n f := by ext <;> apply AddMonoid.nsmul_succ
-  zsmul n f := n • f
   zsmul_zero' := by cat_disch
   zsmul_succ' n f := by ext <;> apply SubNegMonoid.zsmul_succ'
   zsmul_neg' n f := by ext <;> apply SubNegMonoid.zsmul_neg'
diff --git a/Mathlib/Data/BitVec.lean b/Mathlib/Data/BitVec.lean
index c76df5a6a66593..7e2da761f6c3bf 100644
--- a/Mathlib/Data/BitVec.lean
+++ b/Mathlib/Data/BitVec.lean
@@ -71,6 +71,7 @@ lemma toFin_zsmul (z : ℤ) (x : BitVec w) : toFin (z • x) = z • x.toFin :=
     open scoped Fin.CommRing in
     simp only [zsmul_eq_mul, toFin_intCast]
 
+set_option backward.isDefEq.respectTransparency false in
 lemma toFin_pow (x : BitVec w) (n : ℕ) : toFin (x ^ n) = x.toFin ^ n := by
   induction n with
   | zero => simp
@@ -81,7 +82,7 @@ lemma toFin_pow (x : BitVec w) (n : ℕ) : toFin (x ^ n) = x.toFin ^ n := by
 -/
 
 -- Verify that the `HPow` instance from Lean agrees definitionally with the instance via `Monoid`.
-example : @instHPow (Fin (2 ^ w)) ℕ Monoid.toPow = Lean.Grind.Fin.instHPowFinNatOfNeZero := rfl
+example : @instHPow (Fin (2 ^ w)) ℕ NPow.toPow = Lean.Grind.Fin.instHPowFinNatOfNeZero := rfl
 
 instance : CommSemiring (BitVec w) :=
   open Fin.CommRing in
diff --git a/Mathlib/Data/Complex/Basic.lean b/Mathlib/Data/Complex/Basic.lean
index 6efe95f1df5c42..62fed242e95685 100644
--- a/Mathlib/Data/Complex/Basic.lean
+++ b/Mathlib/Data/Complex/Basic.lean
@@ -322,8 +322,6 @@ theorem real_smul {x : ℝ} {z : ℂ} : x • z = x * z :=
 end SMul
 
 instance addCommGroup : AddCommGroup ℂ where
-  nsmul := (· • ·)
-  zsmul := (· • ·)
   zsmul_zero' := by intros; ext <;> simp [smul_re, smul_im]
   nsmul_zero := by intros; ext <;> simp [smul_re, smul_im]
   nsmul_succ := by intros; ext <;> simp [smul_re, smul_im] <;> ring
diff --git a/Mathlib/Data/Rat/Defs.lean b/Mathlib/Data/Rat/Defs.lean
index d40f487083ed05..d99d373b38caf7 100644
--- a/Mathlib/Data/Rat/Defs.lean
+++ b/Mathlib/Data/Rat/Defs.lean
@@ -167,8 +167,10 @@ instance addCommGroup : AddCommGroup ℚ where
     rw [Rat.intCast_add, Rat.add_mul, Rat.intCast_one, Rat.one_mul]
     rfl
   zsmul_zero' := Rat.zero_mul
-  zsmul_succ' _ _ := by simp [Rat.add_mul]
-  zsmul_neg' _ _ := by rw [Int.negSucc_eq, Rat.intCast_neg, Rat.neg_mul]; rfl
+  zsmul_succ' _ _ := by simp_rw [HSMul.hSMul, SMul.smul]; simp [Rat.add_mul]
+  zsmul_neg' _ _ := by
+    simp_rw [HSMul.hSMul, SMul.smul]
+    rw [Int.negSucc_eq, Rat.intCast_neg, Rat.neg_mul]; rfl
 
 instance addGroup : AddGroup ℚ := by infer_instance
 
diff --git a/Mathlib/Data/ZMod/Defs.lean b/Mathlib/Data/ZMod/Defs.lean
index 70625d7130ba48..87de9acc8b0073 100644
--- a/Mathlib/Data/ZMod/Defs.lean
+++ b/Mathlib/Data/ZMod/Defs.lean
@@ -65,17 +65,22 @@ open scoped Fin.IntCast Fin.NatCast
       lia
 
 /-- Multiplicative commutative semigroup structure on `Fin n`. -/
-instance instCommSemigroup (n : ℕ) : CommSemigroup (Fin n) :=
-  { (inferInstance : Mul (Fin n)) with
-    mul_assoc := fun ⟨a, _⟩ ⟨b, _⟩ ⟨c, _⟩ =>
-      Fin.eq_of_val_eq <|
-        calc
-          a * b % n * c ≡ a * b * c [MOD n] := (Nat.mod_modEq _ _).mul_right _
-          _ ≡ a * (b * c) [MOD n] := by rw [mul_assoc]
-          _ ≡ a * (b * c % n) [MOD n] := (Nat.mod_modEq _ _).symm.mul_left _
-    mul_comm := Fin.mul_comm }
-
-set_option backward.privateInPublic true in
+instance instCommSemigroup (n : ℕ) : CommSemigroup (Fin n) where
+  mul_assoc := fun ⟨a, _⟩ ⟨b, _⟩ ⟨c, _⟩ =>
+    Fin.eq_of_val_eq <|
+      calc
+        a * b % n * c ≡ a * b * c [MOD n] := (Nat.mod_modEq _ _).mul_right _
+        _ ≡ a * (b * c) [MOD n] := by rw [mul_assoc]
+        _ ≡ a * (b * c % n) [MOD n] := (Nat.mod_modEq _ _).symm.mul_left _
+  mul_comm := Fin.mul_comm
+
+-- Shortcut instances to replace the power operation on `Fin` with a more efficient one
+instance (n : ℕ) [NeZero n] : HPow (Fin n) ℕ (Fin n) where
+  hPow a m := npowRecAuto m a
+
+instance (n : ℕ) [NeZero n] : Pow (Fin n) ℕ where
+  pow a m := npowRecAuto m a
+
 private theorem left_distrib_aux (n : ℕ) : ∀ a b c : Fin n, a * (b + c) = a * b + a * c :=
   fun ⟨a, _⟩ ⟨b, _⟩ ⟨c, _⟩ =>
   Fin.eq_of_val_eq <|
@@ -84,19 +89,13 @@ private theorem left_distrib_aux (n : ℕ) : ∀ a b c : Fin n, a * (b + c) = a
       _ ≡ a * b + a * c [MOD n] := by rw [mul_add]
       _ ≡ a * b % n + a * c % n [MOD n] := (Nat.mod_modEq _ _).symm.add (Nat.mod_modEq _ _).symm
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 /-- Distributive structure on `Fin n`. -/
-instance instDistrib (n : ℕ) : Distrib (Fin n) :=
-  { Fin.addCommSemigroup n, Fin.instCommSemigroup n with
-    left_distrib := left_distrib_aux n
-    right_distrib := fun a b c => by
-      rw [mul_comm, left_distrib_aux, mul_comm _ b, mul_comm] }
+instance instDistrib (n : ℕ) : Distrib (Fin n) where
+  left_distrib := private left_distrib_aux n
+  right_distrib := fun a b c => by
+    rw [mul_comm, left_distrib_aux, mul_comm _ b, mul_comm]
 
 instance instNonUnitalCommRing (n : ℕ) [NeZero n] : NonUnitalCommRing (Fin n) where
-  __ := Fin.addCommGroup n
-  __ := Fin.instCommSemigroup n
-  __ := Fin.instDistrib n
   zero_mul := Fin.zero_mul
   mul_zero := Fin.mul_zero
 
@@ -106,7 +105,6 @@ instance instCommMonoid (n : ℕ) [NeZero n] : CommMonoid (Fin n) where
 
 /-- Note this is more general than `Fin.instCommRing` as it applies (vacuously) to `Fin 0` too. -/
 instance instHasDistribNeg (n : ℕ) : HasDistribNeg (Fin n) where
-  toInvolutiveNeg := Fin.instInvolutiveNeg n
   mul_neg := Nat.casesOn n finZeroElim fun _i => mul_neg
   neg_mul := Nat.casesOn n finZeroElim fun _i => neg_mul
 
@@ -126,11 +124,6 @@ silently introducing wraparound arithmetic.
 -/
 @[instance_reducible]
 def instCommRing (n : ℕ) [NeZero n] : CommRing (Fin n) where
-  __ := Fin.instAddMonoidWithOne n
-  __ := Fin.addCommGroup n
-  __ := Fin.instCommSemigroup n
-  __ := Fin.instNonUnitalCommRing n
-  __ := Fin.instCommMonoid n
   intCast n := Fin.intCast n
 
 namespace CommRing
diff --git a/Mathlib/Data/ZMod/IntUnitsPower.lean b/Mathlib/Data/ZMod/IntUnitsPower.lean
index 687842a20a1f6a..e341f184756521 100644
--- a/Mathlib/Data/ZMod/IntUnitsPower.lean
+++ b/Mathlib/Data/ZMod/IntUnitsPower.lean
@@ -65,8 +65,8 @@ instance Int.instUnitsPow : Pow ℤˣ R where
 
 -- The above instances form no typeclass diamonds with the standard power operators
 -- but we will need `reducible_and_instances` which currently fails https://github.com/leanprover-community/mathlib4/issues/10906
-example : Int.instUnitsPow = Monoid.toPow := rfl
-example : Int.instUnitsPow = DivInvMonoid.toZPow := rfl
+example : Int.instUnitsPow = NPow.toPow := rfl
+example : Int.instUnitsPow = ZPow.toPow := rfl
 
 @[simp] lemma ofMul_uzpow (u : ℤˣ) (r : R) : Additive.ofMul (u ^ r) = r • Additive.ofMul u := rfl
 
diff --git a/Mathlib/FieldTheory/RatFunc/Basic.lean b/Mathlib/FieldTheory/RatFunc/Basic.lean
index d2b112debb569c..cbeb97883b9817 100644
--- a/Mathlib/FieldTheory/RatFunc/Basic.lean
+++ b/Mathlib/FieldTheory/RatFunc/Basic.lean
@@ -288,10 +288,8 @@ def instAddCommGroup : AddCommGroup K⟮X⟯ where
   add_zero := by frac_tac
   neg_add_cancel := by frac_tac
   sub_eq_add_neg := by frac_tac
-  nsmul := (· • ·)
   nsmul_zero := by smul_tac
   nsmul_succ _ := by smul_tac
-  zsmul := (· • ·)
   zsmul_zero' := by smul_tac
   zsmul_succ' _ := by smul_tac
   zsmul_neg' _ := by smul_tac
diff --git a/Mathlib/GroupTheory/GroupAction/Hom.lean b/Mathlib/GroupTheory/GroupAction/Hom.lean
index f569f8bad2e5f9..e2f8b9611b1e31 100644
--- a/Mathlib/GroupTheory/GroupAction/Hom.lean
+++ b/Mathlib/GroupTheory/GroupAction/Hom.lean
@@ -448,7 +448,6 @@ lemma coe_add [SMul M X] [AddZeroClass Y] [DistribSMul N Y] (f g : X →ₑ[σ]
 instance [SMul M X] [AddMonoid Y] [DistribSMul N Y] :
     AddMonoid (X →ₑ[σ] Y) where
   add_assoc _ _ _ := ext fun _ ↦ add_assoc _ _ _
-  nsmul n f := n • f
   nsmul_zero f := ext fun x ↦ AddMonoid.nsmul_zero (f x)
   nsmul_succ n f := ext fun x ↦ AddMonoid.nsmul_succ n (f x)
 
@@ -484,7 +483,6 @@ instance [SMul M X] [AddGroup Y] [DistribSMul N Y] : AddGroup (X →ₑ[σ] Y) w
   neg f := ⟨-f, by simp⟩
   neg_add_cancel f := ext fun _ ↦ neg_add_cancel _
   sub_eq_add_neg _ _ := ext fun _ ↦ sub_eq_add_neg _ _
-  zsmul z f := z • f
   zsmul_zero' f := ext fun x ↦ SubNegMonoid.zsmul_zero' _
   zsmul_neg' _ _ := ext fun x ↦ SubNegMonoid.zsmul_neg' _ _
   zsmul_succ' _ _ := ext fun x ↦ SubNegMonoid.zsmul_succ' _ _
diff --git a/Mathlib/LinearAlgebra/Matrix/Defs.lean b/Mathlib/LinearAlgebra/Matrix/Defs.lean
index d554ac7a405bbd..618256a8f8057b 100644
--- a/Mathlib/LinearAlgebra/Matrix/Defs.lean
+++ b/Mathlib/LinearAlgebra/Matrix/Defs.lean
@@ -151,6 +151,9 @@ instance inhabited [Inhabited α] : Inhabited (Matrix m n α) :=
 instance add [Add α] : Add (Matrix m n α) :=
   inferInstanceAs <| Add (m → n → α)
 
+instance smul [SMul R α] : SMul R (Matrix m n α) where
+  smul a b := fun i ↦ a • b i
+
 instance addSemigroup [AddSemigroup α] : AddSemigroup (Matrix m n α) :=
   inferInstanceAs <| AddSemigroup (m → n → α)
 
@@ -163,9 +166,8 @@ instance zero [Zero α] : Zero (Matrix m n α) :=
 instance addZeroClass [AddZeroClass α] : AddZeroClass (Matrix m n α) :=
   inferInstanceAs <| AddZeroClass (m → n → α)
 
-instance addMonoid [AddMonoid α] : AddMonoid (Matrix m n α) where
-  __ : AddMonoid (Matrix m n α) := inferInstanceAs <| AddMonoid (m → n → α)
-  nsmul a b := fun i ↦ a • b i
+instance addMonoid [AddMonoid α] : AddMonoid (Matrix m n α) :=
+  inferInstanceAs <| AddMonoid (m → n → α)
 
 instance addCommMonoid [AddCommMonoid α] : AddCommMonoid (Matrix m n α) :=
   inferInstanceAs <| AddCommMonoid (m → n → α)
@@ -179,9 +181,8 @@ instance involutiveNeg [InvolutiveNeg α] : InvolutiveNeg (Matrix m n α) :=
 instance sub [Sub α] : Sub (Matrix m n α) :=
   inferInstanceAs <| Sub (m → n → α)
 
-instance addGroup [AddGroup α] : AddGroup (Matrix m n α) where
-  __ : AddGroup (Matrix m n α) := inferInstanceAs <| AddGroup (m → n → α)
-  zsmul a b := fun i ↦ a • b i
+instance addGroup [AddGroup α] : AddGroup (Matrix m n α) :=
+  inferInstanceAs <| AddGroup (m → n → α)
 
 instance addCommGroup [AddCommGroup α] : AddCommGroup (Matrix m n α) :=
   inferInstanceAs <| AddCommGroup (m → n → α)
@@ -195,9 +196,6 @@ instance subsingleton [Subsingleton α] : Subsingleton (Matrix m n α) :=
 instance nonempty [Nonempty m] [Nonempty n] [Nontrivial α] : Nontrivial (Matrix m n α) :=
   Function.nontrivial
 
-instance smul [SMul R α] : SMul R (Matrix m n α) where
-  smul a b := fun i ↦ a • b i
-
 instance smulCommClass [SMul R α] [SMul S α] [SMulCommClass R S α] :
     SMulCommClass R S (Matrix m n α) :=
   Pi.smulCommClass
diff --git a/Mathlib/LinearAlgebra/Matrix/ZPow.lean b/Mathlib/LinearAlgebra/Matrix/ZPow.lean
index bc46e0f48d750a..373668ea8afa87 100644
--- a/Mathlib/LinearAlgebra/Matrix/ZPow.lean
+++ b/Mathlib/LinearAlgebra/Matrix/ZPow.lean
@@ -97,8 +97,7 @@ theorem inv_zpow (A : M) : ∀ n : ℤ, A⁻¹ ^ n = (A ^ n)⁻¹
 
 @[simp]
 theorem zpow_neg_one (A : M) : A ^ (-1 : ℤ) = A⁻¹ := by
-  convert DivInvMonoid.zpow_neg' 0 A
-  simp only [zpow_one, Int.ofNat_zero, Int.natCast_succ, zpow_eq_pow, zero_add]
+  simpa using DivInvMonoid.zpow_neg' 0 A
 
 @[simp]
 theorem zpow_neg_natCast (A : M) (n : ℕ) : A ^ (-n : ℤ) = (A ^ n)⁻¹ := by
diff --git a/Mathlib/LinearAlgebra/TensorProduct/Basic.lean b/Mathlib/LinearAlgebra/TensorProduct/Basic.lean
index c9949b11f603e9..5d9729181e01ec 100644
--- a/Mathlib/LinearAlgebra/TensorProduct/Basic.lean
+++ b/Mathlib/LinearAlgebra/TensorProduct/Basic.lean
@@ -392,7 +392,6 @@ protected theorem neg_add_cancel (x : M ⊗[R] N) : -x + x = 0 :=
 
 instance addCommGroup : AddCommGroup (M ⊗[R] N) where
   neg_add_cancel := fun x => TensorProduct.neg_add_cancel x
-  zsmul := (· • ·)
   zsmul_zero' := by simp
   zsmul_succ' := by simp [add_comm, TensorProduct.add_smul]
   zsmul_neg' := fun n x => by
diff --git a/Mathlib/LinearAlgebra/TensorProduct/Defs.lean b/Mathlib/LinearAlgebra/TensorProduct/Defs.lean
index eab6b930372d89..e3cc046b46a814 100644
--- a/Mathlib/LinearAlgebra/TensorProduct/Defs.lean
+++ b/Mathlib/LinearAlgebra/TensorProduct/Defs.lean
@@ -224,7 +224,7 @@ Note that in the special case that `R = R'`, since `R` is commutative, we just g
 action on a tensor product of two modules. This special case is important enough that, for
 performance reasons, we define it explicitly below. -/
 instance leftHasSMul : SMul R' (M ⊗[R] N) :=
-  ⟨fun r =>
+  id ⟨fun r =>
     (addConGen (TensorProduct.Eqv R M N)).lift (SMul.aux r : _ →+ M ⊗[R] N) <|
       AddCon.addConGen_le fun x y hxy =>
         match x, y, hxy with
@@ -270,10 +270,8 @@ protected theorem add_smul (r s : R'') (x : M ⊗[R] N) : (r + s) • x = r •
     rw [ihx, ihy, add_add_add_comm]
 
 instance addMonoid : AddMonoid (M ⊗[R] N) where
-  nsmul := fun n v => n • v
   nsmul_zero := by simp [TensorProduct.zero_smul]
-  nsmul_succ := by simp only [TensorProduct.one_smul, TensorProduct.add_smul, add_comm,
-    forall_const]
+  nsmul_succ := by simp only [TensorProduct.one_smul, TensorProduct.add_smul, forall_const]
 
 instance addCommMonoid : AddCommMonoid (M ⊗[R] N) where
 
diff --git a/Mathlib/NumberTheory/ArithmeticFunction/Defs.lean b/Mathlib/NumberTheory/ArithmeticFunction/Defs.lean
index f7387bd07f224d..47590c9b6eb141 100644
--- a/Mathlib/NumberTheory/ArithmeticFunction/Defs.lean
+++ b/Mathlib/NumberTheory/ArithmeticFunction/Defs.lean
@@ -312,7 +312,6 @@ instance [CommSemiring R] : CommSemiring (ArithmeticFunction R) where
 instance [CommRing R] : CommRing (ArithmeticFunction R) where
   neg_add_cancel := neg_add_cancel
   mul_comm := mul_comm
-  zsmul n f := n • f
 
 instance {S : Type*} [Semiring R] [AddCommMonoid S] [Module R S] :
     Module R (ArithmeticFunction S) where
diff --git a/Mathlib/RingTheory/PolynomialLaw/Basic.lean b/Mathlib/RingTheory/PolynomialLaw/Basic.lean
index 428aacc7598da8..63015e49e8c219 100644
--- a/Mathlib/RingTheory/PolynomialLaw/Basic.lean
+++ b/Mathlib/RingTheory/PolynomialLaw/Basic.lean
@@ -165,8 +165,10 @@ instance : AddCommMonoid (M →ₚₗ[R] N) where
   zero_add f := by ext; simp only [add_def, zero_add, zero_def]
   add_zero f := by ext; simp only [add_def, add_zero, zero_def]
   nsmul n f := (n : R) • f
-  nsmul_zero f := by simp only [Nat.cast_zero, zero_smul f]
-  nsmul_succ n f := by simp only [Nat.cast_add, Nat.cast_one, add_smul, one_smul]
+  nsmul_zero f := by simp_rw [HSMul.hSMul, SMul.smul]; simp only [Nat.cast_zero, zero_smul f]
+  nsmul_succ n f := by
+    simp_rw [HSMul.hSMul, SMul.smul]
+    simp only [Nat.cast_add, Nat.cast_one, add_smul, one_smul]
   add_comm f g := by ext; simp only [add_def, add_comm]
 
 instance : Module R (M →ₚₗ[R] N) where
@@ -195,15 +197,17 @@ theorem neg_def (S : Type u) [CommSemiring S] [Algebra R S] :
 
 instance : AddCommGroup (M →ₚₗ[R] N) where
   zsmul n f := (n : R) • f
-  zsmul_zero' f := by simp only [Int.cast_zero, zero_smul]
-  zsmul_succ' n f := by simp only [Nat.cast_succ, Int.cast_add, Int.cast_natCast,
-    Int.cast_one, add_smul, _root_.one_smul]
+  zsmul_zero' f := by simp_rw [HSMul.hSMul, SMul.smul]; simp only [Int.cast_zero, zero_smul]
+  zsmul_succ' n f := by
+    simp_rw [HSMul.hSMul, SMul.smul]
+    simp only [Nat.cast_succ, Int.cast_add, Int.cast_natCast, Int.cast_one, add_smul, one_smul]
   zsmul_neg' n f := by
+    simp_rw [HSMul.hSMul, SMul.smul]
     ext S _ _ m
     rw [neg_def]
-    simp only [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev, _root_.add_smul,
+    simp only [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev, add_smul,
       add_def_apply, smul_def_apply, Nat.succ_eq_add_one, Int.cast_add, Int.cast_natCast,
-      Int.cast_one, _root_.one_smul, add_def, smul_def, Pi.smul_apply, Pi.add_apply, smul_add,
+      Int.cast_one, one_smul, add_def, smul_def, Pi.smul_apply, Pi.add_apply, smul_add,
       smul_smul, neg_mul, one_mul]
     rw [add_comm]
   neg_add_cancel f := by
diff --git a/Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean b/Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean
index 162e0f42544bc5..d7cca3d917b6ab 100644
--- a/Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean
+++ b/Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean
@@ -490,8 +490,8 @@ instance : CommMonoidWithZero (ValueGroupWithZero R) where
       simp only [pow_succ, ← ValueGroupWithZero.mk_mul_mk, ih]
       apply congrArg (_ * ·)
       exact ValueGroupWithZero.sound h₁ h₂
-  npow_zero := ValueGroupWithZero.ind (by simp)
-  npow_succ n := ValueGroupWithZero.ind (by simp [pow_succ])
+  npow_zero := ValueGroupWithZero.ind (by simp_rw [HPow.hPow, Pow.pow]; simp)
+  npow_succ n := ValueGroupWithZero.ind (by simp_rw [HPow.hPow, Pow.pow]; simp [pow_succ])
 
 instance : LE (ValueGroupWithZero R) where
   le := ValueGroupWithZero.lift₂ (fun a s b t => a * t ≤ᵥ b * s) <| by
diff --git a/Mathlib/SetTheory/Cardinal/Order.lean b/Mathlib/SetTheory/Cardinal/Order.lean
index a2f753c4748b1c..c1a5d6f551795c 100644
--- a/Mathlib/SetTheory/Cardinal/Order.lean
+++ b/Mathlib/SetTheory/Cardinal/Order.lean
@@ -231,7 +231,7 @@ instance commSemiring : CommSemiring Cardinal.{u} where
   nsmul := nsmulRec
   npow n c := c ^ (n : Cardinal)
   npow_zero := power_zero
-  npow_succ n c := by rw [cast_succ, power_add, power_one]
+  npow_succ n c := by simp_rw [HPow.hPow, Pow.pow]; rw [cast_succ, power_add, power_one]
   natCast n := lift #(Fin n)
   natCast_zero := rfl
   natCast_succ n := cast_succ n
diff --git a/Mathlib/Tactic/Abel.lean b/Mathlib/Tactic/Abel.lean
index 8a8d41b4dd45c6..ebff96bc3f676c 100644
--- a/Mathlib/Tactic/Abel.lean
+++ b/Mathlib/Tactic/Abel.lean
@@ -377,11 +377,11 @@ partial def eval (e : Expr) : M (NormalExpr × Expr) := do
     let (e₁, p₁) ← eval e
     let (e₂, p₂) ← evalNeg e₁
     return (e₂, ← iapp `Mathlib.Tactic.Abel.subst_into_neg #[e, e₁, e₂, p₁, p₂])
-  | (``AddMonoid.nsmul, #[_, _, e₁, e₂]) => do
+  | (``NSMul.nsmul, #[_, _, e₁, e₂]) => do
     let n ← if (← read).isGroup then mkAppM ``Int.ofNat #[e₁] else pure e₁
     let (e', p) ← eval <| ← iapp ``smul #[n, e₂]
     return (e', ← iapp ``unfold_smul #[e₁, e₂, e', p])
-  | (``SubNegMonoid.zsmul, #[_, _, e₁, e₂]) => do
+  | (``ZSMul.zsmul, #[_, _, e₁, e₂]) => do
       if ¬ (← read).isGroup then failure
       let (e', p) ← eval <| ← iapp ``smul #[e₁, e₂]
       return (e', (← read).app ``unfold_zsmul (← read).inst #[e₁, e₂, e', p])
@@ -411,8 +411,8 @@ def isAtom (e : Expr) : Bool :=
   | (``HAdd.hAdd, #[_, _, _, _, _, _])
   | (``HSub.hSub, #[_, _, _, _, _, _])
   | (``Neg.neg, #[_, _, _])
-  | (``AddMonoid.nsmul, #[_, _, _, _])
-  | (``SubNegMonoid.zsmul, #[_, _, _, _])
+  | (``NSMul.nsmul, #[_, _, _, _])
+  | (``ZSMul.zsmul, #[_, _, _, _])
   | (``SMul.smul, #[.const ``Int _, _, _, _, _])
   | (``SMul.smul, #[.const ``Nat _, _, _, _, _])
   | (``HSMul.hSMul, #[.const ``Int _, _, _, _, _, _])
diff --git a/Mathlib/Tactic/Translate/ToAdditive.lean b/Mathlib/Tactic/Translate/ToAdditive.lean
index 6eb7fc89e91954..152495d9256077 100644
--- a/Mathlib/Tactic/Translate/ToAdditive.lean
+++ b/Mathlib/Tactic/Translate/ToAdditive.lean
@@ -190,8 +190,8 @@ mismatch error.
   This likely only happens when the multiplicative declaration involves `pow`/`^`. Solutions:
   * Ensure that the order of arguments of all relevant declarations are the same for the
     multiplicative and additive version. This might mean that arguments have an "unnatural" order
-    (e.g. `Monoid.npow n x` corresponds to `x ^ n`, but it is convenient that `Monoid.npow` has this
-    argument order, since it matches `AddMonoid.nsmul n x`.
+    (e.g. `NPow.npow n x` corresponds to `x ^ n`, but it is convenient that `NPow.npow` has this
+    argument order, since it matches `NSMul.nsmul n x`.
   * If this is not possible, add `(reorder := ...)` argument to `to_additive`.
 
 If neither of these solutions work, and `to_additive` is unable to automatically generate the
diff --git a/Mathlib/Topology/Algebra/GroupCompletion.lean b/Mathlib/Topology/Algebra/GroupCompletion.lean
index 271859f78c13c2..225c1fb6db3801 100644
--- a/Mathlib/Topology/Algebra/GroupCompletion.lean
+++ b/Mathlib/Topology/Algebra/GroupCompletion.lean
@@ -70,12 +70,11 @@ open UniformSpace
 section Zero
 
 instance [UniformSpace α] [MonoidWithZero M] [Zero α] [MulActionWithZero M α]
-    [UniformContinuousConstSMul M α] : MulActionWithZero M (Completion α) :=
-  { (inferInstance : MulAction M <| Completion α) with
-    smul_zero := fun r ↦ by rw [← coe_zero, ← coe_smul, MulActionWithZero.smul_zero r]
-    zero_smul :=
-      ext' (continuous_const_smul _) continuous_const fun a ↦ by
-        rw [← coe_smul, zero_smul, coe_zero] }
+    [UniformContinuousConstSMul M α] : MulActionWithZero M (Completion α) where
+  smul_zero := fun r ↦ by rw [← coe_zero, ← coe_smul, MulActionWithZero.smul_zero r]
+  zero_smul :=
+    ext' (continuous_const_smul _) continuous_const fun a ↦ by
+      rw [← coe_smul, zero_smul, coe_zero]
 
 end Zero
 
@@ -95,82 +94,73 @@ theorem coe_sub (a b : α) : ((a - b : α) : Completion α) = a - b :=
 theorem coe_add (a b : α) : ((a + b : α) : Completion α) = a + b :=
   (map₂_coe_coe a b (· + ·) uniformContinuous_add).symm
 
-instance : AddMonoid (Completion α) :=
-  { (inferInstance : Zero <| Completion α),
-    (inferInstance : Add <| Completion α) with
-    zero_add := fun a ↦
-      Completion.induction_on a
-        (isClosed_eq (continuous_map₂ continuous_const continuous_id) continuous_id) fun a ↦
-        show 0 + (a : Completion α) = a by rw [← coe_zero, ← coe_add, zero_add]
-    add_zero := fun a ↦
-      Completion.induction_on a
-        (isClosed_eq (continuous_map₂ continuous_id continuous_const) continuous_id) fun a ↦
-        show (a : Completion α) + 0 = a by rw [← coe_zero, ← coe_add, add_zero]
-    add_assoc := fun a b c ↦
-      Completion.induction_on₃ a b c
-        (isClosed_eq
-          (continuous_map₂ (continuous_map₂ continuous_fst (by fun_prop)) (by fun_prop))
-          (continuous_map₂ continuous_fst (continuous_map₂ (by fun_prop) (by fun_prop))))
-        fun a b c ↦
-        show (a : Completion α) + b + c = a + (b + c) by repeat' rw_mod_cast [add_assoc]
-    nsmul := (· • ·)
-    nsmul_zero := fun a ↦
-      Completion.induction_on a (isClosed_eq continuous_map continuous_const) fun a ↦
-        show 0 • (a : Completion α) = 0 by rw [← coe_smul, ← coe_zero, zero_smul]
-    nsmul_succ := fun n a ↦
-      Completion.induction_on a
-        (isClosed_eq continuous_map <| continuous_map₂ continuous_map continuous_id) fun a ↦
-        show (n + 1) • (a : Completion α) = n • (a : Completion α) + (a : Completion α) by
-          rw [← coe_smul, succ_nsmul, coe_add, coe_smul] }
-
-instance : SubNegMonoid (Completion α) :=
-  { (inferInstance : AddMonoid <| Completion α),
-    (inferInstance : Neg <| Completion α),
-    (inferInstance : Sub <| Completion α) with
-    sub_eq_add_neg := fun a b ↦
-      Completion.induction_on₂ a b
-        (isClosed_eq (continuous_map₂ continuous_fst continuous_snd)
-          (continuous_map₂ continuous_fst (Completion.continuous_map.comp continuous_snd)))
-        fun a b ↦ mod_cast congr_arg ((↑) : α → Completion α) (sub_eq_add_neg a b)
-    zsmul := (· • ·)
-    zsmul_zero' := fun a ↦
-      Completion.induction_on a (isClosed_eq continuous_map continuous_const) fun a ↦
-        show (0 : ℤ) • (a : Completion α) = 0 by rw [← coe_smul, ← coe_zero, zero_smul]
-    zsmul_succ' := fun n a ↦
-      Completion.induction_on a
-        (isClosed_eq continuous_map <| continuous_map₂ continuous_map continuous_id) fun a ↦
-          show (n.succ : ℤ) • (a : Completion α) = _ by
-            rw [← coe_smul, show (n.succ : ℤ) • a = (n : ℤ) • a + a from
-              SubNegMonoid.zsmul_succ' n a, coe_add, coe_smul]
-    zsmul_neg' := fun n a ↦
-      Completion.induction_on a
-        (isClosed_eq continuous_map <| Completion.continuous_map.comp continuous_map) fun a ↦
-          show (Int.negSucc n) • (a : Completion α) = _ by
-            rw [← coe_smul, show (Int.negSucc n) • a = -((n.succ : ℤ) • a) from
-              SubNegMonoid.zsmul_neg' n a, coe_neg, coe_smul] }
-
-instance addGroup : AddGroup (Completion α) :=
-  { (inferInstance : SubNegMonoid <| Completion α) with
-    neg_add_cancel := fun a ↦
-      Completion.induction_on a
-        (isClosed_eq (continuous_map₂ Completion.continuous_map continuous_id) continuous_const)
-        fun a ↦
-        show -(a : Completion α) + a = 0 by
-          rw_mod_cast [neg_add_cancel]
-          rfl }
+instance : AddMonoid (Completion α) where
+  zero_add a :=
+    Completion.induction_on a
+      (isClosed_eq (continuous_map₂ continuous_const continuous_id) continuous_id) fun a ↦
+      show 0 + (a : Completion α) = a by rw [← coe_zero, ← coe_add, zero_add]
+  add_zero a :=
+    Completion.induction_on a
+      (isClosed_eq (continuous_map₂ continuous_id continuous_const) continuous_id) fun a ↦
+      show (a : Completion α) + 0 = a by rw [← coe_zero, ← coe_add, add_zero]
+  add_assoc := fun a b c ↦
+    Completion.induction_on₃ a b c
+      (isClosed_eq
+        (continuous_map₂ (continuous_map₂ continuous_fst (by fun_prop)) (by fun_prop))
+        (continuous_map₂ continuous_fst (continuous_map₂ (by fun_prop) (by fun_prop))))
+      fun a b c ↦
+      show (a : Completion α) + b + c = a + (b + c) by repeat' rw_mod_cast [add_assoc]
+  nsmul_zero a :=
+    Completion.induction_on a (isClosed_eq continuous_map continuous_const) fun a ↦
+      show 0 • (a : Completion α) = 0 by rw [← coe_smul, ← coe_zero, zero_smul]
+  nsmul_succ n a :=
+    Completion.induction_on a
+      (isClosed_eq continuous_map <| continuous_map₂ continuous_map continuous_id) fun a ↦
+      show (n + 1) • (a : Completion α) = n • (a : Completion α) + (a : Completion α) by
+        rw [← coe_smul, succ_nsmul, coe_add, coe_smul]
+
+instance : SubNegMonoid (Completion α) where
+  sub_eq_add_neg a b :=
+    Completion.induction_on₂ a b
+      (isClosed_eq (continuous_map₂ continuous_fst continuous_snd)
+        (continuous_map₂ continuous_fst (Completion.continuous_map.comp continuous_snd)))
+      fun a b ↦ mod_cast congr_arg ((↑) : α → Completion α) (sub_eq_add_neg a b)
+  zsmul_zero' a :=
+    Completion.induction_on a (isClosed_eq continuous_map continuous_const) fun a ↦
+      show (0 : ℤ) • (a : Completion α) = 0 by rw [← coe_smul, ← coe_zero, zero_smul]
+  zsmul_succ' n a :=
+    Completion.induction_on a
+      (isClosed_eq continuous_map <| continuous_map₂ continuous_map continuous_id) fun a ↦
+        show (n.succ : ℤ) • (a : Completion α) = _ by
+          rw [← coe_smul, show (n.succ : ℤ) • a = (n : ℤ) • a + a from
+            SubNegMonoid.zsmul_succ' n a, coe_add, coe_smul]
+  zsmul_neg' n a :=
+    Completion.induction_on a
+      (isClosed_eq continuous_map <| Completion.continuous_map.comp continuous_map) fun a ↦
+        show (Int.negSucc n) • (a : Completion α) = _ by
+          rw [← coe_smul, show (Int.negSucc n) • a = -((n.succ : ℤ) • a) from
+            SubNegMonoid.zsmul_neg' n a, coe_neg, coe_smul]
+
+instance addGroup : AddGroup (Completion α) where
+  neg_add_cancel a :=
+    Completion.induction_on a
+      (isClosed_eq (continuous_map₂ Completion.continuous_map continuous_id) continuous_const)
+      fun a ↦
+      show -(a : Completion α) + a = 0 by
+        rw_mod_cast [neg_add_cancel]
+        rfl
 
 instance isUniformAddGroup : IsUniformAddGroup (Completion α) :=
   ⟨uniformContinuous_map₂ Sub.sub⟩
 
 instance {M} [Monoid M] [DistribMulAction M α] [UniformContinuousConstSMul M α] :
-    DistribMulAction M (Completion α) :=
-  { (inferInstance : MulAction M <| Completion α) with
-    smul_add := fun r x y ↦
-      induction_on₂ x y
-        (isClosed_eq ((continuous_fst.add continuous_snd).const_smul _)
-          ((continuous_fst.const_smul _).add (continuous_snd.const_smul _)))
-        fun a b ↦ by simp only [← coe_add, ← coe_smul, smul_add]
-    smul_zero := fun r ↦ by rw [← coe_zero, ← coe_smul, smul_zero r] }
+    DistribMulAction M (Completion α) where
+  smul_add r x y :=
+    induction_on₂ x y
+      (isClosed_eq ((continuous_fst.add continuous_snd).const_smul _)
+        ((continuous_fst.const_smul _).add (continuous_snd.const_smul _)))
+      fun a b ↦ by simp only [← coe_add, ← coe_smul, smul_add]
+  smul_zero := fun r ↦ by rw [← coe_zero, ← coe_smul, smul_zero r]
 
 /-- The map from a group to its completion as a group hom. -/
 @[simps]
diff --git a/Mathlib/Topology/Algebra/Module/LinearMap.lean b/Mathlib/Topology/Algebra/Module/LinearMap.lean
index f7860d68752d09..fef15756f1773e 100644
--- a/Mathlib/Topology/Algebra/Module/LinearMap.lean
+++ b/Mathlib/Topology/Algebra/Module/LinearMap.lean
@@ -419,7 +419,6 @@ instance : AddMonoid (M₁ →SL[σ₁₂] M₂) where
     intros
     ext
     apply_rules [zero_add, add_assoc, add_zero, neg_add_cancel, add_comm]
-  nsmul := (· • ·)
   nsmul_zero f := by
     ext
     simp
@@ -889,7 +888,6 @@ instance sub : Sub (M →SL[σ₁₂] M₂) :=
 
 instance addCommGroup : AddCommGroup (M →SL[σ₁₂] M₂) where
   sub_eq_add_neg _ _ := by ext; apply sub_eq_add_neg
-  zsmul := (· • ·)
   zsmul_zero' f := by ext; simp
   zsmul_succ' n f := by ext; simp [add_smul, add_comm]
   zsmul_neg' n f := by ext; simp [add_smul]
diff --git a/MathlibTest/instance_diamonds.lean b/MathlibTest/instance_diamonds.lean
index 51da1545491e5d..18ce754902b8f0 100644
--- a/MathlibTest/instance_diamonds.lean
+++ b/MathlibTest/instance_diamonds.lean
@@ -24,7 +24,7 @@ section SMul
 
 open scoped Polynomial
 
-example : (SubNegMonoid.toZSMul : SMul ℤ ℂ) = (Complex.SMul.instSMulRealComplex : SMul ℤ ℂ) := by
+example : (ZSMul.toSMul : SMul ℤ ℂ) = (Complex.SMul.instSMulRealComplex : SMul ℤ ℂ) := by
   with_reducible_and_instances rfl
 
 set_option backward.isDefEq.respectTransparency false in
@@ -36,19 +36,19 @@ example : Algebra.restrictScalars ℝ ℂ ℂ = Complex.instAlgebraOfReal := by
   rfl
 
 example (α β : Type _) [AddMonoid α] [AddMonoid β] :
-    (Prod.instSMul : SMul ℕ (α × β)) = AddMonoid.toNSMul := by
+    (Prod.instSMul : SMul ℕ (α × β)) = NSMul.toSMul := by
   with_reducible_and_instances rfl
 
 example (α β : Type _) [SubNegMonoid α] [SubNegMonoid β] :
-    (Prod.instSMul : SMul ℤ (α × β)) = SubNegMonoid.toZSMul := by
+    (Prod.instSMul : SMul ℤ (α × β)) = ZSMul.toSMul := by
   with_reducible_and_instances rfl
 
 example (α : Type _) (β : α → Type _) [∀ a, AddMonoid (β a)] :
-    (Pi.instSMul : SMul ℕ (∀ a, β a)) = AddMonoid.toNSMul := by
+    (Pi.instSMul : SMul ℕ (∀ a, β a)) = NSMul.toSMul := by
   with_reducible_and_instances rfl
 
 example (α : Type _) (β : α → Type _) [∀ a, SubNegMonoid (β a)] :
-    (Pi.instSMul : SMul ℤ (∀ a, β a)) = SubNegMonoid.toZSMul := by
+    (Pi.instSMul : SMul ℤ (∀ a, β a)) = ZSMul.toSMul := by
   with_reducible_and_instances rfl
 
 namespace TensorProduct