feat: NSMul/NPow type class

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

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,15 +236,14 @@ 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 _ (_ * _) = _
     rw [map_zero]
     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

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
 

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
+
+@[to_additive toSMul, default_instance high]
+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 ↦ 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 ↦ 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 :=

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]

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

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' _ _
 

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' ..

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

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 :=