refactor: Unsimp div_pow/div_zpow (#17019)

... and additive versions. These lemmas are not affine (`n` appears twice on the RHS and only once on the LHS). Also note that `mul_pow` and `mul_zpow` are analogous but not simp.

From LeanAPAP

Mathlib/Algebra/Group/Basic.lean

@@ -586,14 +586,16 @@ theorem mul_div_mul_comm : a * b / (c * d) = a / c * (b / d) := by simp
   | (n : ℕ) => by simp_rw [zpow_natCast, mul_pow]
   | .negSucc n => by simp_rw [zpow_negSucc, ← inv_pow, mul_inv, mul_pow]
 
-@[to_additive (attr := simp) nsmul_sub]
+@[to_additive nsmul_sub]
 lemma div_pow (a b : α) (n : ℕ) : (a / b) ^ n = a ^ n / b ^ n := by
   simp only [div_eq_mul_inv, mul_pow, inv_pow]
 
-@[to_additive (attr := simp) zsmul_sub]
+@[to_additive zsmul_sub]
 lemma div_zpow (a b : α) (n : ℤ) : (a / b) ^ n = a ^ n / b ^ n := by
   simp only [div_eq_mul_inv, mul_zpow, inv_zpow]
 
+attribute [field_simps] div_pow div_zpow
+
 end DivisionCommMonoid
 
 section Group

Mathlib/Analysis/Analytic/Basic.lean

@@ -874,7 +874,7 @@ theorem HasFPowerSeriesWithinAt.isBigO_sub_partialSum_pow
   refine isBigO_iff.2 ⟨C * (a / r') ^ n, ?_⟩
   replace r'0 : 0 < (r' : ℝ) := mod_cast r'0
   filter_upwards [inter_mem_nhdsWithin _ (Metric.ball_mem_nhds (0 : E) r'0)] with y hy
-  simpa [mul_pow, mul_div_assoc, mul_assoc, div_mul_eq_mul_div]
+  simpa [mul_pow, mul_div_assoc, mul_assoc, div_mul_eq_mul_div, div_pow]
     using hp y hy.2 n (by simpa using hy.1)
 
 /-- Taylor formula for an analytic function, `IsBigO` version. -/

Mathlib/Analysis/SpecificLimits/Normed.lean

@@ -212,7 +212,7 @@ theorem isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt {R : Type*} [Norm
   have A : (fun n ↦ (n : R) ^ k : ℕ → R) =o[atTop] fun n ↦ (r₂ / ‖r₁‖) ^ n :=
     isLittleO_pow_const_const_pow_of_one_lt k ((one_lt_div h0).2 h)
   suffices (fun n ↦ r₁ ^ n) =O[atTop] fun n ↦ ‖r₁‖ ^ n by
-    simpa [div_mul_cancel₀ _ (pow_pos h0 _).ne'] using A.mul_isBigO this
+    simpa [div_mul_cancel₀ _ (pow_pos h0 _).ne', div_pow] using A.mul_isBigO this
   exact IsBigO.of_bound 1 (by simpa using eventually_norm_pow_le r₁)
 
 theorem tendsto_pow_const_div_const_pow_of_one_lt (k : ℕ) {r : ℝ} (hr : 1 < r) :

Mathlib/Data/Real/GoldenRatio.lean

@@ -95,7 +95,7 @@ theorem gold_ne_zero : φ ≠ 0 :=
 
 theorem one_lt_gold : 1 < φ := by
   refine lt_of_mul_lt_mul_left ?_ (le_of_lt gold_pos)
-  simp [← sq, gold_pos, zero_lt_one, - div_pow] -- Porting note: Added `- div_pow`
+  simp [← sq, gold_pos, zero_lt_one]
 
 theorem gold_lt_two : φ < 2 := by calc
   (1 + sqrt 5) / 2 < (1 + 3) / 2 := by gcongr; rw [sqrt_lt'] <;> norm_num
@@ -168,12 +168,12 @@ theorem fib_isSol_fibRec : fibRec.IsSolution (fun x => x.fib : ℕ → α) := by
 /-- The geometric sequence `fun n ↦ φ^n` is a solution of `fibRec`. -/
 theorem geom_gold_isSol_fibRec : fibRec.IsSolution (φ ^ ·) := by
   rw [fibRec.geom_sol_iff_root_charPoly, fibRec_charPoly_eq]
-  simp [sub_eq_zero, - div_pow] -- Porting note: Added `- div_pow`
+  simp [sub_eq_zero]
 
 /-- The geometric sequence `fun n ↦ ψ^n` is a solution of `fibRec`. -/
 theorem geom_goldConj_isSol_fibRec : fibRec.IsSolution (ψ ^ ·) := by
   rw [fibRec.geom_sol_iff_root_charPoly, fibRec_charPoly_eq]
-  simp [sub_eq_zero, - div_pow] -- Porting note: Added `- div_pow`
+  simp [sub_eq_zero]
 
 end Fibrec
 

Mathlib/FieldTheory/Differential/Basic.lean

@@ -41,7 +41,7 @@ lemma logDeriv_mul (ha : a ≠ 0) (hb : b ≠ 0) : logDeriv (a * b) = logDeriv a
 
 lemma logDeriv_div (ha : a ≠ 0) (hb : b ≠ 0) : logDeriv (a / b) = logDeriv a - logDeriv b := by
   unfold logDeriv
-  field_simp [Derivation.leibniz_div]
+  field_simp [Derivation.leibniz_div, smul_sub]
   ring
 
 @[simp]

Mathlib/LinearAlgebra/RootSystem/Defs.lean

@@ -433,7 +433,7 @@ lemma two_nsmul_reflection_eq_of_perm_eq (hij : P.reflection_perm i = P.reflecti
     2 • ⇑(P.reflection i) = 2 • P.reflection j := by
   ext x
   suffices 2 • P.toLin x (P.coroot i) • P.root i = 2 • P.toLin x (P.coroot j) • P.root j by
-    simpa [reflection_apply]
+    simpa [reflection_apply, smul_sub]
   calc 2 • P.toLin x (P.coroot i) • P.root i
       = P.toLin x (P.coroot i) • ((2 : R) • P.root i) := ?_
     _ = P.toLin x (P.coroot i) • (P.pairing i j • P.root j) := ?_

Mathlib/Topology/Algebra/Field.lean

@@ -132,7 +132,7 @@ theorem IsPreconnected.eq_or_eq_neg_of_sq_eq [Field 𝕜] [HasContinuousInv₀ 
     (hsq : EqOn (f ^ 2) (g ^ 2) S) (hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0) :
     EqOn f g S ∨ EqOn f (-g) S := by
   have hsq : EqOn ((f / g) ^ 2) 1 S := fun x hx => by
-    simpa [div_eq_one_iff_eq (pow_ne_zero _ (hg_ne hx))] using hsq hx
+    simpa [div_eq_one_iff_eq (pow_ne_zero _ (hg_ne hx)), div_pow] using hsq hx
   simpa (config := { contextual := true }) [EqOn, div_eq_iff (hg_ne _)]
     using hS.eq_one_or_eq_neg_one_of_sq_eq (hf.div hg fun z => hg_ne) hsq