chore(Algebra/Group/TypeTags): lemmas about pow and smul (#7862)

Half of these lemmas already existed, but were a long way from the definition that define the operators.
For the ones that did exist, the `#align`s have been kept.

The new lemmas are all `@[simp]` since that matches the corresponding `add`/`mul` lemmas.
This makes some lemmas about `Int` and `Nat` not simp-normal any more (they disagree on commutativity), but that doesn't seem to matter.

Mathlib/Algebra/Group/TypeTags.lean

@@ -267,6 +267,24 @@ instance Multiplicative.monoid [h : AddMonoid α] : Monoid (Multiplicative α) :
     npow_zero := @AddMonoid.nsmul_zero α h
     npow_succ := @AddMonoid.nsmul_succ α h }
 
+@[simp]
+theorem ofMul_pow [Monoid α] (n : ℕ) (a : α) : ofMul (a ^ n) = n • ofMul a :=
+  rfl
+#align of_mul_pow ofMul_pow
+
+@[simp]
+theorem toMul_nsmul [Monoid α] (n : ℕ) (a : Additive α) : toMul (n • a) = toMul a ^ n :=
+  rfl
+
+@[simp]
+theorem ofAdd_nsmul [AddMonoid α] (n : ℕ) (a : α) : ofAdd (n • a) = ofAdd a ^ n :=
+  rfl
+#align of_add_nsmul ofAdd_nsmul
+
+@[simp]
+theorem toAdd_pow [AddMonoid α] (a : Multiplicative α) (n : ℕ) : toAdd (a ^ n) = n • toAdd a :=
+  rfl
+
 instance Additive.addLeftCancelMonoid [LeftCancelMonoid α] : AddLeftCancelMonoid (Additive α) :=
   { Additive.addMonoid, Additive.addLeftCancelSemigroup with }
 
@@ -363,6 +381,24 @@ instance Multiplicative.divInvMonoid [SubNegMonoid α] : DivInvMonoid (Multiplic
     zpow_succ' := @SubNegMonoid.zsmul_succ' α _
     zpow_neg' := @SubNegMonoid.zsmul_neg' α _ }
 
+@[simp]
+theorem ofMul_zpow [DivInvMonoid α] (z : ℤ) (a : α) : ofMul (a ^ z) = z • ofMul a :=
+  rfl
+#align of_mul_zpow ofMul_zpow
+
+@[simp]
+theorem toMul_zsmul [DivInvMonoid α] (z : ℤ) (a : Additive α) : toMul (z • a) = toMul a ^ z :=
+  rfl
+
+@[simp]
+theorem ofAdd_zsmul [SubNegMonoid α] (z : ℤ) (a : α) : ofAdd (z • a) = ofAdd a ^ z :=
+  rfl
+#align of_add_zsmul ofAdd_zsmul
+
+@[simp]
+theorem toAdd_zpow [SubNegMonoid α] (a : Multiplicative α) (z : ℤ) : toAdd (a ^ z) = z • toAdd a :=
+  rfl
+
 instance Additive.subtractionMonoid [DivisionMonoid α] : SubtractionMonoid (Additive α) :=
   { Additive.subNegMonoid, Additive.involutiveNeg with
     neg_add_rev := @mul_inv_rev α _

Mathlib/Algebra/GroupPower/Basic.lean

@@ -443,25 +443,6 @@ theorem pow_dvd_pow [Monoid R] (a : R) {m n : ℕ} (h : m ≤ n) : a ^ m ∣ a ^
   ⟨a ^ (n - m), by rw [← pow_add, Nat.add_comm, Nat.sub_add_cancel h]⟩
 #align pow_dvd_pow pow_dvd_pow
 
-theorem ofAdd_nsmul [AddMonoid A] (x : A) (n : ℕ) :
-    Multiplicative.ofAdd (n • x) = Multiplicative.ofAdd x ^ n :=
-  rfl
-#align of_add_nsmul ofAdd_nsmul
-
-theorem ofAdd_zsmul [SubNegMonoid A] (x : A) (n : ℤ) :
-    Multiplicative.ofAdd (n • x) = Multiplicative.ofAdd x ^ n :=
-  rfl
-#align of_add_zsmul ofAdd_zsmul
-
-theorem ofMul_pow [Monoid A] (x : A) (n : ℕ) : Additive.ofMul (x ^ n) = n • Additive.ofMul x :=
-  rfl
-#align of_mul_pow ofMul_pow
-
-theorem ofMul_zpow [DivInvMonoid G] (x : G) (n : ℤ) :
-    Additive.ofMul (x ^ n) = n • Additive.ofMul x :=
-  rfl
-#align of_mul_zpow ofMul_zpow
-
 @[to_additive (attr := simp)]
 theorem SemiconjBy.zpow_right [Group G] {a x y : G} (h : SemiconjBy a x y) :
     ∀ m : ℤ, SemiconjBy a (x ^ m) (y ^ m)

Mathlib/Algebra/GroupPower/Lemmas.lean

@@ -1177,7 +1177,6 @@ section Multiplicative
 
 open Multiplicative
 
-@[simp]
 theorem Nat.toAdd_pow (a : Multiplicative ℕ) (b : ℕ) : toAdd (a ^ b) = toAdd a * b :=
   mul_comm _ _
 #align nat.to_add_pow Nat.toAdd_pow
@@ -1187,12 +1186,10 @@ theorem Nat.ofAdd_mul (a b : ℕ) : ofAdd (a * b) = ofAdd a ^ b :=
   (Nat.toAdd_pow _ _).symm
 #align nat.of_add_mul Nat.ofAdd_mul
 
-@[simp]
 theorem Int.toAdd_pow (a : Multiplicative ℤ) (b : ℕ) : toAdd (a ^ b) = toAdd a * b :=
   mul_comm _ _
 #align int.to_add_pow Int.toAdd_pow
 
-@[simp]
 theorem Int.toAdd_zpow (a : Multiplicative ℤ) (b : ℤ) : toAdd (a ^ b) = toAdd a * b :=
   mul_comm _ _
 #align int.to_add_zpow Int.toAdd_zpow