style(Algebra): write coe_pow lemmas more clearly (#8292)

Author: eric-wieser

Mathlib/Algebra/Group/WithOne/Defs.lean

@@ -309,7 +309,7 @@ instance [One α] [Pow α ℤ] : Pow (WithZero α) ℤ :=
     | some x, n => ↑(x ^ n)⟩
 
 @[simp, norm_cast]
-theorem coe_zpow [DivInvMonoid α] {a : α} (n : ℤ) : ↑(a ^ n : α) = ((↑a : WithZero α) ^ n) :=
+theorem coe_zpow [DivInvMonoid α] {a : α} (n : ℤ) : ↑(a ^ n) = (↑a : WithZero α) ^ n :=
   rfl
 #align with_zero.coe_zpow WithZero.coe_zpow
 

Mathlib/Data/Rat/Cast/CharZero.lean

@@ -121,7 +121,7 @@ theorem cast_mk (a b : ℤ) : (a /. b : α) = a / b := by
 #align rat.cast_mk Rat.cast_mk
 
 @[simp, norm_cast]
-theorem cast_pow (q : ℚ) (k : ℕ) : (↑(q ^ k) : α) = (q : α) ^ k :=
+theorem cast_pow (q : ℚ) (k : ℕ) : ↑(q ^ k) = (q : α) ^ k :=
   (castHom α).map_pow q k
 #align rat.cast_pow Rat.cast_pow
 

Mathlib/GroupTheory/GroupAction/SubMulAction/Pointwise.lean

@@ -115,14 +115,14 @@ instance : Monoid (SubMulAction R M) :=
   { SubMulAction.semiGroup,
     SubMulAction.mulOneClass with }
 
-theorem coe_pow (p : SubMulAction R M) : ∀ {n : ℕ} (_ : n ≠ 0), ↑(p ^ n) = ((p : Set M) ^ n)
+theorem coe_pow (p : SubMulAction R M) : ∀ {n : ℕ} (_ : n ≠ 0), ↑(p ^ n) = (p : Set M) ^ n
   | 0, hn => (hn rfl).elim
   | 1, _ => by rw [pow_one, pow_one]
   | n + 2, _ => by
     rw [pow_succ _ (n + 1), pow_succ _ (n + 1), coe_mul, coe_pow _ n.succ_ne_zero]
 #align sub_mul_action.coe_pow SubMulAction.coe_pow
 
-theorem subset_coe_pow (p : SubMulAction R M) : ∀ {n : ℕ}, ((p : Set M) ^ n) ⊆ ↑(p ^ n)
+theorem subset_coe_pow (p : SubMulAction R M) : ∀ {n : ℕ}, (p : Set M) ^ n ⊆ ↑(p ^ n)
   | 0 => by
     rw [pow_zero, pow_zero]
     exact subset_coe_one