feat: tag Pow.mk with to_additive (#36302)

This PR uses the new `reorder` support in `to_additive` to automatically generate `SMul` instances from `Pow` instances.

I've tried to address most such instances, but this is probably not exhaustive. I've also taken the opportunity to uniformize the instance names a bit.

I wonder, should we change the order of the arguments in `Monoid.npow : ℕ → M → M` and `npowRec` to be consistent with the usual power operation, now that `to_additive` can support this kind of reordering? I suspect that the current ordering only exists for the sake of `to_additive`.

Author: JovanGerb

Mathlib/Algebra/Group/Defs.lean

@@ -623,14 +623,10 @@ class Monoid (M : Type u) extends Semigroup M, MulOneClass M where
   /-- 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] instance Monoid.toNatPow {M : Type*} [Monoid M] : Pow M ℕ :=
+@[default_instance high, to_additive]
+instance Monoid.toPow {M : Type*} [Monoid M] : Pow M ℕ :=
   ⟨fun x n ↦ Monoid.npow n x⟩
 
-instance AddMonoid.toNatSMul {M : Type*} [AddMonoid M] : SMul ℕ M :=
-  ⟨AddMonoid.nsmul⟩
-
-attribute [to_additive existing toNatSMul] Monoid.toNatPow
-
 section Monoid
 variable {M : Type*} [Monoid M] {a b c : M}
 

Mathlib/Algebra/Group/Hom/Instances.lean

@@ -32,24 +32,13 @@ universe uM uN uP uQ
 
 variable {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ}
 
