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
leanprover-community · Sep 22, 2024 · 9274c08 · 9274c08
1 parent ed1a8a0
commit 9274c08
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 5 deletions.
diff --git a/Mathlib/Algebra/Group/Basic.lean b/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

diff --git a/Mathlib/FieldTheory/Differential/Basic.lean b/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]

diff --git a/Mathlib/LinearAlgebra/RootSystem/Defs.lean b/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) := ?_

diff --git a/Mathlib/Topology/Algebra/Field.lean b/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