diff --git a/Mathlib/Algebra/Group/Basic.lean b/Mathlib/Algebra/Group/Basic.lean index 492d4bb387a9d..1fd34ff37fdbc 100644 --- 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/Analysis/Analytic/Basic.lean b/Mathlib/Analysis/Analytic/Basic.lean index 995fbba71ec66..1abdcf481ef99 100644 --- a/Mathlib/Analysis/Analytic/Basic.lean +++ b/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. -/ diff --git a/Mathlib/Analysis/SpecificLimits/Normed.lean b/Mathlib/Analysis/SpecificLimits/Normed.lean index c25802286eeec..b1303cc470be5 100644 --- a/Mathlib/Analysis/SpecificLimits/Normed.lean +++ b/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) : diff --git a/Mathlib/Data/Real/GoldenRatio.lean b/Mathlib/Data/Real/GoldenRatio.lean index 2fd3574db29a0..7165e37237c30 100644 --- a/Mathlib/Data/Real/GoldenRatio.lean +++ b/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 diff --git a/Mathlib/FieldTheory/Differential/Basic.lean b/Mathlib/FieldTheory/Differential/Basic.lean index 61fe57fe7c197..05c4742401057 100644 --- 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 index 880ff84e9129d..55112f1e275ed 100644 --- 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 index 7fc53eb7891e7..712e7a66bee25 100644 --- 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