-instance ZeroHom.instNatSMul [Zero M] [AddMonoid N] : SMul ℕ (ZeroHom M N) where
-  smul a f :=
-    { toFun := a • f
-      map_zero' := by simp }
-
-instance AddMonoidHom.instNatSMul [AddZeroClass M] [AddCommMonoid N] : SMul ℕ (M →+ N) where
-  smul a f :=
-    { toFun := a • f
-      map_zero' := by simp
-      map_add' x y := by simp [nsmul_add] }
-
-@[to_additive existing ZeroHom.instNatSMul]
+@[to_additive]
 instance OneHom.instPow [One M] [Monoid N] : Pow (OneHom M N) ℕ where
   pow f n :=
     { toFun := f ^ n
       map_one' := by simp }
 
-@[to_additive existing AddMonoidHom.instNatSMul]
+@[to_additive]
 instance MonoidHom.instPow [MulOneClass M] [CommMonoid N] : Pow (M →* N) ℕ where
   pow f n :=
     { toFun := f ^ n
@@ -84,25 +73,14 @@ instance MonoidHom.instCommMonoid [MulOneClass M] [CommMonoid N] : CommMonoid (M
   fast_instance%
     DFunLike.coe_injective.commMonoid DFunLike.coe rfl (fun _ _ => rfl) (fun _ _ => rfl)
 
-instance ZeroHom.instIntSMul [Zero M] [AddGroup N] : SMul ℤ (ZeroHom M N) where
-  smul a f :=
-    { toFun := a • f
-      map_zero' := by simp [zsmul_zero] }
-
-instance AddMonoidHom.instIntSMul [AddZeroClass M] [AddCommGroup N] : SMul ℤ (M →+ N) where
-  smul a f :=
-    { toFun := a • f
-      map_zero' := by simp [zsmul_zero]
-      map_add' x y := by simp [zsmul_add] }
-
-@[to_additive existing ZeroHom.instIntSMul]
-instance OneHom.instIntPow [One M] [Group N] : Pow (OneHom M N) ℤ where
+@[to_additive]
+instance OneHom.instZPow [One M] [Group N] : Pow (OneHom M N) ℤ where
   pow f n :=
     { toFun := f ^ n
       map_one' := by simp }
 
-@[to_additive existing AddMonoidHom.instIntSMul]
-instance MonoidHom.instIntPow [MulOneClass M] [CommGroup N] : Pow (M →* N) ℤ where
+@[to_additive]
+instance MonoidHom.instZPow [MulOneClass M] [CommGroup N] : Pow (M →* N) ℤ where
   pow f n :=
     { toFun := f ^ n
       map_one' := by simp

Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean

@@ -695,30 +695,19 @@ section Instances
 
 variable [DecidableEq α] [DecidableEq β]
 
-/-- Repeated pointwise addition (not the same as pointwise repeated addition!) of a `Finset`. See
-note [pointwise nat action]. -/
-@[instance_reducible]
-protected def nsmul [Zero α] [Add α] : SMul ℕ (Finset α) :=
-  ⟨nsmulRec⟩
-
 /-- Repeated pointwise multiplication (not the same as pointwise repeated multiplication!) of a
 `Finset`. See note [pointwise nat action]. -/
-@[instance_reducible]
+@[to_additive (attr := instance_reducible)
+/-- Repeated pointwise addition (not the same as pointwise repeated addition!) of a `Finset`. See
+note [pointwise nat action]. -/]
 protected def npow [One α] [Mul α] : Pow (Finset α) ℕ :=
   ⟨fun s n => npowRec n s⟩
 
-attribute [to_additive existing] Finset.npow
-
-
-/-- Repeated pointwise addition/subtraction (not the same as pointwise repeated
-addition/subtraction!) of a `Finset`. See note [pointwise nat action]. -/
-@[instance_reducible]
-protected def zsmul [Zero α] [Add α] [Neg α] : SMul ℤ (Finset α) :=
-  ⟨zsmulRec⟩
-
 /-- Repeated pointwise multiplication/division (not the same as pointwise repeated
 multiplication/division!) of a `Finset`. See note [pointwise nat action]. -/
-@[instance_reducible, to_additive existing]
+@[to_additive (attr := instance_reducible)
+/-- Repeated pointwise addition/subtraction (not the same as pointwise repeated
+addition/subtraction!) of a `Finset`. See note [pointwise nat action]. -/]
 protected def zpow [One α] [Mul α] [Inv α] : Pow (Finset α) ℤ :=
   ⟨fun s n => zpowRec npowRec n s⟩
 

Mathlib/Algebra/Group/Pointwise/Set/Basic.lean

@@ -531,27 +531,20 @@ theorem union_div_inter_subset_union : (s₁ ∪ s₂) / (t₁ ∩ t₂) ⊆ s
 
 end Div
 
-/-- Repeated pointwise addition (not the same as pointwise repeated addition!) of a `Set`. See
-note [pointwise nat action]. -/
-@[instance_reducible]
-protected def NSMul [Zero α] [Add α] : SMul ℕ (Set α) :=
-  ⟨nsmulRec⟩
-
+-- TODO: rename `NPow` to `npow` and `ZPow` to `zpow`.
 /-- Repeated pointwise multiplication (not the same as pointwise repeated multiplication!) of a
 `Set`. See note [pointwise nat action]. -/
-@[instance_reducible, to_additive existing]
+@[to_additive (attr := instance_reducible)
+/-- Repeated pointwise addition (not the same as pointwise repeated addition!) of a `Set`. See
+note [pointwise nat action]. -/]
 protected def NPow [One α] [Mul α] : Pow (Set α) ℕ :=
   ⟨fun s n => npowRec n s⟩
 
-/-- Repeated pointwise addition/subtraction (not the same as pointwise repeated
-addition/subtraction!) of a `Set`. See note [pointwise nat action]. -/
-@[instance_reducible]
-protected def ZSMul [Zero α] [Add α] [Neg α] : SMul ℤ (Set α) :=
-  ⟨zsmulRec⟩
-
 /-- Repeated pointwise multiplication/division (not the same as pointwise repeated
 multiplication/division!) of a `Set`. See note [pointwise nat action]. -/
-@[instance_reducible, to_additive existing]
+@[to_additive (attr := instance_reducible)
+/-- Repeated pointwise addition/subtraction (not the same as pointwise repeated
+addition/subtraction!) of a `Set`. See note [pointwise nat action]. -/]
 protected def ZPow [One α] [Mul α] [Inv α] : Pow (Set α) ℤ :=
   ⟨fun s n => zpowRec npowRec n s⟩
 

Mathlib/Algebra/Group/Subgroup/Defs.lean

@@ -190,14 +190,9 @@ theorem subset_union [LE S] [IsConcreteLE S G] {H K L : S} :
 instance div {G S : Type*} [DivInvMonoid G] [SetLike S G] [SubgroupClass S G] {H : S} : Div H :=
   ⟨fun a b => ⟨a / b, div_mem a.2 b.2⟩⟩
 
-/-- An additive subgroup of an `AddGroup` inherits an integer scaling. -/
-instance _root_.AddSubgroupClass.zsmul {M S} [SubNegMonoid M] [SetLike S M]
-    [AddSubgroupClass S M] {H : S} : SMul ℤ H :=
-  ⟨fun n a => ⟨n • a.1, zsmul_mem a.2 n⟩⟩
-
 /-- A subgroup of a group inherits an integer power. -/
-@[to_additive existing]
-instance zpow {M S} [DivInvMonoid M] [SetLike S M] [SubgroupClass S M] {H : S} : Pow H ℤ :=
+@[to_additive /-- An additive subgroup of an `AddGroup` inherits an integer scaling. -/]
+instance instZPow {M S} [DivInvMonoid M] [SetLike S M] [SubgroupClass S M] {H : S} : Pow H ℤ :=
   ⟨fun a n => ⟨a.1 ^ n, zpow_mem a.2 n⟩⟩
 
 @[to_additive (attr := simp, norm_cast)]
@@ -508,21 +503,13 @@ instance inv : Inv H :=
 instance div : Div H :=
   ⟨fun a b => ⟨a / b, H.div_mem a.2 b.2⟩⟩
 
-/-- An `AddSubgroup` of an `AddGroup` inherits a natural scaling. -/
-instance _root_.AddSubgroup.nsmul {G} [AddGroup G] {H : AddSubgroup G} : SMul ℕ H :=
-  ⟨fun n a => ⟨n • a, H.nsmul_mem a.2 n⟩⟩
-
 /-- A subgroup of a group inherits a natural power -/
-@[to_additive existing]
+@[to_additive /-- An `AddSubgroup` of an `AddGroup` inherits a natural scaling. -/]
 protected instance npow : Pow H ℕ :=
   ⟨fun a n => ⟨a ^ n, H.pow_mem a.2 n⟩⟩
 
-/-- An `AddSubgroup` of an `AddGroup` inherits an integer scaling. -/
-instance _root_.AddSubgroup.zsmul {G} [AddGroup G] {H : AddSubgroup G} : SMul ℤ H :=
-  ⟨fun n a => ⟨n • a, H.zsmul_mem a.2 n⟩⟩
-
 /-- A subgroup of a group inherits an integer power -/
-@[to_additive existing]
+@[to_additive /-- An `AddSubgroup` of an `AddGroup` inherits an integer scaling. -/]
 instance zpow : Pow H ℤ :=
   ⟨fun a n => ⟨a ^ n, H.zpow_mem a.2 n⟩⟩
 

Mathlib/Algebra/Group/Subgroup/ZPowers/Basic.lean

@@ -121,12 +121,9 @@ instance zpowers_isMulCommutative (g : G) : IsMulCommutative (zpowers g) :=
 theorem zpowers_le {g : G} {H : Subgroup G} : zpowers g ≤ H ↔ g ∈ H := by
   rw [zpowers_eq_closure, closure_le, Set.singleton_subset_iff, SetLike.mem_coe]
 
+@[to_additive]
 alias ⟨_, zpowers_le_of_mem⟩ := zpowers_le
 
-alias ⟨_, _root_.AddSubgroup.zmultiples_le_of_mem⟩ := AddSubgroup.zmultiples_le
-
-attribute [to_additive existing] zpowers_le_of_mem
-
 @[to_additive (attr := simp)]
 theorem zpowers_eq_bot {g : G} : zpowers g = ⊥ ↔ g = 1 := by rw [eq_bot_iff, zpowers_le, mem_bot]
 

Mathlib/Algebra/Group/Submonoid/Defs.lean

@@ -357,19 +357,13 @@ end OneMemClass
 
 variable {A : Type*} [MulOneClass M] [SetLike A M] [hA : SubmonoidClass A M] (S' : A)
 
-/-- An `AddSubmonoid` of an `AddMonoid` inherits a scalar multiplication. -/
-instance AddSubmonoidClass.nSMul {M} [AddMonoid M] {A : Type*} [SetLike A M]
-    [AddSubmonoidClass A M] (S : A) : SMul ℕ S :=
-  ⟨fun n a => ⟨n • a.1, nsmul_mem a.2 n⟩⟩
-
 namespace SubmonoidClass
 
 /-- A submonoid of a monoid inherits a power operator. -/
-instance nPow {M} [Monoid M] {A : Type*} [SetLike A M] [SubmonoidClass A M] (S : A) : Pow S ℕ :=
+@[to_additive /-- An `AddSubmonoid` of an `AddMonoid` inherits a scalar multiplication. -/]
+instance instPow {M} [Monoid M] {A : Type*} [SetLike A M] [SubmonoidClass A M] (S : A) : Pow S ℕ :=
   ⟨fun a n => ⟨a.1 ^ n, pow_mem a.2 n⟩⟩
 
-attribute [to_additive existing nSMul] nPow
-
 @[to_additive (attr := simp, norm_cast)]
 theorem coe_pow {M} [Monoid M] {A : Type*} [SetLike A M] [SubmonoidClass A M] {S : A} (x : S)
     (n : ℕ) : ↑(x ^ n) = (x : M) ^ n :=

Mathlib/Algebra/Group/TransferInstance.lean

@@ -67,22 +67,13 @@ lemma inv_def [Inv β] (x : α) :
     letI := e.Inv
     x⁻¹ = e.symm (e x)⁻¹ := rfl
 
-variable (M) in
-/-- Transfer `SMul` across an `Equiv` -/
-@[to_additive /-- Transfer `VAdd` across an `Equiv` -/]
-protected abbrev smul [SMul M β] : SMul M α where smul r x := e.symm (r • e x)
-
-@[to_additive]
-lemma smul_def [SMul M β] (r : M) (x : α) :
-    letI := e.smul M
-    r • x = e.symm (r • e x) := rfl
-
 variable (M) in
 /-- Transfer `Pow` across an `Equiv` -/
-@[to_additive existing smul]
+@[to_additive (attr := to_additive /-- Transfer `VAdd` across an `Equiv` -/) smul
+/-- Transfer `SMul` across an `Equiv` -/]
 protected abbrev pow [Pow β M] : Pow α M where pow x n := e.symm (e x ^ n)
 
-@[to_additive existing smul_def]
+@[to_additive (attr := to_additive) smul_def]
 lemma pow_def [Pow β M] (n : M) (x : α) :
     letI := e.pow M
     x ^ n = e.symm (e x ^ n) := rfl

Mathlib/Algebra/Group/ULift.lean

@@ -60,19 +60,11 @@ instance inv [Inv α] : Inv (ULift α) :=
 theorem inv_down [Inv α] : x⁻¹.down = x.down⁻¹ :=
   rfl
 
-@[to_additive]
-instance smul [SMul α β] : SMul α (ULift β) :=
-  ⟨fun n x => up (n • x.down)⟩
-
-@[to_additive (attr := simp)]
-theorem smul_down [SMul α β] (a : α) (b : ULift.{w} β) : (a • b).down = a • b.down :=
-  rfl
-
-@[to_additive existing smul]
+@[to_additive (attr := to_additive) smul]
 instance pow [Pow α β] : Pow (ULift α) β :=
   ⟨fun x n => up (x.down ^ n)⟩
 
-@[to_additive existing (attr := simp) smul_down]
+@[to_additive (attr := to_additive, simp) smul_down]
 theorem pow_down [Pow α β] (a : ULift.{w} α) (b : β) : (a ^ b).down = a.down ^ b :=
   rfl
 

Mathlib/Algebra/Notation/Defs.lean

@@ -64,7 +64,9 @@ class VSub (G : outParam Type*) (P : Type*) where
   type-dependent, but it is intended to be used for additive torsors. -/
   vsub : P → P → G
 
-attribute [to_additive] SMul
+attribute [to_additive existing] SMul HSMul
+attribute [to_additive (attr := default_instance)] instHSMul
+
 attribute [ext] SMul VAdd
 
 @[inherit_doc] infixr:65 " +ᵥ " => HVAdd.hVAdd
@@ -73,19 +75,8 @@ attribute [ext] SMul VAdd
 recommended_spelling "vadd" for "+ᵥ" in [HVAdd.hVAdd, «term_+ᵥ_»]
 recommended_spelling "vsub" for "-ᵥ" in [VSub.vsub, «term_-ᵥ_»]
 
-attribute [to_additive existing] Mul Div HMul instHMul HDiv instHDiv HSMul
-attribute [to_additive (reorder := 1 2) SMul] Pow
-attribute [to_additive (reorder := 1 2)] HPow
-attribute [to_additive existing (reorder := 1 2, 5 6) hSMul] HPow.hPow
-attribute [to_additive existing (reorder := 1 2, 4 5) smul] Pow.pow
-
-attribute [to_additive (attr := default_instance)] instHSMul
-attribute [to_additive existing] instHPow
-
 variable {G : Type*}
 
-attribute [to_additive, notation_class] Inv
-
 section Star
 
 /-- Notation typeclass (with no default notation!) for an algebraic structure with a star operation.