From 09ff17d9bdc80993ca0a4168429680acd31a65b0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Thu, 3 Oct 2024 08:34:01 +0000 Subject: [PATCH] chore: generalise more lemmas from `LinearOrderedField` to `GroupWithZero` (#17359) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ... and move the lemmas from `Algebra.Order.Field.Basic` to `Algebra.Order.GroupWithZero.Unbundled`. Also take the opportunity to add `₀` at the end, per the naming convention. --- Archive/Imo/Imo1972Q5.lean | 4 +- Archive/Imo/Imo1986Q5.lean | 2 +- Mathlib.lean | 1 + .../Computation/ApproximationCorollaries.lean | 4 +- Mathlib/Algebra/Order/Archimedean/Basic.lean | 10 +- Mathlib/Algebra/Order/Field/Basic.lean | 82 +++++------ Mathlib/Algebra/Order/Field/Pointwise.lean | 12 +- Mathlib/Algebra/Order/Floor.lean | 12 +- .../Order/GroupWithZero/Canonical.lean | 6 - .../Order/GroupWithZero/Unbundled.lean | 137 +++++++++++++++++- .../Order/GroupWithZero/Unbundled/Lemmas.lean | 27 ++++ Mathlib/Analysis/Asymptotics/Asymptotics.lean | 4 +- .../Analysis/CStarAlgebra/Unitization.lean | 2 +- .../ApproximatesLinearOn.lean | 2 +- Mathlib/Analysis/Calculus/MeanValue.lean | 2 +- .../Analysis/Calculus/UniformLimitsDeriv.lean | 4 +- Mathlib/Analysis/Complex/AbelLimit.lean | 2 +- Mathlib/Analysis/Complex/Hadamard.lean | 6 +- .../Analysis/Complex/PhragmenLindelof.lean | 2 +- .../Complex/UpperHalfPlane/Metric.lean | 2 +- Mathlib/Analysis/Convex/Body.lean | 2 +- Mathlib/Analysis/Convex/Continuous.lean | 2 +- Mathlib/Analysis/Convex/Deriv.lean | 4 +- Mathlib/Analysis/Convex/Gauge.lean | 8 +- Mathlib/Analysis/Convex/Integral.lean | 2 +- Mathlib/Analysis/Convex/Slope.lean | 4 +- .../Convex/SpecificFunctions/Basic.lean | 33 +++-- .../Analysis/Convex/StrictConvexSpace.lean | 2 +- .../Analysis/Distribution/SchwartzSpace.lean | 4 +- .../Fourier/RiemannLebesgueLemma.lean | 8 +- .../InnerProductSpace/LaxMilgram.lean | 2 +- .../Analysis/LocallyConvex/WithSeminorms.lean | 2 +- Mathlib/Analysis/Normed/Affine/AddTorsor.lean | 2 +- Mathlib/Analysis/Normed/Algebra/Spectrum.lean | 2 +- .../Analysis/Normed/Field/ProperSpace.lean | 2 +- Mathlib/Analysis/Normed/Group/Quotient.lean | 4 +- Mathlib/Analysis/Normed/Module/Basic.lean | 2 +- .../NormedSpace/OperatorNorm/NNNorm.lean | 2 +- Mathlib/Analysis/NormedSpace/Pointwise.lean | 2 +- Mathlib/Analysis/NormedSpace/RieszLemma.lean | 6 +- Mathlib/Analysis/Seminorm.lean | 12 +- .../SpecialFunctions/Complex/Arctan.lean | 2 +- Mathlib/Analysis/SpecialFunctions/Exp.lean | 2 +- .../SpecialFunctions/JapaneseBracket.lean | 2 +- .../Analysis/SpecialFunctions/Log/Base.lean | 2 +- .../Analysis/SpecialFunctions/Log/Basic.lean | 2 +- .../SpecialFunctions/Pow/Complex.lean | 2 +- .../Analysis/SpecialFunctions/Pow/Real.lean | 2 +- .../SpecialFunctions/Trigonometric/Angle.lean | 4 +- .../Trigonometric/Arctan.lean | 2 +- Mathlib/Analysis/SpecificLimits/FloorPow.lean | 2 +- .../Additive/AP/Three/Behrend.lean | 4 +- Mathlib/Combinatorics/Schnirelmann.lean | 2 +- .../SimpleGraph/Regularity/Bound.lean | 4 +- .../SimpleGraph/Regularity/Uniform.lean | 2 +- Mathlib/Data/Complex/Exponential.lean | 4 +- Mathlib/Data/Int/CardIntervalMod.lean | 10 +- Mathlib/Data/NNReal/Basic.lean | 29 ++-- Mathlib/Data/Real/Archimedean.lean | 2 +- Mathlib/Data/Real/Pi/Bounds.lean | 4 +- Mathlib/Data/Real/Pi/Irrational.lean | 4 +- Mathlib/Data/Set/Pointwise/Interval.lean | 8 +- .../Geometry/Manifold/Instances/Sphere.lean | 2 +- Mathlib/Geometry/Manifold/IntegralCurve.lean | 2 +- Mathlib/LinearAlgebra/Matrix/Gershgorin.lean | 2 +- .../Covering/DensityTheorem.lean | 2 +- Mathlib/MeasureTheory/Covering/Vitali.lean | 2 +- .../Function/ConvergenceInMeasure.lean | 2 +- .../Integral/MeanInequalities.lean | 2 +- .../MeasureTheory/Integral/PeakFunction.lean | 2 +- .../Measure/Lebesgue/VolumeOfBalls.lean | 4 +- .../ClassNumber/AdmissibleAbs.lean | 4 +- .../ClassNumber/AdmissibleCardPowDegree.lean | 2 +- .../DiophantineApproximation.lean | 8 +- Mathlib/NumberTheory/Liouville/Basic.lean | 4 +- .../NumberTheory/Liouville/LiouvilleWith.lean | 4 +- Mathlib/NumberTheory/Modular.lean | 4 +- .../CanonicalEmbedding/ConvexBody.lean | 2 +- .../NumberTheory/NumberField/ClassNumber.lean | 2 +- .../NumberField/Discriminant.lean | 4 +- .../NumberField/Units/DirichletTheorem.lean | 2 +- Mathlib/NumberTheory/Padics/Hensel.lean | 2 +- Mathlib/NumberTheory/Rayleigh.lean | 8 +- Mathlib/RingTheory/RootsOfUnity/Complex.lean | 2 +- .../Algebra/Module/FiniteDimension.lean | 2 +- Mathlib/Topology/Algebra/PontryaginDual.lean | 4 +- Mathlib/Topology/ContinuousMap/Ideals.lean | 2 +- 87 files changed, 373 insertions(+), 228 deletions(-) create mode 100644 Mathlib/Algebra/Order/GroupWithZero/Unbundled/Lemmas.lean diff --git a/Archive/Imo/Imo1972Q5.lean b/Archive/Imo/Imo1972Q5.lean index f96965f9d6a75a..ba2e4d8c6a0a07 100644 --- a/Archive/Imo/Imo1972Q5.lean +++ b/Archive/Imo/Imo1972Q5.lean @@ -50,7 +50,7 @@ theorem imo1972_q5 (f g : ℝ → ℝ) (hf1 : ∀ x, ∀ y, f (x + y) + f (x - y calc 0 < ‖f x‖ := norm_pos_iff.mpr hx _ ≤ k := hk₁ x - rw [div_lt_iff] + rw [div_lt_iff₀] · apply lt_mul_of_one_lt_right h₁ hneg · exact zero_lt_one.trans hneg -- Demonstrate that `k ≤ k'` using `hk₂`. @@ -87,7 +87,7 @@ theorem imo1972_q5' (f g : ℝ → ℝ) (hf1 : ∀ x, ∀ y, f (x + y) + f (x - have h : ∀ x, ‖f x‖ ≤ k := le_ciSup hf2 have hgy : 0 < ‖g y‖ := by linarith have k_pos : 0 < k := lt_of_lt_of_le (norm_pos_iff.mpr hx) (h x) - have : k / ‖g y‖ < k := (div_lt_iff hgy).mpr (lt_mul_of_one_lt_right k_pos H) + have : k / ‖g y‖ < k := (div_lt_iff₀ hgy).mpr (lt_mul_of_one_lt_right k_pos H) have : k ≤ k / ‖g y‖ := by suffices ∀ x, ‖f x‖ ≤ k / ‖g y‖ from ciSup_le this intro x diff --git a/Archive/Imo/Imo1986Q5.lean b/Archive/Imo/Imo1986Q5.lean index 6789efcbb837d0..82fe5961c16471 100644 --- a/Archive/Imo/Imo1986Q5.lean +++ b/Archive/Imo/Imo1986Q5.lean @@ -54,7 +54,7 @@ theorem map_of_lt_two (hx : x < 2) : f x = 2 / (2 - x) := by have hx' : 0 < 2 - x := tsub_pos_of_lt hx have hfx : f x ≠ 0 := hf.map_ne_zero_iff.2 hx apply le_antisymm - · rw [le_div_iff₀ hx', ← NNReal.le_div_iff' hfx, tsub_le_iff_right, ← hf.map_eq_zero, + · rw [le_div_iff₀ hx', ← le_div_iff₀' hfx.bot_lt, tsub_le_iff_right, ← hf.map_eq_zero, hf.map_add, div_mul_cancel₀ _ hfx, hf.map_two, zero_mul] · rw [div_le_iff₀' hx', ← hf.map_eq_zero] refine (mul_eq_zero.1 ?_).resolve_right hfx diff --git a/Mathlib.lean b/Mathlib.lean index 128adb94db271d..22ea50c9663f9e 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -610,6 +610,7 @@ import Mathlib.Algebra.Order.GroupWithZero.Canonical import Mathlib.Algebra.Order.GroupWithZero.Submonoid import Mathlib.Algebra.Order.GroupWithZero.Synonym import Mathlib.Algebra.Order.GroupWithZero.Unbundled +import Mathlib.Algebra.Order.GroupWithZero.Unbundled.Lemmas import Mathlib.Algebra.Order.GroupWithZero.WithZero import Mathlib.Algebra.Order.Hom.Basic import Mathlib.Algebra.Order.Hom.Monoid diff --git a/Mathlib/Algebra/ContinuedFractions/Computation/ApproximationCorollaries.lean b/Mathlib/Algebra/ContinuedFractions/Computation/ApproximationCorollaries.lean index 34d81f490bea6e..73f695ecae794e 100644 --- a/Mathlib/Algebra/ContinuedFractions/Computation/ApproximationCorollaries.lean +++ b/Mathlib/Algebra/ContinuedFractions/Computation/ApproximationCorollaries.lean @@ -97,9 +97,9 @@ theorem of_convergence_epsilon : have zero_lt_B : 0 < B := B_ineq.trans_lt' <| mod_cast fib_pos.2 n.succ_pos have nB_pos : 0 < nB := nB_ineq.trans_lt' <| mod_cast fib_pos.2 <| succ_pos _ have zero_lt_mul_conts : 0 < B * nB := by positivity - suffices 1 < ε * (B * nB) from (div_lt_iff zero_lt_mul_conts).mpr this + suffices 1 < ε * (B * nB) from (div_lt_iff₀ zero_lt_mul_conts).mpr this -- use that `N' ≥ n` was obtained from the archimedean property to show the following - calc 1 < ε * (N' : K) := (div_lt_iff' ε_pos).mp one_div_ε_lt_N' + calc 1 < ε * (N' : K) := (div_lt_iff₀' ε_pos).mp one_div_ε_lt_N' _ ≤ ε * (B * nB) := ?_ -- cancel `ε` gcongr diff --git a/Mathlib/Algebra/Order/Archimedean/Basic.lean b/Mathlib/Algebra/Order/Archimedean/Basic.lean index 8706c7c0c0d174..c9b87a14420e89 100644 --- a/Mathlib/Algebra/Order/Archimedean/Basic.lean +++ b/Mathlib/Algebra/Order/Archimedean/Basic.lean @@ -223,7 +223,7 @@ variable [LinearOrderedSemifield α] [Archimedean α] {x y ε : α} lemma exists_nat_one_div_lt (hε : 0 < ε) : ∃ n : ℕ, 1 / (n + 1 : α) < ε := by cases' exists_nat_gt (1 / ε) with n hn use n - rw [div_lt_iff, ← div_lt_iff' hε] + rw [div_lt_iff₀, ← div_lt_iff₀' hε] · apply hn.trans simp [zero_lt_one] · exact n.cast_add_one_pos @@ -299,11 +299,11 @@ theorem exists_rat_btwn {x y : α} (h : x < y) : ∃ q : ℚ, x < q ∧ (q : α) refine ⟨(z + 1 : ℤ) / n, ?_⟩ have n0' := (inv_pos.2 (sub_pos.2 h)).trans nh have n0 := Nat.cast_pos.1 n0' - rw [Rat.cast_div_of_ne_zero, Rat.cast_natCast, Rat.cast_intCast, div_lt_iff n0'] - · refine ⟨(lt_div_iff n0').2 <| (lt_iff_lt_of_le_iff_le (zh _)).1 (lt_add_one _), ?_⟩ + rw [Rat.cast_div_of_ne_zero, Rat.cast_natCast, Rat.cast_intCast, div_lt_iff₀ n0'] + · refine ⟨(lt_div_iff₀ n0').2 <| (lt_iff_lt_of_le_iff_le (zh _)).1 (lt_add_one _), ?_⟩ rw [Int.cast_add, Int.cast_one] refine lt_of_le_of_lt (add_le_add_right ((zh _).1 le_rfl) _) ?_ - rwa [← lt_sub_iff_add_lt', ← sub_mul, ← div_lt_iff' (sub_pos.2 h), one_div] + rwa [← lt_sub_iff_add_lt', ← sub_mul, ← div_lt_iff₀' (sub_pos.2 h), one_div] · rw [Rat.den_intCast, Nat.cast_one] exact one_ne_zero · intro H @@ -352,7 +352,7 @@ variable [LinearOrderedField α] theorem archimedean_iff_nat_lt : Archimedean α ↔ ∀ x : α, ∃ n : ℕ, x < n := ⟨@exists_nat_gt α _, fun H => ⟨fun x y y0 => - (H (x / y)).imp fun n h => le_of_lt <| by rwa [div_lt_iff y0, ← nsmul_eq_mul] at h⟩⟩ + (H (x / y)).imp fun n h => le_of_lt <| by rwa [div_lt_iff₀ y0, ← nsmul_eq_mul] at h⟩⟩ theorem archimedean_iff_nat_le : Archimedean α ↔ ∀ x : α, ∃ n : ℕ, x ≤ n := archimedean_iff_nat_lt.trans diff --git a/Mathlib/Algebra/Order/Field/Basic.lean b/Mathlib/Algebra/Order/Field/Basic.lean index 2385c27aac0327..72a133e1ff7a77 100644 --- a/Mathlib/Algebra/Order/Field/Basic.lean +++ b/Mathlib/Algebra/Order/Field/Basic.lean @@ -5,6 +5,7 @@ Authors: Robert Y. Lewis, Leonardo de Moura, Mario Carneiro, Floris van Doorn -/ import Mathlib.Algebra.CharZero.Lemmas import Mathlib.Algebra.Order.Field.Defs +import Mathlib.Algebra.Order.GroupWithZero.Unbundled.Lemmas import Mathlib.Algebra.Order.Ring.Abs import Mathlib.Order.Bounds.OrderIso import Mathlib.Tactic.Bound.Attribute @@ -23,55 +24,46 @@ section LinearOrderedSemifield variable [LinearOrderedSemifield α] {a b c d e : α} {m n : ℤ} -/-- `Equiv.mulLeft₀` as an order_iso. -/ -@[simps! (config := { simpRhs := true })] -def OrderIso.mulLeft₀ (a : α) (ha : 0 < a) : α ≃o α := - { Equiv.mulLeft₀ a ha.ne' with map_rel_iff' := @fun _ _ => mul_le_mul_left ha } - -/-- `Equiv.mulRight₀` as an order_iso. -/ -@[simps! (config := { simpRhs := true })] -def OrderIso.mulRight₀ (a : α) (ha : 0 < a) : α ≃o α := - { Equiv.mulRight₀ a ha.ne' with map_rel_iff' := @fun _ _ => mul_le_mul_right ha } - /-! ### Relating one division with another term. -/ -theorem lt_div_iff (hc : 0 < c) : a < b / c ↔ a * c < b := - lt_iff_lt_of_le_iff_le <| div_le_iff₀ hc - -theorem lt_div_iff' (hc : 0 < c) : a < b / c ↔ c * a < b := by rw [mul_comm, lt_div_iff hc] - -theorem div_lt_iff (hc : 0 < c) : b / c < a ↔ b < a * c := - lt_iff_lt_of_le_iff_le (le_div_iff₀ hc) +@[deprecated lt_div_iff₀ (since := "2024-10-02")] +theorem lt_div_iff (hc : 0 < c) : a < b / c ↔ a * c < b := lt_div_iff₀ hc -theorem div_lt_iff' (hc : 0 < c) : b / c < a ↔ b < c * a := by rw [mul_comm, div_lt_iff hc] +@[deprecated lt_div_iff₀' (since := "2024-10-02")] +theorem lt_div_iff' (hc : 0 < c) : a < b / c ↔ c * a < b := lt_div_iff₀' hc -lemma div_lt_comm₀ (hb : 0 < b) (hc : 0 < c) : a / b < c ↔ a / c < b := by - rw [div_lt_iff hb, div_lt_iff' hc] +@[deprecated div_lt_iff₀ (since := "2024-10-02")] +theorem div_lt_iff (hc : 0 < c) : b / c < a ↔ b < a * c := div_lt_iff₀ hc -theorem inv_mul_le_iff (h : 0 < b) : b⁻¹ * a ≤ c ↔ a ≤ b * c := by - rw [inv_eq_one_div, mul_comm, ← div_eq_mul_one_div] - exact div_le_iff₀' h +@[deprecated div_lt_iff₀' (since := "2024-10-02")] +theorem div_lt_iff' (hc : 0 < c) : b / c < a ↔ b < c * a := div_lt_iff₀' hc -theorem inv_mul_le_iff' (h : 0 < b) : b⁻¹ * a ≤ c ↔ a ≤ c * b := by rw [inv_mul_le_iff h, mul_comm] +@[deprecated inv_mul_le_iff₀ (since := "2024-10-02")] +theorem inv_mul_le_iff (h : 0 < b) : b⁻¹ * a ≤ c ↔ a ≤ b * c := inv_mul_le_iff₀ h -theorem mul_inv_le_iff (h : 0 < b) : a * b⁻¹ ≤ c ↔ a ≤ b * c := by rw [mul_comm, inv_mul_le_iff h] +set_option linter.docPrime false in +@[deprecated inv_mul_le_iff₀' (since := "2024-10-02")] +theorem inv_mul_le_iff' (h : 0 < b) : b⁻¹ * a ≤ c ↔ a ≤ c * b := inv_mul_le_iff₀' h -theorem mul_inv_le_iff' (h : 0 < b) : a * b⁻¹ ≤ c ↔ a ≤ c * b := by rw [mul_comm, inv_mul_le_iff' h] +@[deprecated mul_inv_le_iff₀' (since := "2024-10-02")] +theorem mul_inv_le_iff (h : 0 < b) : a * b⁻¹ ≤ c ↔ a ≤ b * c := mul_inv_le_iff₀' h -theorem div_self_le_one (a : α) : a / a ≤ 1 := - if h : a = 0 then by simp [h] else by simp [h] +@[deprecated mul_inv_le_iff₀ (since := "2024-10-02")] +theorem mul_inv_le_iff' (h : 0 < b) : a * b⁻¹ ≤ c ↔ a ≤ c * b := mul_inv_le_iff₀ h -theorem inv_mul_lt_iff (h : 0 < b) : b⁻¹ * a < c ↔ a < b * c := by - rw [inv_eq_one_div, mul_comm, ← div_eq_mul_one_div] - exact div_lt_iff' h +@[deprecated inv_mul_lt_iff₀ (since := "2024-10-02")] +theorem inv_mul_lt_iff (h : 0 < b) : b⁻¹ * a < c ↔ a < b * c := inv_mul_lt_iff₀ h -theorem inv_mul_lt_iff' (h : 0 < b) : b⁻¹ * a < c ↔ a < c * b := by rw [inv_mul_lt_iff h, mul_comm] +@[deprecated inv_mul_lt_iff₀' (since := "2024-10-02")] +theorem inv_mul_lt_iff' (h : 0 < b) : b⁻¹ * a < c ↔ a < c * b := inv_mul_lt_iff₀' h -theorem mul_inv_lt_iff (h : 0 < b) : a * b⁻¹ < c ↔ a < b * c := by rw [mul_comm, inv_mul_lt_iff h] +@[deprecated mul_inv_lt_iff₀' (since := "2024-10-02")] +theorem mul_inv_lt_iff (h : 0 < b) : a * b⁻¹ < c ↔ a < b * c := mul_inv_lt_iff₀' h -theorem mul_inv_lt_iff' (h : 0 < b) : a * b⁻¹ < c ↔ a < c * b := by rw [mul_comm, inv_mul_lt_iff' h] +@[deprecated mul_inv_lt_iff₀ (since := "2024-10-02")] +theorem mul_inv_lt_iff' (h : 0 < b) : a * b⁻¹ < c ↔ a < c * b := mul_inv_lt_iff₀ h theorem inv_pos_le_iff_one_le_mul (ha : 0 < a) : a⁻¹ ≤ b ↔ 1 ≤ b * a := by rw [inv_eq_one_div] @@ -83,11 +75,11 @@ theorem inv_pos_le_iff_one_le_mul' (ha : 0 < a) : a⁻¹ ≤ b ↔ 1 ≤ a * b : theorem inv_pos_lt_iff_one_lt_mul (ha : 0 < a) : a⁻¹ < b ↔ 1 < b * a := by rw [inv_eq_one_div] - exact div_lt_iff ha + exact div_lt_iff₀ ha theorem inv_pos_lt_iff_one_lt_mul' (ha : 0 < a) : a⁻¹ < b ↔ 1 < a * b := by rw [inv_eq_one_div] - exact div_lt_iff' ha + exact div_lt_iff₀' ha /-- One direction of `div_le_iff` where `b` is allowed to be `0` (but `c` must be nonnegative) -/ theorem div_le_of_nonneg_of_le_mul (hb : 0 ≤ b) (hc : 0 ≤ c) (h : a ≤ c * b) : a / b ≤ c := by @@ -237,7 +229,7 @@ theorem div_le_div_left (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a / b ≤ a / c le_iff_le_iff_lt_iff_lt.2 (div_lt_div_left ha hc hb) theorem div_lt_div_iff (b0 : 0 < b) (d0 : 0 < d) : a / b < c / d ↔ a * d < c * b := by - rw [lt_div_iff d0, div_mul_eq_mul_div, div_lt_iff b0] + rw [lt_div_iff₀ d0, div_mul_eq_mul_div, div_lt_iff₀ b0] theorem div_le_div_iff (b0 : 0 < b) (d0 : 0 < d) : a / b ≤ c / d ↔ a * d ≤ c * b := by rw [le_div_iff₀ d0, div_mul_eq_mul_div, div_le_iff₀ b0] @@ -275,9 +267,9 @@ theorem one_le_div (hb : 0 < b) : 1 ≤ a / b ↔ b ≤ a := by rw [le_div_iff theorem div_le_one (hb : 0 < b) : a / b ≤ 1 ↔ a ≤ b := by rw [div_le_iff₀ hb, one_mul] -theorem one_lt_div (hb : 0 < b) : 1 < a / b ↔ b < a := by rw [lt_div_iff hb, one_mul] +theorem one_lt_div (hb : 0 < b) : 1 < a / b ↔ b < a := by rw [lt_div_iff₀ hb, one_mul] -theorem div_lt_one (hb : 0 < b) : a / b < 1 ↔ a < b := by rw [div_lt_iff hb, one_mul] +theorem div_lt_one (hb : 0 < b) : a / b < 1 ↔ a < b := by rw [div_lt_iff₀ hb, one_mul] theorem one_div_le (ha : 0 < a) (hb : 0 < b) : 1 / a ≤ b ↔ 1 / b ≤ a := by simpa using inv_le ha hb @@ -300,7 +292,7 @@ theorem one_div_le_one_div_of_le (ha : 0 < a) (h : a ≤ b) : 1 / b ≤ 1 / a := simpa using inv_le_inv_of_le ha h theorem one_div_lt_one_div_of_lt (ha : 0 < a) (h : a < b) : 1 / b < 1 / a := by - rwa [lt_div_iff' ha, ← div_eq_mul_one_div, div_lt_one (ha.trans h)] + rwa [lt_div_iff₀' ha, ← div_eq_mul_one_div, div_lt_one (ha.trans h)] theorem le_of_one_div_le_one_div (ha : 0 < a) (h : 1 / a ≤ 1 / b) : b ≤ a := le_imp_le_of_lt_imp_lt (one_div_lt_one_div_of_lt ha) h @@ -341,7 +333,7 @@ theorem half_le_self_iff : a / 2 ≤ a ↔ 0 ≤ a := by @[simp] theorem half_lt_self_iff : a / 2 < a ↔ 0 < a := by - rw [div_lt_iff (zero_lt_two' α), mul_two, lt_add_iff_pos_left] + rw [div_lt_iff₀ (zero_lt_two' α), mul_two, lt_add_iff_pos_left] alias ⟨_, half_le_self⟩ := half_le_self_iff @@ -355,9 +347,9 @@ theorem one_half_lt_one : (1 / 2 : α) < 1 := theorem two_inv_lt_one : (2⁻¹ : α) < 1 := (one_div _).symm.trans_lt one_half_lt_one -theorem left_lt_add_div_two : a < (a + b) / 2 ↔ a < b := by simp [lt_div_iff, mul_two] +theorem left_lt_add_div_two : a < (a + b) / 2 ↔ a < b := by simp [lt_div_iff₀, mul_two] -theorem add_div_two_lt_right : (a + b) / 2 < b ↔ a < b := by simp [div_lt_iff, mul_two] +theorem add_div_two_lt_right : (a + b) / 2 < b ↔ a < b := by simp [div_lt_iff₀, mul_two] theorem add_thirds (a : α) : a / 3 + a / 3 + a / 3 = a := by rw [div_add_div_same, div_add_div_same, ← two_mul, ← add_one_mul 2 a, two_add_one_eq_three, @@ -385,12 +377,12 @@ theorem div_mul_le_div_mul_of_div_le_div (h : a / b ≤ c / d) (he : 0 ≤ e) : theorem exists_pos_mul_lt {a : α} (h : 0 < a) (b : α) : ∃ c : α, 0 < c ∧ b * c < a := by have : 0 < a / max (b + 1) 1 := div_pos h (lt_max_iff.2 (Or.inr zero_lt_one)) refine ⟨a / max (b + 1) 1, this, ?_⟩ - rw [← lt_div_iff this, div_div_cancel' h.ne'] + rw [← lt_div_iff₀ this, div_div_cancel' h.ne'] exact lt_max_iff.2 (Or.inl <| lt_add_one _) theorem exists_pos_lt_mul {a : α} (h : 0 < a) (b : α) : ∃ c : α, 0 < c ∧ b < c * a := let ⟨c, hc₀, hc⟩ := exists_pos_mul_lt h b; - ⟨c⁻¹, inv_pos.2 hc₀, by rwa [← div_eq_inv_mul, lt_div_iff hc₀]⟩ + ⟨c⁻¹, inv_pos.2 hc₀, by rwa [← div_eq_inv_mul, lt_div_iff₀ hc₀]⟩ lemma monotone_div_right_of_nonneg (ha : 0 ≤ a) : Monotone (· / a) := fun _b _c hbc ↦ div_le_div_of_nonneg_right hbc ha diff --git a/Mathlib/Algebra/Order/Field/Pointwise.lean b/Mathlib/Algebra/Order/Field/Pointwise.lean index 0b5b49e3c6bb96..01d4453c225239 100644 --- a/Mathlib/Algebra/Order/Field/Pointwise.lean +++ b/Mathlib/Algebra/Order/Field/Pointwise.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Alex J. Best, Yaël Dillies -/ import Mathlib.Algebra.Group.Pointwise.Set.Basic -import Mathlib.Algebra.Order.Field.Basic +import Mathlib.Algebra.Order.Field.Defs import Mathlib.Algebra.SMulWithZero /-! @@ -33,7 +33,7 @@ theorem smul_Ioo : r • Ioo a b = Ioo (r • a) (r • b) := by · exact (mul_lt_mul_left hr).mpr a_h_left_right · rintro ⟨a_left, a_right⟩ use x / r - refine ⟨⟨(lt_div_iff' hr).mpr a_left, (div_lt_iff' hr).mpr a_right⟩, ?_⟩ + refine ⟨⟨(lt_div_iff₀' hr).mpr a_left, (div_lt_iff₀' hr).mpr a_right⟩, ?_⟩ rw [mul_div_cancel₀ _ (ne_of_gt hr)] theorem smul_Icc : r • Icc a b = Icc (r • a) (r • b) := by @@ -59,7 +59,7 @@ theorem smul_Ico : r • Ico a b = Ico (r • a) (r • b) := by · exact (mul_lt_mul_left hr).mpr a_h_left_right · rintro ⟨a_left, a_right⟩ use x / r - refine ⟨⟨(le_div_iff₀' hr).mpr a_left, (div_lt_iff' hr).mpr a_right⟩, ?_⟩ + refine ⟨⟨(le_div_iff₀' hr).mpr a_left, (div_lt_iff₀' hr).mpr a_right⟩, ?_⟩ rw [mul_div_cancel₀ _ (ne_of_gt hr)] theorem smul_Ioc : r • Ioc a b = Ioc (r • a) (r • b) := by @@ -72,7 +72,7 @@ theorem smul_Ioc : r • Ioc a b = Ioc (r • a) (r • b) := by · exact (mul_le_mul_left hr).mpr a_h_left_right · rintro ⟨a_left, a_right⟩ use x / r - refine ⟨⟨(lt_div_iff' hr).mpr a_left, (div_le_iff₀' hr).mpr a_right⟩, ?_⟩ + refine ⟨⟨(lt_div_iff₀' hr).mpr a_left, (div_le_iff₀' hr).mpr a_right⟩, ?_⟩ rw [mul_div_cancel₀ _ (ne_of_gt hr)] theorem smul_Ioi : r • Ioi a = Ioi (r • a) := by @@ -84,7 +84,7 @@ theorem smul_Ioi : r • Ioi a = Ioi (r • a) := by · rintro h use x / r constructor - · exact (lt_div_iff' hr).mpr h + · exact (lt_div_iff₀' hr).mpr h · exact mul_div_cancel₀ _ (ne_of_gt hr) theorem smul_Iio : r • Iio a = Iio (r • a) := by @@ -96,7 +96,7 @@ theorem smul_Iio : r • Iio a = Iio (r • a) := by · rintro h use x / r constructor - · exact (div_lt_iff' hr).mpr h + · exact (div_lt_iff₀' hr).mpr h · exact mul_div_cancel₀ _ (ne_of_gt hr) theorem smul_Ici : r • Ici a = Ici (r • a) := by diff --git a/Mathlib/Algebra/Order/Floor.lean b/Mathlib/Algebra/Order/Floor.lean index a3689333018fb7..18797cc6170d3f 100644 --- a/Mathlib/Algebra/Order/Floor.lean +++ b/Mathlib/Algebra/Order/Floor.lean @@ -484,7 +484,7 @@ theorem floor_div_nat (a : α) (n : ℕ) : ⌊a / n⌋₊ = ⌊a⌋₊ / n := by · exact div_nonneg ha n.cast_nonneg constructor · exact cast_div_le.trans (div_le_div_of_nonneg_right (floor_le ha) n.cast_nonneg) - rw [div_lt_iff, add_mul, one_mul, ← cast_mul, ← cast_add, ← floor_lt ha] + rw [div_lt_iff₀, add_mul, one_mul, ← cast_mul, ← cast_add, ← floor_lt ha] · exact lt_div_mul_add hn · exact cast_pos.2 hn @@ -515,7 +515,7 @@ lemma ceil_lt_mul (hb : 1 < b) (hba : ⌈(b - 1)⁻¹⌉₊ / b < a) : ⌈a⌉ obtain hab | hba := le_total a (b - 1)⁻¹ · calc ⌈a⌉₊ ≤ (⌈(b - 1)⁻¹⌉₊ : α) := by gcongr - _ < b * a := by rwa [← div_lt_iff']; positivity + _ < b * a := by rwa [← div_lt_iff₀']; positivity · rw [← sub_pos] at hb calc ⌈a⌉₊ < a + 1 := ceil_lt_add_one <| hba.trans' <| by positivity @@ -1027,7 +1027,7 @@ theorem sub_floor_div_mul_nonneg (a : k) (hb : 0 < b) : 0 ≤ a - ⌊a / b⌋ * theorem sub_floor_div_mul_lt (a : k) (hb : 0 < b) : a - ⌊a / b⌋ * b < b := sub_lt_iff_lt_add.2 <| by -- Porting note: `← one_add_mul` worked in mathlib3 without the argument - rw [← one_add_mul _ b, ← div_lt_iff hb, add_comm] + rw [← one_add_mul _ b, ← div_lt_iff₀ hb, add_comm] exact lt_floor_add_one _ theorem fract_div_natCast_eq_div_natCast_mod {m n : ℕ} : fract ((m : k) / n) = ↑(m % n) / n := by @@ -1261,7 +1261,7 @@ lemma ceil_div_ceil_inv_sub_one (ha : 1 ≤ a) : ⌈⌈(a - 1)⁻¹⌉ / a⌉ = have : 0 < ⌈(a - 1)⁻¹⌉ := ceil_pos.2 <| by positivity refine le_antisymm (ceil_le.2 <| div_le_self (by positivity) ha.le) <| ?_ rw [le_ceil_iff, sub_lt_comm, div_eq_mul_inv, ← mul_one_sub, - ← lt_div_iff (sub_pos.2 <| inv_lt_one ha)] + ← lt_div_iff₀ (sub_pos.2 <| inv_lt_one ha)] convert ceil_lt_add_one _ using 1 field_simp @@ -1269,7 +1269,7 @@ lemma ceil_lt_mul (hb : 1 < b) (hba : ⌈(b - 1)⁻¹⌉ / b < a) : ⌈a⌉ < b obtain hab | hba := le_total a (b - 1)⁻¹ · calc ⌈a⌉ ≤ (⌈(b - 1)⁻¹⌉ : k) := by gcongr - _ < b * a := by rwa [← div_lt_iff']; positivity + _ < b * a := by rwa [← div_lt_iff₀']; positivity · rw [← sub_pos] at hb calc ⌈a⌉ < a + 1 := ceil_lt_add_one _ @@ -1453,7 +1453,7 @@ section LinearOrderedField variable [LinearOrderedField α] [FloorRing α] theorem round_eq (x : α) : round x = ⌊x + 1 / 2⌋ := by - simp_rw [round, (by simp only [lt_div_iff', two_pos] : 2 * fract x < 1 ↔ fract x < 1 / 2)] + simp_rw [round, (by simp only [lt_div_iff₀', two_pos] : 2 * fract x < 1 ↔ fract x < 1 / 2)] cases' lt_or_le (fract x) (1 / 2) with hx hx · conv_rhs => rw [← fract_add_floor x, add_assoc, add_left_comm, floor_int_add] rw [if_pos hx, self_eq_add_right, floor_eq_iff, cast_zero, zero_add] diff --git a/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean b/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean index f8df22be3c53e0..cabc69bb601813 100644 --- a/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean +++ b/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean @@ -185,12 +185,6 @@ theorem inv_mul_lt_of_lt_mul₀ (h : a < b * c) : b⁻¹ * a < c := by theorem mul_lt_right₀ (c : α) (h : a < b) (hc : c ≠ 0) : a * c < b * c := mul_lt_mul_of_pos_right h (zero_lt_iff.2 hc) -theorem inv_lt_one₀ (ha : a ≠ 0) : a⁻¹ < 1 ↔ 1 < a := - inv_lt_one' (a := Units.mk0 a ha) - -theorem one_lt_inv₀ (ha : a ≠ 0) : 1 < a⁻¹ ↔ a < 1 := - one_lt_inv' (a := Units.mk0 a ha) - theorem inv_lt_inv₀ (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ < b⁻¹ ↔ b < a := show (Units.mk0 a ha)⁻¹ < (Units.mk0 b hb)⁻¹ ↔ Units.mk0 b hb < Units.mk0 a ha from have : CovariantClass αˣ αˣ (· * ·) (· < ·) := diff --git a/Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean b/Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean index ce7ed361fd599a..2b57798b2b4fd5 100644 --- a/Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean +++ b/Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean @@ -1113,6 +1113,14 @@ end CancelMonoidWithZero section GroupWithZero variable [GroupWithZero G₀] +section Preorder +variable [Preorder G₀] [ZeroLEOneClass G₀] + +/-- See `div_self` for the version with equality when `a ≠ 0`. -/ +lemma div_self_le_one (a : G₀) : a / a ≤ 1 := by obtain rfl | ha := eq_or_ne a 0 <;> simp [*] + +end Preorder + section PartialOrder variable [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b c d : G₀} @@ -1149,10 +1157,12 @@ lemma zpow_pos_of_pos [PosMulStrictMono G₀] (ha : 0 < a) : ∀ n : ℤ, 0 < a section PosMulMono variable [PosMulMono G₀] +/-- See `le_inv_mul_iff₀'` for a version with multiplication on the other side. -/ lemma le_inv_mul_iff₀ (hc : 0 < c) : a ≤ c⁻¹ * b ↔ c * a ≤ b where mp h := by simpa [hc.ne'] using mul_le_mul_of_nonneg_left h hc.le mpr h := by simpa [hc.ne'] using mul_le_mul_of_nonneg_left h (inv_nonneg.2 hc.le) +/-- See `inv_mul_le_iff₀'` for a version with multiplication on the other side. -/ lemma inv_mul_le_iff₀ (hc : 0 < c) : c⁻¹ * b ≤ a ↔ b ≤ c * a where mp h := by simpa [hc.ne'] using mul_le_mul_of_nonneg_left h hc.le mpr h := by simpa [hc.ne'] using mul_le_mul_of_nonneg_left h (inv_nonneg.2 hc.le) @@ -1168,17 +1178,21 @@ end PosMulMono section MulPosMono variable [MulPosMono G₀] +/-- See `le_mul_inv_iff₀'` for a version with multiplication on the other side. -/ lemma le_mul_inv_iff₀ (hc : 0 < c) : a ≤ b * c⁻¹ ↔ a * c ≤ b where mp h := by simpa [hc.ne'] using mul_le_mul_of_nonneg_right h hc.le mpr h := by simpa [hc.ne'] using mul_le_mul_of_nonneg_right h (inv_nonneg.2 hc.le) +/-- See `mul_inv_le_iff₀'` for a version with multiplication on the other side. -/ lemma mul_inv_le_iff₀ (hc : 0 < c) : b * c⁻¹ ≤ a ↔ b ≤ a * c where mp h := by simpa [hc.ne'] using mul_le_mul_of_nonneg_right h hc.le mpr h := by simpa [hc.ne'] using mul_le_mul_of_nonneg_right h (inv_nonneg.2 hc.le) +/-- See `le_div_iff₀'` for a version with multiplication on the other side. -/ lemma le_div_iff₀ (hc : 0 < c) : a ≤ b / c ↔ a * c ≤ b := by rw [div_eq_mul_inv, le_mul_inv_iff₀ hc] +/-- See `div_le_iff₀'` for a version with multiplication on the other side. -/ lemma div_le_iff₀ (hc : 0 < c) : b / c ≤ a ↔ b ≤ a * c := by rw [div_eq_mul_inv, mul_inv_le_iff₀ hc] @@ -1189,6 +1203,50 @@ lemma div_le_one₀ (hb : 0 < b) : a / b ≤ 1 ↔ a ≤ b := by rw [div_le_iff @[deprecated (since := "2024-08-21")] alias div_le_iff := div_le_iff₀ end MulPosMono + +section PosMulStrictMono +variable [PosMulStrictMono G₀] + +/-- See `lt_inv_mul_iff₀'` for a version with multiplication on the other side. -/ +lemma lt_inv_mul_iff₀ (hc : 0 < c) : a < c⁻¹ * b ↔ c * a < b where + mp h := by simpa [hc.ne'] using mul_lt_mul_of_pos_left h hc + mpr h := by simpa [hc.ne'] using mul_lt_mul_of_pos_left h (inv_pos.2 hc) + +/-- See `inv_mul_lt_iff₀'` for a version with multiplication on the other side. -/ +lemma inv_mul_lt_iff₀ (hc : 0 < c) : c⁻¹ * b < a ↔ b < c * a where + mp h := by simpa [hc.ne'] using mul_lt_mul_of_pos_left h hc + mpr h := by simpa [hc.ne'] using mul_lt_mul_of_pos_left h (inv_pos.2 hc) + +lemma one_lt_inv_mul₀ (ha : 0 < a) : 1 < a⁻¹ * b ↔ a < b := by rw [lt_inv_mul_iff₀ ha, mul_one] +lemma inv_mul_lt_one₀ (ha : 0 < a) : a⁻¹ * b < 1 ↔ b < a := by rw [inv_mul_lt_iff₀ ha, mul_one] + +lemma one_lt_inv₀ (ha : 0 < a) : 1 < a⁻¹ ↔ a < 1 := by simpa using one_lt_inv_mul₀ ha (b := 1) +lemma inv_lt_one₀ (ha : 0 < a) : a⁻¹ < 1 ↔ 1 < a := by simpa using inv_mul_lt_one₀ ha (b := 1) + +end PosMulStrictMono + +section MulPosStrictMono +variable [MulPosStrictMono G₀] + +/-- See `lt_mul_inv_iff₀'` for a version with multiplication on the other side. -/ +lemma lt_mul_inv_iff₀ (hc : 0 < c) : a < b * c⁻¹ ↔ a * c < b where + mp h := by simpa [hc.ne'] using mul_lt_mul_of_pos_right h hc + mpr h := by simpa [hc.ne'] using mul_lt_mul_of_pos_right h (inv_pos.2 hc) + +/-- See `mul_inv_lt_iff₀'` for a version with multiplication on the other side. -/ +lemma mul_inv_lt_iff₀ (hc : 0 < c) : b * c⁻¹ < a ↔ b < a * c where + mp h := by simpa [hc.ne'] using mul_lt_mul_of_pos_right h hc + mpr h := by simpa [hc.ne'] using mul_lt_mul_of_pos_right h (inv_pos.2 hc) + +/-- See `lt_div_iff₀'` for a version with multiplication on the other side. -/ +lemma lt_div_iff₀ (hc : 0 < c) : a < b / c ↔ a * c < b := by + rw [div_eq_mul_inv, lt_mul_inv_iff₀ hc] + +/-- See `div_le_iff₀'` for a version with multiplication on the other side. -/ +lemma div_lt_iff₀ (hc : 0 < c) : b / c < a ↔ b < a * c := by + rw [div_eq_mul_inv, mul_inv_lt_iff₀ hc] + +end MulPosStrictMono end PartialOrder section LinearOrder @@ -1227,22 +1285,95 @@ end CommSemigroupHasZero section CommGroupWithZero variable [CommGroupWithZero G₀] -variable [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] [MulPosMono G₀] {a b c d : G₀} +variable [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] + +section PosMulMono +variable [PosMulMono G₀] {a b c d : G₀} + +/-- See `le_inv_mul_iff₀` for a version with multiplication on the other side. -/ +lemma le_inv_mul_iff₀' (hc : 0 < c) : a ≤ c⁻¹ * b ↔ c * a ≤ b := by + rw [le_inv_mul_iff₀ hc, mul_comm] + +/-- See `inv_mul_le_iff₀` for a version with multiplication on the other side. -/ +lemma inv_mul_le_iff₀' (hc : 0 < c) : c⁻¹ * b ≤ a ↔ b ≤ a * c := by + rw [inv_mul_le_iff₀ hc, mul_comm] + +/-- See `le_mul_inv_iff₀` for a version with multiplication on the other side. -/ +lemma le_mul_inv_iff₀' (hc : 0 < c) : a ≤ b * c⁻¹ ↔ c * a ≤ b := by + have := posMulMono_iff_mulPosMono.1 ‹_› + rw [le_mul_inv_iff₀ hc, mul_comm] + +/-- See `mul_inv_le_iff₀` for a version with multiplication on the other side. -/ +lemma mul_inv_le_iff₀' (hc : 0 < c) : b * c⁻¹ ≤ a ↔ b ≤ c * a := by + have := posMulMono_iff_mulPosMono.1 ‹_› + rw [mul_inv_le_iff₀ hc, mul_comm] lemma div_le_div₀ (hb : 0 < b) (hd : 0 < d) : a / b ≤ c / d ↔ a * d ≤ c * b := by + have := posMulMono_iff_mulPosMono.1 ‹_› rw [div_le_iff₀ hb, ← mul_div_right_comm, le_div_iff₀ hd] -lemma le_div_iff₀' (hc : 0 < c) : a ≤ b / c ↔ c * a ≤ b := by rw [le_div_iff₀ hc, mul_comm] -lemma div_le_iff₀' (hc : 0 < c) : b / c ≤ a ↔ b ≤ c * a := by rw [div_le_iff₀ hc, mul_comm] +/-- See `le_div_iff₀` for a version with multiplication on the other side. -/ +lemma le_div_iff₀' (hc : 0 < c) : a ≤ b / c ↔ c * a ≤ b := by + have := posMulMono_iff_mulPosMono.1 ‹_› + rw [le_div_iff₀ hc, mul_comm] + +/-- See `div_le_iff₀` for a version with multiplication on the other side. -/ +lemma div_le_iff₀' (hc : 0 < c) : b / c ≤ a ↔ b ≤ c * a := by + have := posMulMono_iff_mulPosMono.1 ‹_› + rw [div_le_iff₀ hc, mul_comm] lemma le_div_comm₀ (ha : 0 < a) (hc : 0 < c) : a ≤ b / c ↔ c ≤ b / a := by + have := posMulMono_iff_mulPosMono.1 ‹_› rw [le_div_iff₀ ha, le_div_iff₀' hc] lemma div_le_comm₀ (hb : 0 < b) (hc : 0 < c) : a / b ≤ c ↔ a / c ≤ b := by + have := posMulMono_iff_mulPosMono.1 ‹_› rw [div_le_iff₀ hb, div_le_iff₀' hc] @[deprecated (since := "2024-08-21")] alias le_div_iff' := le_div_iff₀' @[deprecated (since := "2024-08-21")] alias div_le_iff' := div_le_iff₀' +end PosMulMono + +section PosMulStrictMono +variable [PosMulStrictMono G₀] {a b c : G₀} + +/-- See `lt_inv_mul_iff₀` for a version with multiplication on the other side. -/ +lemma lt_inv_mul_iff₀' (hc : 0 < c) : a < c⁻¹ * b ↔ a * c < b := by + rw [lt_inv_mul_iff₀ hc, mul_comm] + +/-- See `inv_mul_lt_iff₀` for a version with multiplication on the other side. -/ +lemma inv_mul_lt_iff₀' (hc : 0 < c) : c⁻¹ * b < a ↔ b < a * c := by + rw [inv_mul_lt_iff₀ hc, mul_comm] + +/-- See `lt_mul_inv_iff₀` for a version with multiplication on the other side. -/ +lemma lt_mul_inv_iff₀' (hc : 0 < c) : a < b * c⁻¹ ↔ c * a < b := by + have := posMulStrictMono_iff_mulPosStrictMono.1 ‹_› + rw [lt_mul_inv_iff₀ hc, mul_comm] + +/-- See `mul_inv_lt_iff₀` for a version with multiplication on the other side. -/ +lemma mul_inv_lt_iff₀' (hc : 0 < c) : b * c⁻¹ < a ↔ b < c * a := by + have := posMulStrictMono_iff_mulPosStrictMono.1 ‹_› + rw [mul_inv_lt_iff₀ hc, mul_comm] + +/-- See `lt_div_iff₀` for a version with multiplication on the other side. -/ +lemma lt_div_iff₀' (hc : 0 < c) : a < b / c ↔ c * a < b := by + have := posMulStrictMono_iff_mulPosStrictMono.1 ‹_› + rw [lt_div_iff₀ hc, mul_comm] + +/-- See `div_lt_iff₀` for a version with multiplication on the other side. -/ +lemma div_lt_iff₀' (hc : 0 < c) : b / c < a ↔ b < c * a := by + have := posMulStrictMono_iff_mulPosStrictMono.1 ‹_› + rw [div_lt_iff₀ hc, mul_comm] + +lemma lt_div_comm₀ (ha : 0 < a) (hc : 0 < c) : a < b / c ↔ c < b / a := by + have := posMulStrictMono_iff_mulPosStrictMono.1 ‹_› + rw [lt_div_iff₀ ha, lt_div_iff₀' hc] + +lemma div_lt_comm₀ (hb : 0 < b) (hc : 0 < c) : a / b < c ↔ a / c < b := by + have := posMulStrictMono_iff_mulPosStrictMono.1 ‹_› + rw [div_lt_iff₀ hb, div_lt_iff₀' hc] + +end PosMulStrictMono end CommGroupWithZero diff --git a/Mathlib/Algebra/Order/GroupWithZero/Unbundled/Lemmas.lean b/Mathlib/Algebra/Order/GroupWithZero/Unbundled/Lemmas.lean new file mode 100644 index 00000000000000..edc0cb47b953dc --- /dev/null +++ b/Mathlib/Algebra/Order/GroupWithZero/Unbundled/Lemmas.lean @@ -0,0 +1,27 @@ +/- +Copyright (c) 2021 Eric Wieser. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Eric Wieser +-/ +import Mathlib.Algebra.Group.Pi.Basic +import Mathlib.Algebra.Order.GroupWithZero.Unbundled +import Mathlib.Algebra.GroupWithZero.Units.Equiv +import Mathlib.Order.Hom.Basic + +/-! +# Multiplication by a positive element as an order isomorphism +-/ + +variable {G₀} [GroupWithZero G₀] [Preorder G₀] [ZeroLEOneClass G₀] {a b c d : G₀} + +/-- `Equiv.mulLeft₀` as an order isomorphism. -/ +@[simps! (config := { simpRhs := true })] +def OrderIso.mulLeft₀ [PosMulMono G₀] [PosMulReflectLE G₀] (a : G₀) (ha : 0 < a) : G₀ ≃o G₀ where + toEquiv := .mulLeft₀ a ha.ne' + map_rel_iff' := mul_le_mul_left ha + +/-- `Equiv.mulRight₀` as an order isomorphism. -/ +@[simps! (config := { simpRhs := true })] +def OrderIso.mulRight₀ [MulPosMono G₀] [MulPosReflectLE G₀] (a : G₀) (ha : 0 < a) : G₀ ≃o G₀ where + toEquiv := .mulRight₀ a ha.ne' + map_rel_iff' := mul_le_mul_right ha diff --git a/Mathlib/Analysis/Asymptotics/Asymptotics.lean b/Mathlib/Analysis/Asymptotics/Asymptotics.lean index fda3788c247e8b..9017527a7eefa1 100644 --- a/Mathlib/Analysis/Asymptotics/Asymptotics.lean +++ b/Mathlib/Analysis/Asymptotics/Asymptotics.lean @@ -128,13 +128,13 @@ theorem isBigO_iff'' {g : α → E'''} : obtain ⟨c, ⟨hc_pos, hc⟩⟩ := h refine ⟨c⁻¹, ⟨by positivity, ?_⟩⟩ filter_upwards [hc] with x hx - rwa [inv_mul_le_iff (by positivity)] + rwa [inv_mul_le_iff₀ (by positivity)] case mpr => rw [isBigO_iff'] obtain ⟨c, ⟨hc_pos, hc⟩⟩ := h refine ⟨c⁻¹, ⟨by positivity, ?_⟩⟩ filter_upwards [hc] with x hx - rwa [← inv_inv c, inv_mul_le_iff (by positivity)] at hx + rwa [← inv_inv c, inv_mul_le_iff₀ (by positivity)] at hx theorem IsBigO.of_bound (c : ℝ) (h : ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖) : f =O[l] g := isBigO_iff.2 ⟨c, h⟩ diff --git a/Mathlib/Analysis/CStarAlgebra/Unitization.lean b/Mathlib/Analysis/CStarAlgebra/Unitization.lean index d664e50c7c2195..7a5bdee2eef6e3 100644 --- a/Mathlib/Analysis/CStarAlgebra/Unitization.lean +++ b/Mathlib/Analysis/CStarAlgebra/Unitization.lean @@ -72,7 +72,7 @@ instance CStarRing.instRegularNormedAlgebra : RegularNormedAlgebra 𝕜 E where · simpa only [mem_closedBall_zero_iff, norm_smul, one_mul, norm_star] using (NNReal.le_inv_iff_mul_le ha.ne').1 (one_mul ‖a‖₊⁻¹ ▸ hk₂.le : ‖k‖₊ ≤ ‖a‖₊⁻¹) · simp only [map_smul, nnnorm_smul, mul_apply', mul_smul_comm, CStarRing.nnnorm_self_mul_star] - rwa [← NNReal.div_lt_iff (mul_pos ha ha).ne', div_eq_mul_inv, mul_inv, ← mul_assoc] + rwa [← div_lt_iff₀ (mul_pos ha ha), div_eq_mul_inv, mul_inv, ← mul_assoc] section CStarProperty diff --git a/Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean b/Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean index ea6f8405c48bf3..67b3db1e4cd80a 100644 --- a/Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean +++ b/Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean @@ -144,7 +144,7 @@ theorem surjOn_closedBall_of_nonlinearRightInverse simp only [dist_le_zero] at this rw [this] have If' : (0 : ℝ) < f'symm.nnnorm := by rw [← inv_pos]; exact (NNReal.coe_nonneg _).trans_lt hc - have Icf' : (c : ℝ) * f'symm.nnnorm < 1 := by rwa [inv_eq_one_div, lt_div_iff If'] at hc + have Icf' : (c : ℝ) * f'symm.nnnorm < 1 := by rwa [inv_eq_one_div, lt_div_iff₀ If'] at hc have Jf' : (f'symm.nnnorm : ℝ) ≠ 0 := ne_of_gt If' have Jcf' : (1 : ℝ) - c * f'symm.nnnorm ≠ 0 := by apply ne_of_gt; linarith /- We have to show that `y` can be written as `f x` for some `x ∈ closedBall b ε`. diff --git a/Mathlib/Analysis/Calculus/MeanValue.lean b/Mathlib/Analysis/Calculus/MeanValue.lean index 7459bc396a5f2e..703da3c9d5c78d 100644 --- a/Mathlib/Analysis/Calculus/MeanValue.lean +++ b/Mathlib/Analysis/Calculus/MeanValue.lean @@ -901,7 +901,7 @@ theorem Convex.mul_sub_lt_image_sub_of_lt_deriv {D : Set ℝ} (hD : Convex ℝ D obtain ⟨a, a_mem, ha⟩ : ∃ a ∈ Ioo x y, deriv f a = (f y - f x) / (y - x) := exists_deriv_eq_slope f hxy (hf.mono hxyD) (hf'.mono hxyD') have : C < (f y - f x) / (y - x) := ha ▸ hf'_gt _ (hxyD' a_mem) - exact (lt_div_iff (sub_pos.2 hxy)).1 this + exact (lt_div_iff₀ (sub_pos.2 hxy)).1 this /-- Let `f : ℝ → ℝ` be a differentiable function. If `C < f'`, then `f` grows faster than `C * x`, i.e., `C * (y - x) < f y - f x` whenever `x < y`. -/ diff --git a/Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean b/Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean index da30835b1f395e..df41e2606b7e8c 100644 --- a/Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean +++ b/Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean @@ -286,7 +286,7 @@ theorem difference_quotients_converge_uniformly refine lt_of_le_of_lt ?_ hqε by_cases hyz' : x = y; · simp [hyz', hqpos.le] have hyz : 0 < ‖y - x‖ := by rw [norm_pos_iff]; intro hy'; exact hyz' (eq_of_sub_eq_zero hy').symm - rw [inv_mul_le_iff hyz, mul_comm, sub_sub_sub_comm] + rw [inv_mul_le_iff₀ hyz, mul_comm, sub_sub_sub_comm] simp only [Pi.zero_apply, dist_zero_left] at e refine Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le @@ -385,7 +385,7 @@ theorem hasFDerivAt_of_tendstoUniformlyOnFilter [NeBot l] by_cases hx : x = n.2; · simp [hx] have hnx : 0 < ‖n.2 - x‖ := by rw [norm_pos_iff]; intro hx'; exact hx (eq_of_sub_eq_zero hx').symm - rw [inv_mul_le_iff hnx, mul_comm] + rw [inv_mul_le_iff₀ hnx, mul_comm] simp only [Function.comp_apply, Prod.map_apply'] rw [norm_sub_rev] exact (f' n.1 x - g' x).le_opNorm (n.2 - x) diff --git a/Mathlib/Analysis/Complex/AbelLimit.lean b/Mathlib/Analysis/Complex/AbelLimit.lean index 84347303b29c2d..167aa0434d8061 100644 --- a/Mathlib/Analysis/Complex/AbelLimit.lean +++ b/Mathlib/Analysis/Complex/AbelLimit.lean @@ -208,7 +208,7 @@ theorem tendsto_tsum_powerSeries_nhdsWithin_stolzSet gcongr; nth_rw 3 [← mul_one ‖_‖] gcongr; exact pow_le_one₀ (norm_nonneg _) zn.le _ ≤ ‖1 - z‖ * (F + 1) := by gcongr; linarith only - _ < _ := by rwa [norm_sub_rev, lt_div_iff (by positivity)] at zd + _ < _ := by rwa [norm_sub_rev, lt_div_iff₀ (by positivity)] at zd have S₂ : ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4 := calc _ ≤ ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ε / 4 / M * ‖z‖ ^ i := by diff --git a/Mathlib/Analysis/Complex/Hadamard.lean b/Mathlib/Analysis/Complex/Hadamard.lean index 88d6c801d518c9..37d20a8d075404 100644 --- a/Mathlib/Analysis/Complex/Hadamard.lean +++ b/Mathlib/Analysis/Complex/Hadamard.lean @@ -189,14 +189,14 @@ lemma F_edge_le_one (f : ℂ → E) (ε : ℝ) (hε : ε > 0) (z : ℂ) rcases hz with hz0 | hz1 -- `z.re = 0` · simp only [hz0, zero_sub, Real.rpow_neg_one, neg_zero, Real.rpow_zero, mul_one, - inv_mul_le_iff (sSupNormIm_eps_pos f hε 0)] + inv_mul_le_iff₀ (sSupNormIm_eps_pos f hε 0)] rw [← hz0] apply le_of_lt (norm_lt_sSupNormIm_eps f ε hε _ _ hB) simp only [verticalClosedStrip, mem_preimage, zero_le_one, left_mem_Icc, hz0] -- `z.re = 1` · rw [mem_singleton_iff] at hz1 simp only [hz1, one_mul, Real.rpow_zero, sub_self, Real.rpow_neg_one, - inv_mul_le_iff (sSupNormIm_eps_pos f hε 1), mul_one] + inv_mul_le_iff₀ (sSupNormIm_eps_pos f hε 1), mul_one] rw [← hz1] apply le_of_lt (norm_lt_sSupNormIm_eps f ε hε _ _ hB) simp only [verticalClosedStrip, mem_preimage, zero_le_one, hz1, right_mem_Icc] @@ -304,7 +304,7 @@ lemma norm_le_interpStrip_of_mem_verticalClosedStrip_eps (ε : ℝ) (hε : ε > ‖f z‖ ≤ ‖((ε + sSupNormIm f 0) ^ (1-z) * (ε + sSupNormIm f 1) ^ z : ℂ)‖ := by simp only [F, abs_invInterpStrip _ _ hε, norm_smul, norm_mul, norm_eq_abs, ← ofReal_add, abs_cpow_eq_rpow_re_of_pos (sSupNormIm_eps_pos f hε _) _, sub_re, one_re] - rw [← mul_inv_le_iff, ← one_mul (((ε + sSupNormIm f 1) ^ z.re)), ← mul_inv_le_iff', + rw [← mul_inv_le_iff₀', ← one_mul (((ε + sSupNormIm f 1) ^ z.re)), ← mul_inv_le_iff₀, ← Real.rpow_neg_one, ← Real.rpow_neg_one] · simp only [← Real.rpow_mul (le_of_lt (sSupNormIm_eps_pos f hε _)), mul_neg, mul_one, neg_sub, mul_assoc] diff --git a/Mathlib/Analysis/Complex/PhragmenLindelof.lean b/Mathlib/Analysis/Complex/PhragmenLindelof.lean index e172dd9cfe0311..a457d182cf8425 100644 --- a/Mathlib/Analysis/Complex/PhragmenLindelof.lean +++ b/Mathlib/Analysis/Complex/PhragmenLindelof.lean @@ -133,7 +133,7 @@ theorem horizontal_strip (hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)) rcases hB with ⟨c, hc, B, hO⟩ obtain ⟨d, ⟨hcd, hd₀⟩, hd⟩ : ∃ d, (c < d ∧ 0 < d) ∧ d < π / 2 / b := by simpa only [max_lt_iff] using exists_between (max_lt hc hπb) - have hb' : d * b < π / 2 := (lt_div_iff hb).1 hd + have hb' : d * b < π / 2 := (lt_div_iff₀ hb).1 hd set aff := (fun w => d * (w - a * I) : ℂ → ℂ) set g := fun (ε : ℝ) (w : ℂ) => exp (ε * (exp (aff w) + exp (-aff w))) /- Since `g ε z → 1` as `ε → 0⁻`, it suffices to prove that `‖g ε z • f z‖ ≤ C` diff --git a/Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean b/Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean index f4c7f5c6d05f35..256120e3063494 100644 --- a/Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean +++ b/Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean @@ -261,7 +261,7 @@ instance : MetricSpace ℍ := have h₀ : 0 < R / im z + 1 := one_pos.trans h₁ refine ⟨log (R / im z + 1), Real.log_pos h₁, ?_⟩ refine fun w hw => (dist_coe_le w z).trans_lt ?_ - rwa [← lt_div_iff' z.im_pos, sub_lt_iff_lt_add, ← Real.lt_log_iff_exp_lt h₀] + rwa [← lt_div_iff₀' z.im_pos, sub_lt_iff_lt_add, ← Real.lt_log_iff_exp_lt h₀] theorem im_pos_of_dist_center_le {z : ℍ} {r : ℝ} {w : ℂ} (h : dist w (center z r) ≤ z.im * Real.sinh r) : 0 < w.im := diff --git a/Mathlib/Analysis/Convex/Body.lean b/Mathlib/Analysis/Convex/Body.lean index ab8c493ff10c34..219c7807cb05dc 100644 --- a/Mathlib/Analysis/Convex/Body.lean +++ b/Mathlib/Analysis/Convex/Body.lean @@ -212,7 +212,7 @@ theorem iInter_smul_eq_self [T2Space V] {u : ℕ → ℝ≥0} (K : ConvexBody V) rw [show (1 + u n : ℝ) • y - y = (u n : ℝ) • y by rw [add_smul, one_smul, add_sub_cancel_left], norm_smul, Real.norm_eq_abs] specialize hn n le_rfl - rw [_root_.lt_div_iff' hC_pos, mul_comm, NNReal.coe_zero, sub_zero, Real.norm_eq_abs] at hn + rw [lt_div_iff₀' hC_pos, mul_comm, NNReal.coe_zero, sub_zero, Real.norm_eq_abs] at hn refine lt_of_le_of_lt ?_ hn exact mul_le_mul_of_nonneg_left (hC_bdd _ hyK) (abs_nonneg _) · refine Set.mem_iInter.mpr (fun n => Convex.mem_smul_of_zero_mem K.convex h_zero h ?_) diff --git a/Mathlib/Analysis/Convex/Continuous.lean b/Mathlib/Analysis/Convex/Continuous.lean index 746b4cf9313a68..4b2ebd632b395d 100644 --- a/Mathlib/Analysis/Convex/Continuous.lean +++ b/Mathlib/Analysis/Convex/Continuous.lean @@ -139,7 +139,7 @@ lemma ConvexOn.continuousOn_tfae (hC : IsOpen C) (hC' : C.Nonempty) (hf : Convex let w := δ⁻¹ • (z - y) + y have hwyz : δ • w + (1 - δ) • y = z := by simp [w, hδ₀.ne', sub_smul] have hw : dist w x₀ < ε := by - simpa [w, ← hx₀', dist_smul₀, abs_of_nonneg, hδ₀.le, inv_mul_lt_iff', hδ₀] + simpa [w, ← hx₀', dist_smul₀, abs_of_nonneg, hδ₀.le, inv_mul_lt_iff₀', hδ₀] calc f z ≤ max (f w) (f y) := hf.le_max_of_mem_segment (hr hw).2 hy ⟨_, _, hδ₀.le, sub_nonneg.2 hδ₁.le, by simp, hwyz⟩ diff --git a/Mathlib/Analysis/Convex/Deriv.lean b/Mathlib/Analysis/Convex/Deriv.lean index 6954ba6c48f2bd..4d71b529373a4f 100644 --- a/Mathlib/Analysis/Convex/Deriv.lean +++ b/Mathlib/Analysis/Convex/Deriv.lean @@ -95,7 +95,7 @@ theorem StrictMonoOn.exists_slope_lt_deriv {x y : ℝ} {f : ℝ → ℝ} (hf : C apply ne_of_gt exact hf'_mono ⟨hxw, hwy⟩ ⟨hxw.trans hz.1, hz.2⟩ hz.1 refine ⟨b, ⟨hxw.trans hwb, hby⟩, ?_⟩ - simp only [div_lt_iff, hxy, hxw, hwy, sub_pos] at ha hb ⊢ + simp only [div_lt_iff₀, hxy, hxw, hwy, sub_pos] at ha hb ⊢ have : deriv f a * (w - x) < deriv f b * (w - x) := by apply mul_lt_mul _ le_rfl (sub_pos.2 hxw) _ · exact hf'_mono ⟨hxa, haw.trans hwy⟩ ⟨hxw.trans hwb, hby⟩ (haw.trans hwb) @@ -139,7 +139,7 @@ theorem StrictMonoOn.exists_deriv_lt_slope {x y : ℝ} {f : ℝ → ℝ} (hf : C apply ne_of_gt exact hf'_mono ⟨hxw, hwy⟩ ⟨hxw.trans hz.1, hz.2⟩ hz.1 refine ⟨a, ⟨hxa, haw.trans hwy⟩, ?_⟩ - simp only [lt_div_iff, hxy, hxw, hwy, sub_pos] at ha hb ⊢ + simp only [lt_div_iff₀, hxy, hxw, hwy, sub_pos] at ha hb ⊢ have : deriv f a * (y - w) < deriv f b * (y - w) := by apply mul_lt_mul _ le_rfl (sub_pos.2 hwy) _ · exact hf'_mono ⟨hxa, haw.trans hwy⟩ ⟨hxw.trans hwb, hby⟩ (haw.trans hwb) diff --git a/Mathlib/Analysis/Convex/Gauge.lean b/Mathlib/Analysis/Convex/Gauge.lean index e68cb3085d3d7f..b04bce7ae39f28 100644 --- a/Mathlib/Analysis/Convex/Gauge.lean +++ b/Mathlib/Analysis/Convex/Gauge.lean @@ -139,7 +139,7 @@ theorem gauge_le_eq (hs₁ : Convex ℝ s) (hs₀ : (0 : E) ∈ s) (hs₂ : Abso suffices (r⁻¹ * δ) • δ⁻¹ • x ∈ s by rwa [smul_smul, mul_inv_cancel_right₀ δ_pos.ne'] at this rw [mem_smul_set_iff_inv_smul_mem₀ δ_pos.ne'] at hδ refine hs₁.smul_mem_of_zero_mem hs₀ hδ ⟨by positivity, ?_⟩ - rw [inv_mul_le_iff hr', mul_one] + rw [inv_mul_le_iff₀ hr', mul_one] exact hδr.le · have hε' := (lt_add_iff_pos_right a).2 (half_pos hε) exact @@ -369,7 +369,7 @@ theorem gauge_lt_of_mem_smul (x : E) (ε : ℝ) (hε : 0 < ε) (hs₂ : IsOpen s gauge s x < ε := by have : ε⁻¹ • x ∈ s := by rwa [← mem_smul_set_iff_inv_smul_mem₀ hε.ne'] have h_gauge_lt := gauge_lt_one_of_mem_of_isOpen hs₂ this - rwa [gauge_smul_of_nonneg (inv_nonneg.2 hε.le), smul_eq_mul, inv_mul_lt_iff hε, mul_one] + rwa [gauge_smul_of_nonneg (inv_nonneg.2 hε.le), smul_eq_mul, inv_mul_lt_iff₀ hε, mul_one] at h_gauge_lt theorem mem_closure_of_gauge_le_one (hc : Convex ℝ s) (hs₀ : 0 ∈ s) (ha : Absorbent ℝ s) @@ -500,7 +500,7 @@ protected theorem Seminorm.gauge_ball (p : Seminorm ℝ E) : gauge (p.ball 0 1) have hpx₂ : 0 < 2 * p x := mul_pos zero_lt_two hpx refine hp.subset ⟨hpx₂, (2 * p x)⁻¹ • x, ?_, smul_inv_smul₀ hpx₂.ne' _⟩ rw [p.mem_ball_zero, map_smul_eq_mul, Real.norm_eq_abs, abs_of_pos (inv_pos.2 hpx₂), - inv_mul_lt_iff hpx₂, mul_one] + inv_mul_lt_iff₀ hpx₂, mul_one] exact lt_mul_of_one_lt_left hpx one_lt_two refine IsGLB.csInf_eq ⟨fun r => ?_, fun r hr => le_of_forall_pos_le_add fun ε hε => ?_⟩ hp · rintro ⟨hr, y, hy, rfl⟩ @@ -512,7 +512,7 @@ protected theorem Seminorm.gauge_ball (p : Seminorm ℝ E) : gauge (p.ball 0 1) add_pos_of_nonneg_of_pos (apply_nonneg _ _) hε refine hr ⟨hpε, (p x + ε)⁻¹ • x, ?_, smul_inv_smul₀ hpε.ne' _⟩ rw [p.mem_ball_zero, map_smul_eq_mul, Real.norm_eq_abs, abs_of_pos (inv_pos.2 hpε), - inv_mul_lt_iff hpε, mul_one] + inv_mul_lt_iff₀ hpε, mul_one] exact lt_add_of_pos_right _ hε theorem Seminorm.gaugeSeminorm_ball (p : Seminorm ℝ E) : diff --git a/Mathlib/Analysis/Convex/Integral.lean b/Mathlib/Analysis/Convex/Integral.lean index 12b11b68057db2..dd75c412a4ffc2 100644 --- a/Mathlib/Analysis/Convex/Integral.lean +++ b/Mathlib/Analysis/Convex/Integral.lean @@ -328,7 +328,7 @@ theorem ae_eq_const_or_norm_integral_lt_of_norm_le_const [StrictConvexSpace ℝ simp [ENNReal.toReal_pos_iff, pos_iff_ne_zero, h₀, measure_lt_top] refine (ae_eq_const_or_norm_average_lt_of_norm_le_const h_le).imp_right fun H => ?_ rwa [average_eq, norm_smul, norm_inv, Real.norm_eq_abs, abs_of_pos hμ, ← div_eq_inv_mul, - div_lt_iff' hμ] at H + div_lt_iff₀' hμ] at H /-- If `E` is a strictly convex normed space and `f : α → E` is a function such that `‖f x‖ ≤ C` a.e. on a set `t` of finite measure, then either this function is a.e. equal to its average value on diff --git a/Mathlib/Analysis/Convex/Slope.lean b/Mathlib/Analysis/Convex/Slope.lean index ea7ca88a2e8532..38072902d3e919 100644 --- a/Mathlib/Analysis/Convex/Slope.lean +++ b/Mathlib/Analysis/Convex/Slope.lean @@ -158,7 +158,7 @@ theorem strictConvexOn_of_slope_strict_mono_adjacent (hs : Convex 𝕜 s) simp_rw [div_eq_iff hxz.ne', ← hab] ring rwa [sub_mul, sub_mul, sub_lt_iff_lt_add', ← add_sub_assoc, lt_sub_iff_add_lt, ← mul_add, - sub_add_sub_cancel, ← lt_div_iff hxz, add_div, mul_div_assoc, mul_div_assoc, mul_comm (f x), + sub_add_sub_cancel, ← lt_div_iff₀ hxz, add_div, mul_div_assoc, mul_div_assoc, mul_comm (f x), mul_comm (f z), ha, hb] at this /-- If for any three points `x < y < z`, the slope of the secant line of `f : 𝕜 → 𝕜` on `[x, y]` is @@ -267,7 +267,7 @@ theorem StrictConvexOn.secant_strict_mono_aux1 (hf : StrictConvexOn 𝕜 s f) {x have hxy' : 0 < y - x := by linarith have hyz' : 0 < z - y := by linarith have hxz' : 0 < z - x := by linarith - rw [← lt_div_iff' hxz'] + rw [← lt_div_iff₀' hxz'] have ha : 0 < (z - y) / (z - x) := by positivity have hb : 0 < (y - x) / (z - x) := by positivity calc diff --git a/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean b/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean index 922b18543ffe03..b293f4c6a7eb3e 100644 --- a/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean +++ b/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean @@ -40,14 +40,14 @@ theorem strictConvexOn_exp : StrictConvexOn ℝ univ exp := by trans exp y · have h1 : 0 < y - x := by linarith have h2 : x - y < 0 := by linarith - rw [div_lt_iff h1] + rw [div_lt_iff₀ h1] calc exp y - exp x = exp y - exp y * exp (x - y) := by rw [← exp_add]; ring_nf _ = exp y * (1 - exp (x - y)) := by ring _ < exp y * -(x - y) := by gcongr; linarith [add_one_lt_exp h2.ne] _ = exp y * (y - x) := by ring · have h1 : 0 < z - y := by linarith - rw [lt_div_iff h1] + rw [lt_div_iff₀ h1] calc exp y * (z - y) < exp y * (exp (z - y) - 1) := by gcongr _ * ?_ @@ -66,7 +66,7 @@ theorem strictConcaveOn_log_Ioi : StrictConcaveOn ℝ (Ioi 0) log := by have hy : 0 < y := hx.trans hxy trans y⁻¹ · have h : 0 < z - y := by linarith - rw [div_lt_iff h] + rw [div_lt_iff₀ h] have hyz' : 0 < z / y := by positivity have hyz'' : z / y ≠ 1 := by contrapose! h @@ -77,7 +77,7 @@ theorem strictConcaveOn_log_Ioi : StrictConcaveOn ℝ (Ioi 0) log := by _ < z / y - 1 := log_lt_sub_one_of_pos hyz' hyz'' _ = y⁻¹ * (z - y) := by field_simp · have h : 0 < y - x := by linarith - rw [lt_div_iff h] + rw [lt_div_iff₀ h] have hxy' : 0 < x / y := by positivity have hxy'' : x / y ≠ 1 := by contrapose! h @@ -105,12 +105,12 @@ theorem one_add_mul_self_lt_rpow_one_add {s : ℝ} (hs : -1 ≤ s) (hs' : s ≠ rw [rpow_def_of_pos hs1, ← exp_log hs2] apply exp_strictMono cases' lt_or_gt_of_ne hs' with hs' hs' - · rw [← div_lt_iff hp', ← div_lt_div_right_of_neg hs'] + · rw [← div_lt_iff₀ hp', ← div_lt_div_right_of_neg hs'] convert strictConcaveOn_log_Ioi.secant_strict_mono (zero_lt_one' ℝ) hs2 hs1 hs4 hs3 _ using 1 · rw [add_sub_cancel_left, log_one, sub_zero] · rw [add_sub_cancel_left, div_div, log_one, sub_zero] · apply add_lt_add_left (mul_lt_of_one_lt_left hs' hp) - · rw [← div_lt_iff hp', ← div_lt_div_right hs'] + · rw [← div_lt_iff₀ hp', ← div_lt_div_right hs'] convert strictConcaveOn_log_Ioi.secant_strict_mono (zero_lt_one' ℝ) hs1 hs2 hs3 hs4 _ using 1 · rw [add_sub_cancel_left, div_div, log_one, sub_zero] · rw [add_sub_cancel_left, log_one, sub_zero] @@ -144,12 +144,12 @@ theorem rpow_one_add_lt_one_add_mul_self {s : ℝ} (hs : -1 ≤ s) (hs' : s ≠ rw [rpow_def_of_pos hs1, ← exp_log hs2] apply exp_strictMono cases' lt_or_gt_of_ne hs' with hs' hs' - · rw [← lt_div_iff hp1, ← div_lt_div_right_of_neg hs'] + · rw [← lt_div_iff₀ hp1, ← div_lt_div_right_of_neg hs'] convert strictConcaveOn_log_Ioi.secant_strict_mono (zero_lt_one' ℝ) hs1 hs2 hs3 hs4 _ using 1 · rw [add_sub_cancel_left, div_div, log_one, sub_zero] · rw [add_sub_cancel_left, log_one, sub_zero] · apply add_lt_add_left (lt_mul_of_lt_one_left hs' hp2) - · rw [← lt_div_iff hp1, ← div_lt_div_right hs'] + · rw [← lt_div_iff₀ hp1, ← div_lt_div_right hs'] convert strictConcaveOn_log_Ioi.secant_strict_mono (zero_lt_one' ℝ) hs2 hs1 hs4 hs3 _ using 1 · rw [add_sub_cancel_left, log_one, sub_zero] · rw [add_sub_cancel_left, div_div, log_one, sub_zero] @@ -175,20 +175,21 @@ theorem strictConvexOn_rpow {p : ℝ} (hp : 1 < p) : StrictConvexOn ℝ (Ici 0) have hy' : 0 < y ^ p := rpow_pos_of_pos hy _ trans p * y ^ (p - 1) · have q : 0 < y - x := by rwa [sub_pos] - rw [div_lt_iff q, ← div_lt_div_right hy', _root_.sub_div, div_self hy'.ne', ← div_rpow hx hy.le, - sub_lt_comm, ← add_sub_cancel_right (x / y) 1, add_comm, add_sub_assoc, ← div_mul_eq_mul_div, - mul_div_assoc, ← rpow_sub hy, sub_sub_cancel_left, rpow_neg_one, mul_assoc, ← div_eq_inv_mul, - sub_eq_add_neg, ← mul_neg, ← neg_div, neg_sub, _root_.sub_div, div_self hy.ne'] + rw [div_lt_iff₀ q, ← div_lt_div_right hy', _root_.sub_div, div_self hy'.ne', + ← div_rpow hx hy.le, sub_lt_comm, ← add_sub_cancel_right (x / y) 1, add_comm, add_sub_assoc, + ← div_mul_eq_mul_div, mul_div_assoc, ← rpow_sub hy, sub_sub_cancel_left, rpow_neg_one, + mul_assoc, ← div_eq_inv_mul, sub_eq_add_neg, ← mul_neg, ← neg_div, neg_sub, _root_.sub_div, + div_self hy.ne'] apply one_add_mul_self_lt_rpow_one_add _ _ hp · rw [le_sub_iff_add_le, neg_add_cancel, div_nonneg_iff] exact Or.inl ⟨hx, hy.le⟩ · rw [sub_ne_zero] exact ((div_lt_one hy).mpr hxy).ne · have q : 0 < z - y := by rwa [sub_pos] - rw [lt_div_iff q, ← div_lt_div_right hy', _root_.sub_div, div_self hy'.ne', ← div_rpow hz hy.le, - lt_sub_iff_add_lt', ← add_sub_cancel_right (z / y) 1, add_comm _ 1, add_sub_assoc, - ← div_mul_eq_mul_div, mul_div_assoc, ← rpow_sub hy, sub_sub_cancel_left, rpow_neg_one, - mul_assoc, ← div_eq_inv_mul, _root_.sub_div, div_self hy.ne'] + rw [lt_div_iff₀ q, ← div_lt_div_right hy', _root_.sub_div, div_self hy'.ne', + ← div_rpow hz hy.le, lt_sub_iff_add_lt', ← add_sub_cancel_right (z / y) 1, add_comm _ 1, + add_sub_assoc, ← div_mul_eq_mul_div, mul_div_assoc, ← rpow_sub hy, sub_sub_cancel_left, + rpow_neg_one, mul_assoc, ← div_eq_inv_mul, _root_.sub_div, div_self hy.ne'] apply one_add_mul_self_lt_rpow_one_add _ _ hp · rw [le_sub_iff_add_le, neg_add_cancel, div_nonneg_iff] exact Or.inl ⟨hz, hy.le⟩ diff --git a/Mathlib/Analysis/Convex/StrictConvexSpace.lean b/Mathlib/Analysis/Convex/StrictConvexSpace.lean index 29a52bd553f835..32a1cef9cd3a92 100644 --- a/Mathlib/Analysis/Convex/StrictConvexSpace.lean +++ b/Mathlib/Analysis/Convex/StrictConvexSpace.lean @@ -204,5 +204,5 @@ theorem not_sameRay_iff_abs_lt_norm_sub : ¬SameRay ℝ x y ↔ |‖x‖ - ‖y theorem norm_midpoint_lt_iff (h : ‖x‖ = ‖y‖) : ‖(1 / 2 : ℝ) • (x + y)‖ < ‖x‖ ↔ x ≠ y := by rw [norm_smul, Real.norm_of_nonneg (one_div_nonneg.2 zero_le_two), ← inv_eq_one_div, ← - div_eq_inv_mul, div_lt_iff (zero_lt_two' ℝ), mul_two, ← not_sameRay_iff_of_norm_eq h, + div_eq_inv_mul, div_lt_iff₀ (zero_lt_two' ℝ), mul_two, ← not_sameRay_iff_of_norm_eq h, not_sameRay_iff_norm_add_lt, h] diff --git a/Mathlib/Analysis/Distribution/SchwartzSpace.lean b/Mathlib/Analysis/Distribution/SchwartzSpace.lean index 43f9326f818a88..17917e748b4da3 100644 --- a/Mathlib/Analysis/Distribution/SchwartzSpace.lean +++ b/Mathlib/Analysis/Distribution/SchwartzSpace.lean @@ -1182,7 +1182,7 @@ instance instZeroAtInftyContinuousMapClass : ZeroAtInftyContinuousMapClass 𝓢( intro ε hε use (SchwartzMap.seminorm ℝ 1 0) f / ε intro x hx - rw [div_lt_iff hε] at hx + rw [div_lt_iff₀ hε] at hx have hxpos : 0 < ‖x‖ := by rw [norm_pos_iff'] intro hxzero @@ -1191,7 +1191,7 @@ instance instZeroAtInftyContinuousMapClass : ZeroAtInftyContinuousMapClass 𝓢( have := norm_pow_mul_le_seminorm ℝ f 1 x rw [pow_one, ← le_div_iff₀' hxpos] at this apply lt_of_le_of_lt this - rwa [div_lt_iff' hxpos] + rwa [div_lt_iff₀' hxpos] /-- Schwartz functions as continuous functions vanishing at infinity. -/ def toZeroAtInfty (f : 𝓢(E, F)) : C₀(E, F) where diff --git a/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean b/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean index 024a1e6a9ca37e..5b128034dec9b3 100644 --- a/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean +++ b/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean @@ -140,7 +140,7 @@ theorem tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support have : ‖(1 / 2 : ℂ)‖ = 2⁻¹ := by norm_num rw [fourierIntegral_eq_half_sub_half_period_translate hw_ne (hf1.integrable_of_hasCompactSupport hf2), - norm_smul, this, inv_mul_eq_div, div_lt_iff' two_pos] + norm_smul, this, inv_mul_eq_div, div_lt_iff₀' two_pos] refine lt_of_le_of_lt (norm_integral_le_integral_norm _) ?_ simp_rw [Circle.norm_smul] --* Show integral can be taken over A only. @@ -164,8 +164,8 @@ theorem tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support simp_rw [norm_norm] simp_rw [dist_eq_norm] at hδ2 refine fun x _ => (hδ2 ?_).le - rw [sub_add_cancel_left, norm_neg, hw'_nm, ← div_div, div_lt_iff (norm_pos_iff.mpr hw_ne), ← - div_lt_iff' hδ1, div_div] + rw [sub_add_cancel_left, norm_neg, hw'_nm, ← div_div, div_lt_iff₀ (norm_pos_iff.mpr hw_ne), ← + div_lt_iff₀' hδ1, div_div] exact (lt_add_of_pos_left _ one_half_pos).trans_le hw_bd have bdA2 := norm_setIntegral_le_of_norm_le_const (hB_vol.trans_lt ENNReal.coe_lt_top) bdA ?_ swap @@ -177,7 +177,7 @@ theorem tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support Real.norm_of_nonneg (setIntegral_nonneg mA fun x _ => norm_nonneg _) rw [this] at bdA2 refine bdA2.trans_lt ?_ - rw [div_mul_eq_mul_div, div_lt_iff (NNReal.coe_pos.mpr hB_pos), mul_comm (2 : ℝ), mul_assoc, + rw [div_mul_eq_mul_div, div_lt_iff₀ (NNReal.coe_pos.mpr hB_pos), mul_comm (2 : ℝ), mul_assoc, mul_lt_mul_left hε] rw [← ENNReal.toReal_le_toReal] at hB_vol · refine hB_vol.trans_lt ?_ diff --git a/Mathlib/Analysis/InnerProductSpace/LaxMilgram.lean b/Mathlib/Analysis/InnerProductSpace/LaxMilgram.lean index 7ac440395d2e81..9aa623e738fae3 100644 --- a/Mathlib/Analysis/InnerProductSpace/LaxMilgram.lean +++ b/Mathlib/Analysis/InnerProductSpace/LaxMilgram.lean @@ -64,7 +64,7 @@ theorem antilipschitz (coercive : IsCoercive B) : ∃ C : ℝ≥0, 0 < C ∧ Ant refine ⟨C⁻¹.toNNReal, Real.toNNReal_pos.mpr (inv_pos.mpr C_pos), ?_⟩ refine ContinuousLinearMap.antilipschitz_of_bound B♯ ?_ simp_rw [Real.coe_toNNReal', max_eq_left_of_lt (inv_pos.mpr C_pos), ← - inv_mul_le_iff (inv_pos.mpr C_pos)] + inv_mul_le_iff₀ (inv_pos.mpr C_pos)] simpa using below_bound theorem ker_eq_bot (coercive : IsCoercive B) : ker B♯ = ⊥ := by diff --git a/Mathlib/Analysis/LocallyConvex/WithSeminorms.lean b/Mathlib/Analysis/LocallyConvex/WithSeminorms.lean index ae6a4a37290bc3..b4165a1a770533 100644 --- a/Mathlib/Analysis/LocallyConvex/WithSeminorms.lean +++ b/Mathlib/Analysis/LocallyConvex/WithSeminorms.lean @@ -135,7 +135,7 @@ theorem basisSets_smul_right (v : E) (U : Set E) (hU : U ∈ p.basisSets) : rw [hU, Filter.eventually_iff] simp_rw [(s.sup p).mem_ball_zero, map_smul_eq_mul] by_cases h : 0 < (s.sup p) v - · simp_rw [(lt_div_iff h).symm] + · simp_rw [(lt_div_iff₀ h).symm] rw [← _root_.ball_zero_eq] exact Metric.ball_mem_nhds 0 (div_pos hr h) simp_rw [le_antisymm (not_lt.mp h) (apply_nonneg _ v), mul_zero, hr] diff --git a/Mathlib/Analysis/Normed/Affine/AddTorsor.lean b/Mathlib/Analysis/Normed/Affine/AddTorsor.lean index caa4e080fffdf9..2e2257c96f378e 100644 --- a/Mathlib/Analysis/Normed/Affine/AddTorsor.lean +++ b/Mathlib/Analysis/Normed/Affine/AddTorsor.lean @@ -220,7 +220,7 @@ theorem eventually_homothety_mem_of_mem_interior (x : Q) {s : Set Q} {y : Q} (hy obtain ⟨u, hu₁, hu₂, hu₃⟩ := mem_interior.mp hy obtain ⟨ε, hε, hyε⟩ := Metric.isOpen_iff.mp hu₂ y hu₃ refine ⟨ε / ‖y -ᵥ x‖, div_pos hε hxy, fun δ (hδ : ‖δ - 1‖ < ε / ‖y -ᵥ x‖) => hu₁ (hyε ?_)⟩ - rw [lt_div_iff hxy, ← norm_smul, sub_smul, one_smul] at hδ + rw [lt_div_iff₀ hxy, ← norm_smul, sub_smul, one_smul] at hδ rwa [homothety_apply, Metric.mem_ball, dist_eq_norm_vsub W, vadd_vsub_eq_sub_vsub] theorem eventually_homothety_image_subset_of_finite_subset_interior (x : Q) {s : Set Q} {t : Set Q} diff --git a/Mathlib/Analysis/Normed/Algebra/Spectrum.lean b/Mathlib/Analysis/Normed/Algebra/Spectrum.lean index 61bab9e550cc35..fa49b3701161ca 100644 --- a/Mathlib/Analysis/Normed/Algebra/Spectrum.lean +++ b/Mathlib/Analysis/Normed/Algebra/Spectrum.lean @@ -101,7 +101,7 @@ theorem mem_resolventSet_of_norm_lt_mul {a : A} {k : 𝕜} (h : ‖a‖ * ‖(1 ne_zero_of_norm_ne_zero ((mul_nonneg (norm_nonneg _) (norm_nonneg _)).trans_lt h).ne' letI ku := Units.map ↑ₐ.toMonoidHom (Units.mk0 k hk) rw [← inv_inv ‖(1 : A)‖, - mul_inv_lt_iff (inv_pos.2 <| norm_pos_iff.2 (one_ne_zero : (1 : A) ≠ 0))] at h + mul_inv_lt_iff₀' (inv_pos.2 <| norm_pos_iff.2 (one_ne_zero : (1 : A) ≠ 0))] at h have hku : ‖-a‖ < ‖(↑ku⁻¹ : A)‖⁻¹ := by simpa [ku, norm_algebraMap] using h simpa [ku, sub_eq_add_neg, Algebra.algebraMap_eq_smul_one] using (ku.add (-a) hku).isUnit diff --git a/Mathlib/Analysis/Normed/Field/ProperSpace.lean b/Mathlib/Analysis/Normed/Field/ProperSpace.lean index 2c8c91cffa8cd7..58a51d47a39f0c 100644 --- a/Mathlib/Analysis/Normed/Field/ProperSpace.lean +++ b/Mathlib/Analysis/Normed/Field/ProperSpace.lean @@ -42,7 +42,7 @@ lemma ProperSpace.of_nontriviallyNormedField_of_weaklyLocallyCompactSpace ext simp only [mem_closedBall, dist_zero_right, Set.mem_smul_set_iff_inv_smul_mem₀ this, smul_eq_mul, norm_mul, norm_inv, norm_pow, - inv_mul_le_iff (by simpa only [norm_pow] using norm_pos_iff.mpr this)] + inv_mul_le_iff₀ (by simpa only [norm_pow] using norm_pos_iff.mpr this)] have hTop : Tendsto (fun n ↦ ‖c‖^n * r) atTop atTop := Tendsto.atTop_mul_const rpos (tendsto_pow_atTop_atTop_of_one_lt hc) exact .of_seq_closedBall hTop (Eventually.of_forall hC) diff --git a/Mathlib/Analysis/Normed/Group/Quotient.lean b/Mathlib/Analysis/Normed/Group/Quotient.lean index 0759e6a9c2fc66..9acc022a5fcfbf 100644 --- a/Mathlib/Analysis/Normed/Group/Quotient.lean +++ b/Mathlib/Analysis/Normed/Group/Quotient.lean @@ -282,9 +282,9 @@ theorem _root_.QuotientAddGroup.norm_lift_apply_le {S : AddSubgroup M} (f : Norm rcases mk_surjective x with ⟨x, rfl⟩ simpa [h] using le_opNorm f x | inr h => - rw [← not_lt, ← _root_.lt_div_iff' h, norm_lt_iff] + rw [← not_lt, ← lt_div_iff₀' h, norm_lt_iff] rintro ⟨x, rfl, hx⟩ - exact ((lt_div_iff' h).1 hx).not_le (le_opNorm f x) + exact ((lt_div_iff₀' h).1 hx).not_le (le_opNorm f x) /-- The operator norm of the projection is `1` if the subspace is not dense. -/ theorem norm_normedMk (S : AddSubgroup M) (h : (S.topologicalClosure : Set M) ≠ univ) : diff --git a/Mathlib/Analysis/Normed/Module/Basic.lean b/Mathlib/Analysis/Normed/Module/Basic.lean index a14d459bc62801..b35a5c4e3baf1d 100644 --- a/Mathlib/Analysis/Normed/Module/Basic.lean +++ b/Mathlib/Analysis/Normed/Module/Basic.lean @@ -186,7 +186,7 @@ theorem NormedSpace.exists_lt_norm (c : ℝ) : ∃ x : E, c < ‖x‖ := by rcases exists_ne (0 : E) with ⟨x, hx⟩ rcases NormedField.exists_lt_norm 𝕜 (c / ‖x‖) with ⟨r, hr⟩ use r • x - rwa [norm_smul, ← _root_.div_lt_iff] + rwa [norm_smul, ← div_lt_iff₀] rwa [norm_pos_iff] protected theorem NormedSpace.unbounded_univ : ¬Bornology.IsBounded (univ : Set E) := fun h => diff --git a/Mathlib/Analysis/NormedSpace/OperatorNorm/NNNorm.lean b/Mathlib/Analysis/NormedSpace/OperatorNorm/NNNorm.lean index 7461f70c18dfc8..020de596c8f44c 100644 --- a/Mathlib/Analysis/NormedSpace/OperatorNorm/NNNorm.lean +++ b/Mathlib/Analysis/NormedSpace/OperatorNorm/NNNorm.lean @@ -156,7 +156,7 @@ theorem exists_lt_apply_of_lt_opNNNorm {𝕜 𝕜₂ E F : Type*} [NormedAddComm obtain ⟨k, hk₁, hk₂⟩ := NormedField.exists_lt_nnnorm_lt 𝕜 hy refine ⟨k • y, (nnnorm_smul k y).symm ▸ (NNReal.lt_inv_iff_mul_lt hy').1 hk₂, ?_⟩ have : ‖σ₁₂ k‖₊ = ‖k‖₊ := Subtype.ext RingHomIsometric.is_iso - rwa [map_smulₛₗ f, nnnorm_smul, ← NNReal.div_lt_iff hfy, div_eq_mul_inv, this] + rwa [map_smulₛₗ f, nnnorm_smul, ← div_lt_iff₀ hfy.bot_lt, div_eq_mul_inv, this] @[deprecated (since := "2024-02-02")] alias exists_lt_apply_of_lt_op_nnnorm := exists_lt_apply_of_lt_opNNNorm diff --git a/Mathlib/Analysis/NormedSpace/Pointwise.lean b/Mathlib/Analysis/NormedSpace/Pointwise.lean index bb061dfe9e1866..866ca33561073d 100644 --- a/Mathlib/Analysis/NormedSpace/Pointwise.lean +++ b/Mathlib/Analysis/NormedSpace/Pointwise.lean @@ -78,7 +78,7 @@ theorem smul_ball {c : 𝕜} (hc : c ≠ 0) (x : E) (r : ℝ) : c • ball x r = ext y rw [mem_smul_set_iff_inv_smul_mem₀ hc] conv_lhs => rw [← inv_smul_smul₀ hc x] - simp [← div_eq_inv_mul, div_lt_iff (norm_pos_iff.2 hc), mul_comm _ r, dist_smul₀] + simp [← div_eq_inv_mul, div_lt_iff₀ (norm_pos_iff.2 hc), mul_comm _ r, dist_smul₀] theorem smul_unitBall {c : 𝕜} (hc : c ≠ 0) : c • ball (0 : E) (1 : ℝ) = ball (0 : E) ‖c‖ := by rw [_root_.smul_ball hc, smul_zero, mul_one] diff --git a/Mathlib/Analysis/NormedSpace/RieszLemma.lean b/Mathlib/Analysis/NormedSpace/RieszLemma.lean index 415a55f95a3f48..553d89feaaa42b 100644 --- a/Mathlib/Analysis/NormedSpace/RieszLemma.lean +++ b/Mathlib/Analysis/NormedSpace/RieszLemma.lean @@ -50,7 +50,7 @@ theorem riesz_lemma {F : Subspace 𝕜 E} (hFc : IsClosed (F : Set E)) (hF : ∃ simp only [r', max_lt_iff, hr, true_and] norm_num have hlt : 0 < r' := lt_of_lt_of_le (by norm_num) (le_max_right r 2⁻¹) - have hdlt : d < d / r' := (lt_div_iff hlt).mpr ((mul_lt_iff_lt_one_right hdp).2 hr') + have hdlt : d < d / r' := (lt_div_iff₀ hlt).mpr ((mul_lt_iff_lt_one_right hdp).2 hr') obtain ⟨y₀, hy₀F, hxy₀⟩ : ∃ y ∈ F, dist x y < d / r' := (Metric.infDist_lt_iff hFn).mp hdlt have x_ne_y₀ : x - y₀ ∉ F := by by_contra h @@ -63,7 +63,7 @@ theorem riesz_lemma {F : Subspace 𝕜 E} (hFc : IsClosed (F : Set E)) (hF : ∃ r * ‖x - y₀‖ ≤ r' * ‖x - y₀‖ := by gcongr; apply le_max_left _ < d := by rw [← dist_eq_norm] - exact (lt_div_iff' hlt).1 hxy₀ + exact (lt_div_iff₀' hlt).1 hxy₀ _ ≤ dist x (y₀ + y) := Metric.infDist_le_dist_of_mem hy₀y _ = ‖x - y₀ - y‖ := by rw [sub_sub, dist_eq_norm] @@ -82,7 +82,7 @@ theorem riesz_lemma_of_norm_lt {c : 𝕜} (hc : 1 < ‖c‖) {R : ℝ} (hR : ‖ ∃ x₀ : E, ‖x₀‖ ≤ R ∧ ∀ y ∈ F, 1 ≤ ‖x₀ - y‖ := by have Rpos : 0 < R := (norm_nonneg _).trans_lt hR have : ‖c‖ / R < 1 := by - rw [div_lt_iff Rpos] + rw [div_lt_iff₀ Rpos] simpa using hR rcases riesz_lemma hFc hF this with ⟨x, xF, hx⟩ have x0 : x ≠ 0 := fun H => by simp [H] at xF diff --git a/Mathlib/Analysis/Seminorm.lean b/Mathlib/Analysis/Seminorm.lean index c77e95d8e0c87c..c59be01c216894 100644 --- a/Mathlib/Analysis/Seminorm.lean +++ b/Mathlib/Analysis/Seminorm.lean @@ -658,7 +658,7 @@ theorem ball_smul (p : Seminorm 𝕜 E) {c : NNReal} (hc : 0 < c) (r : ℝ) (x : (c • p).ball x r = p.ball x (r / c) := by ext rw [mem_ball, mem_ball, smul_apply, NNReal.smul_def, smul_eq_mul, mul_comm, - lt_div_iff (NNReal.coe_pos.mpr hc)] + lt_div_iff₀ (NNReal.coe_pos.mpr hc)] theorem closedBall_smul (p : Seminorm 𝕜 E) {c : NNReal} (hc : 0 < c) (r : ℝ) (x : E) : (c • p).closedBall x r = p.closedBall x (r / c) := by @@ -899,7 +899,7 @@ theorem smul_ball_zero {p : Seminorm 𝕜 E} {k : 𝕜} {r : ℝ} (hk : k ≠ 0) k • p.ball 0 r = p.ball 0 (‖k‖ * r) := by ext rw [mem_smul_set_iff_inv_smul_mem₀ hk, p.mem_ball_zero, p.mem_ball_zero, map_smul_eq_mul, - norm_inv, ← div_eq_inv_mul, div_lt_iff (norm_pos_iff.2 hk), mul_comm] + norm_inv, ← div_eq_inv_mul, div_lt_iff₀ (norm_pos_iff.2 hk), mul_comm] theorem smul_closedBall_subset {p : Seminorm 𝕜 E} {k : 𝕜} {r : ℝ} : k • p.closedBall 0 r ⊆ p.closedBall 0 (‖k‖ * r) := by @@ -952,7 +952,7 @@ protected theorem absorbent_closedBall (hpr : p x < r) : Absorbent 𝕜 (closedB theorem smul_ball_preimage (p : Seminorm 𝕜 E) (y : E) (r : ℝ) (a : 𝕜) (ha : a ≠ 0) : (a • ·) ⁻¹' p.ball y r = p.ball (a⁻¹ • y) (r / ‖a‖) := Set.ext fun _ => by - rw [mem_preimage, mem_ball, mem_ball, lt_div_iff (norm_pos_iff.mpr ha), mul_comm, ← + rw [mem_preimage, mem_ball, mem_ball, lt_div_iff₀ (norm_pos_iff.mpr ha), mul_comm, ← map_smul_eq_mul p, smul_sub, smul_inv_smul₀ ha] end NormedField @@ -1047,7 +1047,7 @@ theorem continuousAt_zero' [TopologicalSpace E] [ContinuousConstSMul 𝕜 E] {p obtain ⟨k, hk₀, hk⟩ : ∃ k : 𝕜, 0 < ‖k‖ ∧ ‖k‖ * r < ε := by rcases le_or_lt r 0 with hr | hr · use 1; simpa using hr.trans_lt hε - · simpa [lt_div_iff hr] using exists_norm_lt 𝕜 (div_pos hε hr) + · simpa [lt_div_iff₀ hr] using exists_norm_lt 𝕜 (div_pos hε hr) rw [← set_smul_mem_nhds_zero_iff (norm_pos_iff.1 hk₀), smul_closedBall_zero hk₀] at hp exact mem_of_superset hp <| p.closedBall_mono hk.le @@ -1184,9 +1184,9 @@ lemma rescale_to_shell_zpow (p : Seminorm 𝕜 E) {c : 𝕜} (hc : 1 < ‖c‖) refine ⟨-(n+1), ?_, ?_, ?_, ?_⟩ · show c ^ (-(n + 1)) ≠ 0; exact zpow_ne_zero _ (norm_pos_iff.1 cpos) · show p ((c ^ (-(n + 1))) • x) < ε - rw [map_smul_eq_mul, zpow_neg, norm_inv, ← div_eq_inv_mul, div_lt_iff cnpos, mul_comm, + rw [map_smul_eq_mul, zpow_neg, norm_inv, ← div_eq_inv_mul, div_lt_iff₀ cnpos, mul_comm, norm_zpow] - exact (div_lt_iff εpos).1 (hn.2) + exact (div_lt_iff₀ εpos).1 (hn.2) · show ε / ‖c‖ ≤ p (c ^ (-(n + 1)) • x) rw [zpow_neg, div_le_iff₀ cpos, map_smul_eq_mul, norm_inv, norm_zpow, zpow_add₀ (ne_of_gt cpos), zpow_one, mul_inv_rev, mul_comm, ← mul_assoc, ← mul_assoc, mul_inv_cancel₀ (ne_of_gt cpos), diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/Arctan.lean b/Mathlib/Analysis/SpecialFunctions/Complex/Arctan.lean index d9d625ead931a6..d5bc0c1f1b5bab 100644 --- a/Mathlib/Analysis/SpecialFunctions/Complex/Arctan.lean +++ b/Mathlib/Analysis/SpecialFunctions/Complex/Arctan.lean @@ -73,7 +73,7 @@ theorem arctan_tan {z : ℂ} (h₀ : z ≠ π / 2) (h₁ : -(π / 2) < z.re) (h rw [← exp_mul_I, ← exp_mul_I, ← exp_sub, show z * I - -z * I = 2 * (I * z) by ring, log_exp, show -I / 2 * (2 * (I * z)) = -(I * I) * z by ring, I_mul_I, neg_neg, one_mul] all_goals norm_num - · rwa [← div_lt_iff' two_pos, neg_div] + · rwa [← div_lt_iff₀' two_pos, neg_div] · rwa [← le_div_iff₀' two_pos] @[simp, norm_cast] diff --git a/Mathlib/Analysis/SpecialFunctions/Exp.lean b/Mathlib/Analysis/SpecialFunctions/Exp.lean index d9317023529a23..8d018a967ecb06 100644 --- a/Mathlib/Analysis/SpecialFunctions/Exp.lean +++ b/Mathlib/Analysis/SpecialFunctions/Exp.lean @@ -263,7 +263,7 @@ theorem tendsto_exp_div_pow_atTop (n : ℕ) : Tendsto (fun x => exp x / x ^ n) a eventually_atTop.1 ((tendsto_pow_const_div_const_pow_of_one_lt n (one_lt_exp_iff.2 zero_lt_one)).eventually (gt_mem_nhds this)) - simp only [← exp_nat_mul, mul_one, div_lt_iff, exp_pos, ← div_eq_inv_mul] at hN + simp only [← exp_nat_mul, mul_one, div_lt_iff₀, exp_pos, ← div_eq_inv_mul] at hN refine ⟨N, trivial, fun x hx => ?_⟩ rw [Set.mem_Ioi] at hx have hx₀ : 0 < x := (Nat.cast_nonneg N).trans_lt hx diff --git a/Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean b/Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean index 79be49beb847d7..86a45e8436078d 100644 --- a/Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean +++ b/Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean @@ -85,7 +85,7 @@ theorem finite_integral_rpow_sub_one_pow_aux {r : ℝ} (n : ℕ) (hnr : (n : ℝ refine IntegrableOn.setLIntegral_lt_top ?_ rw [← intervalIntegrable_iff_integrableOn_Ioc_of_le zero_le_one] apply intervalIntegral.intervalIntegrable_rpow' - rwa [neg_lt_neg_iff, inv_mul_lt_iff' hr, one_mul] + rwa [neg_lt_neg_iff, inv_mul_lt_iff₀' hr, one_mul] variable [MeasurableSpace E] [BorelSpace E] {μ : Measure E} [μ.IsAddHaarMeasure] diff --git a/Mathlib/Analysis/SpecialFunctions/Log/Base.lean b/Mathlib/Analysis/SpecialFunctions/Log/Base.lean index 23dedfcd330668..f7fafb38f92f68 100644 --- a/Mathlib/Analysis/SpecialFunctions/Log/Base.lean +++ b/Mathlib/Analysis/SpecialFunctions/Log/Base.lean @@ -423,7 +423,7 @@ lemma Real.induction_Ico_mul {P : ℝ → Prop} (x₀ r : ℝ) (hr : 1 < r) (hx intro x hx have hx' : 0 < x / x₀ := div_pos (hx₀.trans_le hx) hx₀ refine this ⌊logb r (x / x₀)⌋₊ x ?_ - rw [mem_Ico, ← div_lt_iff hx₀, ← rpow_natCast, ← logb_lt_iff_lt_rpow hr hx', Nat.cast_add, + rw [mem_Ico, ← div_lt_iff₀ hx₀, ← rpow_natCast, ← logb_lt_iff_lt_rpow hr hx', Nat.cast_add, Nat.cast_one] exact ⟨hx, Nat.lt_floor_add_one _⟩ intro n diff --git a/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean index 705e2df157be4a..c5f7769a08f9d8 100644 --- a/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean +++ b/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean @@ -296,7 +296,7 @@ theorem abs_log_mul_self_lt (x : ℝ) (h1 : 0 < x) (h2 : x ≤ 1) : |log x * x| have : 0 < 1 / x := by simpa only [one_div, inv_pos] using h1 replace := log_le_sub_one_of_pos this replace : log (1 / x) < 1 / x := by linarith - rw [log_div one_ne_zero h1.ne', log_one, zero_sub, lt_div_iff h1] at this + rw [log_div one_ne_zero h1.ne', log_one, zero_sub, lt_div_iff₀ h1] at this have aux : 0 ≤ -log x * x := by refine mul_nonneg ?_ h1.le rw [← log_inv] diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean b/Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean index 9a2469906a6612..c9a10865fd507e 100644 --- a/Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean +++ b/Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean @@ -175,7 +175,7 @@ lemma cpow_ofNat_mul' {x : ℂ} {n : ℕ} [n.AtLeastTwo] (hlt : -π < OfNat.ofNa lemma pow_cpow_nat_inv {x : ℂ} {n : ℕ} (h₀ : n ≠ 0) (hlt : -(π / n) < x.arg) (hle : x.arg ≤ π / n) : (x ^ n) ^ (n⁻¹ : ℂ) = x := by rw [← cpow_nat_mul', mul_inv_cancel₀ (Nat.cast_ne_zero.2 h₀), cpow_one] - · rwa [← div_lt_iff' (Nat.cast_pos.2 h₀.bot_lt), neg_div] + · rwa [← div_lt_iff₀' (Nat.cast_pos.2 h₀.bot_lt), neg_div] · rwa [← le_div_iff₀' (Nat.cast_pos.2 h₀.bot_lt)] lemma pow_cpow_ofNat_inv {x : ℂ} {n : ℕ} [n.AtLeastTwo] (hlt : -(π / OfNat.ofNat n) < x.arg) diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean b/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean index 0bfe01f772deed..80400c08a6e5db 100644 --- a/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean +++ b/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean @@ -823,7 +823,7 @@ theorem rpow_le_one_iff_of_pos (hx : 0 < x) : x ^ y ≤ 1 ↔ 1 ≤ x ∧ y ≤ /-- Bound for `|log x * x ^ t|` in the interval `(0, 1]`, for positive real `t`. -/ theorem abs_log_mul_self_rpow_lt (x t : ℝ) (h1 : 0 < x) (h2 : x ≤ 1) (ht : 0 < t) : |log x * x ^ t| < 1 / t := by - rw [lt_div_iff ht] + rw [lt_div_iff₀ ht] have := abs_log_mul_self_lt (x ^ t) (rpow_pos_of_pos h1 t) (rpow_le_one h1.le h2 ht.le) rwa [log_rpow h1, mul_assoc, abs_mul, abs_of_pos ht, mul_comm] at this diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean index 364f5e72076c6d..c5ed6917124713 100644 --- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean +++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean @@ -554,7 +554,7 @@ theorem nsmul_toReal_eq_mul {n : ℕ} (h : n ≠ 0) {θ : Angle} : (n • θ).toReal = n * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / n) (π / n) := by nth_rw 1 [← coe_toReal θ] have h' : 0 < (n : ℝ) := mod_cast Nat.pos_of_ne_zero h - rw [← coe_nsmul, nsmul_eq_mul, toReal_coe_eq_self_iff, Set.mem_Ioc, div_lt_iff' h', + rw [← coe_nsmul, nsmul_eq_mul, toReal_coe_eq_self_iff, Set.mem_Ioc, div_lt_iff₀' h', le_div_iff₀' h'] theorem two_nsmul_toReal_eq_two_mul {θ : Angle} : @@ -585,7 +585,7 @@ theorem two_nsmul_toReal_eq_two_mul_sub_two_pi {θ : Angle} : rw [← coe_nsmul, two_nsmul, ← two_mul, toReal_coe_eq_self_sub_two_pi_iff, Set.mem_Ioc] exact ⟨fun h => by linarith, fun h => - ⟨(div_lt_iff' (zero_lt_two' ℝ)).1 h, by linarith [pi_pos, toReal_le_pi θ]⟩⟩ + ⟨(div_lt_iff₀' (zero_lt_two' ℝ)).1 h, by linarith [pi_pos, toReal_le_pi θ]⟩⟩ theorem two_zsmul_toReal_eq_two_mul_sub_two_pi {θ : Angle} : ((2 : ℤ) • θ).toReal = 2 * θ.toReal - 2 * π ↔ π / 2 < θ.toReal := by diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean index 2ea81c6afbe959..ee71f3e92b789f 100644 --- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean +++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean @@ -208,7 +208,7 @@ lemma arctan_add_arctan_lt_pi_div_two {x y : ℝ} (h : x * y < 1) : arctan x + a cases' le_or_lt y 0 with hy hy · rw [← add_zero (π / 2), ← arctan_zero] exact add_lt_add_of_lt_of_le (arctan_lt_pi_div_two _) (tanOrderIso.symm.monotone hy) - · rw [← lt_div_iff hy, ← inv_eq_one_div] at h + · rw [← lt_div_iff₀ hy, ← inv_eq_one_div] at h replace h : arctan x < arctan y⁻¹ := tanOrderIso.symm.strictMono h rwa [arctan_inv_of_pos hy, lt_tsub_iff_right] at h diff --git a/Mathlib/Analysis/SpecificLimits/FloorPow.lean b/Mathlib/Analysis/SpecificLimits/FloorPow.lean index ae6a39293a1df2..68cd1103fc6e61 100644 --- a/Mathlib/Analysis/SpecificLimits/FloorPow.lean +++ b/Mathlib/Analysis/SpecificLimits/FloorPow.lean @@ -236,7 +236,7 @@ theorem sum_div_pow_sq_le_div_sq (N : ℕ) {j : ℝ} (hj : 0 < j) {c : ℝ} (hc simp only [hi.1, mem_Ico, and_true] apply Nat.floor_le_of_le apply le_of_lt - rw [div_lt_iff (Real.log_pos hc), ← Real.log_pow] + rw [div_lt_iff₀ (Real.log_pos hc), ← Real.log_pow] exact Real.log_lt_log hj hi.2 _ = ∑ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N, (c⁻¹ ^ 2) ^ i := by congr 1 with i diff --git a/Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean b/Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean index 9b660a299371d1..076f7c450bcdee 100644 --- a/Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean +++ b/Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean @@ -356,7 +356,7 @@ theorem three_le_nValue (hN : 64 ≤ N) : 3 ≤ nValue N := by rw [rpow_natCast] exact (cast_le.2 hN).trans' (by norm_num1) apply lt_of_lt_of_le _ (log_le_log (rpow_pos_of_pos zero_lt_two _) this) - rw [log_rpow zero_lt_two, ← div_lt_iff'] + rw [log_rpow zero_lt_two, ← div_lt_iff₀'] · exact log_two_gt_d9.trans_le' (by norm_num1) · norm_num1 @@ -459,7 +459,7 @@ theorem roth_lower_bound_explicit (hN : 4096 ≤ N) : theorem exp_four_lt : exp 4 < 64 := by rw [show (64 : ℝ) = 2 ^ ((6 : ℕ) : ℝ) by rw [rpow_natCast]; norm_num1, - ← lt_log_iff_exp_lt (rpow_pos_of_pos zero_lt_two _), log_rpow zero_lt_two, ← div_lt_iff'] + ← lt_log_iff_exp_lt (rpow_pos_of_pos zero_lt_two _), log_rpow zero_lt_two, ← div_lt_iff₀'] · exact log_two_gt_d9.trans_le' (by norm_num1) · norm_num diff --git a/Mathlib/Combinatorics/Schnirelmann.lean b/Mathlib/Combinatorics/Schnirelmann.lean index d56f44bd816fff..266093dff23aba 100644 --- a/Mathlib/Combinatorics/Schnirelmann.lean +++ b/Mathlib/Combinatorics/Schnirelmann.lean @@ -196,7 +196,7 @@ lemma schnirelmannDensity_finset (A : Finset ℕ) : schnirelmannDensity A = 0 := let n : ℕ := ⌊A.card / ε⌋₊ + 1 have hn : 0 < n := Nat.succ_pos _ use n, hn - rw [div_lt_iff (Nat.cast_pos.2 hn), ← div_lt_iff' hε, Nat.cast_add_one] + rw [div_lt_iff₀ (Nat.cast_pos.2 hn), ← div_lt_iff₀' hε, Nat.cast_add_one] exact (Nat.lt_floor_add_one _).trans_le' <| by gcongr; simp [subset_iff] /-- The Schnirelmann density of any finite set is `0`. -/ diff --git a/Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean b/Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean index 251ede22462dd4..ec596991292565 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean @@ -175,8 +175,8 @@ theorem initialBound_pos : 0 < initialBound ε l := theorem hundred_lt_pow_initialBound_mul {ε : ℝ} (hε : 0 < ε) (l : ℕ) : 100 < ↑4 ^ initialBound ε l * ε ^ 5 := by - rw [← rpow_natCast 4, ← div_lt_iff (pow_pos hε 5), lt_rpow_iff_log_lt _ zero_lt_four, ← - div_lt_iff, initialBound, Nat.cast_max, Nat.cast_max] + rw [← rpow_natCast 4, ← div_lt_iff₀ (pow_pos hε 5), lt_rpow_iff_log_lt _ zero_lt_four, ← + div_lt_iff₀, initialBound, Nat.cast_max, Nat.cast_max] · push_cast exact lt_max_of_lt_right (lt_max_of_lt_right <| Nat.lt_floor_add_one _) · exact log_pos (by norm_num) diff --git a/Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean b/Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean index a6610b54a4adee..572c8e65f679c3 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean @@ -276,7 +276,7 @@ lemma IsEquipartition.card_interedges_sparsePairs_le' (hP : P.IsEquipartition) · gcongr with UV hUV obtain ⟨U, V⟩ := UV simp [mk_mem_sparsePairs, ← card_interedges_div_card] at hUV - refine ((div_lt_iff ?_).1 hUV.2.2.2).le + refine ((div_lt_iff₀ ?_).1 hUV.2.2.2).le exact mul_pos (Nat.cast_pos.2 (P.nonempty_of_mem_parts hUV.1).card_pos) (Nat.cast_pos.2 (P.nonempty_of_mem_parts hUV.2.1).card_pos) norm_cast diff --git a/Mathlib/Data/Complex/Exponential.lean b/Mathlib/Data/Complex/Exponential.lean index cd187d52acfae4..9c2622348ebe21 100644 --- a/Mathlib/Data/Complex/Exponential.lean +++ b/Mathlib/Data/Complex/Exponential.lean @@ -28,7 +28,7 @@ theorem isCauSeq_abs_exp (z : ℂ) : let ⟨n, hn⟩ := exists_nat_gt (abs z) have hn0 : (0 : ℝ) < n := lt_of_le_of_lt (abs.nonneg _) hn IsCauSeq.series_ratio_test n (abs z / n) (div_nonneg (abs.nonneg _) (le_of_lt hn0)) - (by rwa [div_lt_iff hn0, one_mul]) fun m hm => by + (by rwa [div_lt_iff₀ hn0, one_mul]) fun m hm => by rw [abs_abs, abs_abs, Nat.factorial_succ, pow_succ', mul_comm m.succ, Nat.cast_mul, ← div_div, mul_div_assoc, mul_div_right_comm, map_mul, map_div₀, abs_natCast] gcongr @@ -1398,7 +1398,7 @@ theorem exp_bound_div_one_sub_of_interval' {x : ℝ} (h1 : 0 < x) (h2 : x < 1) : repeat erw [Finset.sum_range_succ] norm_num [Nat.factorial] nlinarith - _ < 1 / (1 - x) := by rw [lt_div_iff] <;> nlinarith + _ < 1 / (1 - x) := by rw [lt_div_iff₀] <;> nlinarith theorem exp_bound_div_one_sub_of_interval {x : ℝ} (h1 : 0 ≤ x) (h2 : x < 1) : Real.exp x ≤ 1 / (1 - x) := by diff --git a/Mathlib/Data/Int/CardIntervalMod.lean b/Mathlib/Data/Int/CardIntervalMod.lean index 045f7ee4c7aa86..b5725e3f43eb68 100644 --- a/Mathlib/Data/Int/CardIntervalMod.lean +++ b/Mathlib/Data/Int/CardIntervalMod.lean @@ -43,14 +43,14 @@ include hr lemma Ico_filter_dvd_eq : (Ico a b).filter (r ∣ ·) = (Ico ⌈a / (r : ℚ)⌉ ⌈b / (r : ℚ)⌉).map ⟨(· * r), mul_left_injective₀ hr.ne'⟩ := by ext x - simp only [mem_map, mem_filter, mem_Ico, ceil_le, lt_ceil, div_le_iff₀, lt_div_iff, + simp only [mem_map, mem_filter, mem_Ico, ceil_le, lt_ceil, div_le_iff₀, lt_div_iff₀, dvd_iff_exists_eq_mul_left, cast_pos.2 hr, ← cast_mul, cast_lt, cast_le] aesop lemma Ioc_filter_dvd_eq : (Ioc a b).filter (r ∣ ·) = (Ioc ⌊a / (r : ℚ)⌋ ⌊b / (r : ℚ)⌋).map ⟨(· * r), mul_left_injective₀ hr.ne'⟩ := by ext x - simp only [mem_map, mem_filter, mem_Ioc, floor_lt, le_floor, div_lt_iff, le_div_iff₀, + simp only [mem_map, mem_filter, mem_Ioc, floor_lt, le_floor, div_lt_iff₀, le_div_iff₀, dvd_iff_exists_eq_mul_left, cast_pos.2 hr, ← cast_mul, cast_lt, cast_le] aesop @@ -125,7 +125,7 @@ theorem count_modEq_card_eq_ceil (v : ℕ) : rw [← div_add_mod v r, cast_add, cast_mul, add_comm] tactic => simp_rw [← sub_sub, sub_div (_ - _), mul_div_cancel_left₀ _ hr'.ne', ceil_sub_nat] rw [sub_sub_sub_cancel_right, cast_zero, zero_sub] - rw [sub_eq_self, ceil_eq_zero_iff, Set.mem_Ioc, div_le_iff₀ hr', lt_div_iff hr', neg_one_mul, + rw [sub_eq_self, ceil_eq_zero_iff, Set.mem_Ioc, div_le_iff₀ hr', lt_div_iff₀ hr', neg_one_mul, zero_mul, neg_lt_neg_iff, cast_lt] exact ⟨mod_lt _ hr, by simp⟩ @@ -139,10 +139,10 @@ theorem count_modEq_card (v : ℕ) : mul_div_cancel_left₀ _ hr'.ne', add_comm, Int.ceil_add_nat, add_comm] rw [add_right_inj] split_ifs with h - · rw [← cast_sub h.le, Int.ceil_eq_iff, div_le_iff₀ hr', lt_div_iff hr', cast_one, Int.cast_one, + · rw [← cast_sub h.le, Int.ceil_eq_iff, div_le_iff₀ hr', lt_div_iff₀ hr', cast_one, Int.cast_one, sub_self, zero_mul, cast_pos, tsub_pos_iff_lt, one_mul, cast_le, tsub_le_iff_right] exact ⟨h, ((mod_lt _ hr).trans_le (by simp)).le⟩ - · rw [cast_zero, ceil_eq_zero_iff, Set.mem_Ioc, div_le_iff₀ hr', lt_div_iff hr', zero_mul, + · rw [cast_zero, ceil_eq_zero_iff, Set.mem_Ioc, div_le_iff₀ hr', lt_div_iff₀ hr', zero_mul, tsub_nonpos, ← neg_eq_neg_one_mul, neg_lt_sub_iff_lt_add, ← cast_add, cast_lt, cast_le] exact ⟨(mod_lt _ hr).trans_le (by simp), not_lt.mp h⟩ diff --git a/Mathlib/Data/NNReal/Basic.lean b/Mathlib/Data/NNReal/Basic.lean index da7622c261a6f6..796985dd715ad0 100644 --- a/Mathlib/Data/NNReal/Basic.lean +++ b/Mathlib/Data/NNReal/Basic.lean @@ -841,25 +841,25 @@ theorem div_le_of_le_mul' {a b c : ℝ≥0} (h : a ≤ b * c) : a / b ≤ c := @[deprecated le_div_iff₀ (since := "2024-08-21")] protected lemma le_div_iff {a b r : ℝ≥0} (hr : r ≠ 0) : a ≤ b / r ↔ a * r ≤ b := - le_div_iff₀ <| pos_iff_ne_zero.2 hr + le_div_iff₀ hr.bot_lt -nonrec theorem le_div_iff' {a b r : ℝ≥0} (hr : r ≠ 0) : a ≤ b / r ↔ r * a ≤ b := - le_div_iff₀' <| pos_iff_ne_zero.2 hr +@[deprecated le_div_iff₀' (since := "2024-10-02")] +theorem le_div_iff' {a b r : ℝ≥0} (hr : r ≠ 0) : a ≤ b / r ↔ r * a ≤ b := le_div_iff₀' hr.bot_lt -theorem div_lt_iff {a b r : ℝ≥0} (hr : r ≠ 0) : a / r < b ↔ a < b * r := - lt_iff_lt_of_le_iff_le (le_div_iff₀ (pos_iff_ne_zero.2 hr)) +@[deprecated div_lt_iff₀ (since := "2024-10-02")] +theorem div_lt_iff {a b r : ℝ≥0} (hr : r ≠ 0) : a / r < b ↔ a < b * r := div_lt_iff₀ hr.bot_lt -theorem div_lt_iff' {a b r : ℝ≥0} (hr : r ≠ 0) : a / r < b ↔ a < r * b := - lt_iff_lt_of_le_iff_le (le_div_iff₀' (pos_iff_ne_zero.2 hr)) +@[deprecated div_lt_iff₀' (since := "2024-10-02")] +theorem div_lt_iff' {a b r : ℝ≥0} (hr : r ≠ 0) : a / r < b ↔ a < r * b := div_lt_iff₀' hr.bot_lt -theorem lt_div_iff {a b r : ℝ≥0} (hr : r ≠ 0) : a < b / r ↔ a * r < b := - lt_iff_lt_of_le_iff_le (div_le_iff₀ (pos_iff_ne_zero.2 hr)) +@[deprecated lt_div_iff₀ (since := "2024-10-02")] +theorem lt_div_iff {a b r : ℝ≥0} (hr : r ≠ 0) : a < b / r ↔ a * r < b := lt_div_iff₀ hr.bot_lt -theorem lt_div_iff' {a b r : ℝ≥0} (hr : r ≠ 0) : a < b / r ↔ r * a < b := - lt_iff_lt_of_le_iff_le (div_le_iff₀' (pos_iff_ne_zero.2 hr)) +@[deprecated lt_div_iff₀' (since := "2024-10-02")] +theorem lt_div_iff' {a b r : ℝ≥0} (hr : r ≠ 0) : a < b / r ↔ r * a < b := lt_div_iff₀' hr.bot_lt theorem mul_lt_of_lt_div {a b r : ℝ≥0} (h : a < b / r) : a * r < b := - (lt_div_iff fun hr => False.elim <| by simp [hr] at h).1 h + (lt_div_iff₀ <| pos_iff_ne_zero.2 fun hr => False.elim <| by simp [hr] at h).1 h theorem div_le_div_left_of_le {a b c : ℝ≥0} (c0 : c ≠ 0) (cb : c ≤ b) : a / b ≤ a / c := @@ -884,8 +884,7 @@ nonrec theorem half_lt_self {a : ℝ≥0} (h : a ≠ 0) : a / 2 < a := half_lt_self h.bot_lt theorem div_lt_one_of_lt {a b : ℝ≥0} (h : a < b) : a / b < 1 := by - rwa [div_lt_iff, one_mul] - exact ne_of_gt (lt_of_le_of_lt (zero_le _) h) + rwa [div_lt_iff₀ h.bot_lt, one_mul] theorem _root_.Real.toNNReal_inv {x : ℝ} : Real.toNNReal x⁻¹ = (Real.toNNReal x)⁻¹ := by rcases le_total 0 x with hx | hx @@ -902,7 +901,7 @@ theorem _root_.Real.toNNReal_div' {x y : ℝ} (hy : 0 ≤ y) : rw [div_eq_inv_mul, div_eq_inv_mul, Real.toNNReal_mul (inv_nonneg.2 hy), Real.toNNReal_inv] theorem inv_lt_one_iff {x : ℝ≥0} (hx : x ≠ 0) : x⁻¹ < 1 ↔ 1 < x := by - rw [← one_div, div_lt_iff hx, one_mul] + rw [← one_div, div_lt_iff₀ hx.bot_lt, one_mul] theorem zpow_pos {x : ℝ≥0} (hx : x ≠ 0) (n : ℤ) : 0 < x ^ n := zpow_pos_of_pos hx.bot_lt _ diff --git a/Mathlib/Data/Real/Archimedean.lean b/Mathlib/Data/Real/Archimedean.lean index aab8b86739170d..f27de94d155e4a 100644 --- a/Mathlib/Data/Real/Archimedean.lean +++ b/Mathlib/Data/Real/Archimedean.lean @@ -68,7 +68,7 @@ theorem exists_isLUB (hne : s.Nonempty) (hbdd : BddAbove s) : ∃ x, IsLUB s x : intro n n0 y yS have := (Int.sub_one_lt_floor _).trans_le (Int.cast_le.2 <| (hf n).2 _ ⟨y, yS, Int.floor_le _⟩) simp only [Rat.cast_div, Rat.cast_intCast, Rat.cast_natCast, gt_iff_lt] - rwa [lt_div_iff (Nat.cast_pos.2 n0 : (_ : ℝ) < _), sub_mul, inv_mul_cancel₀] + rwa [lt_div_iff₀ (Nat.cast_pos.2 n0 : (_ : ℝ) < _), sub_mul, inv_mul_cancel₀] exact ne_of_gt (Nat.cast_pos.2 n0) have hg : IsCauSeq abs (fun n => f n / n : ℕ → ℚ) := by intro ε ε0 diff --git a/Mathlib/Data/Real/Pi/Bounds.lean b/Mathlib/Data/Real/Pi/Bounds.lean index 53573cbcf7b0bb..9a77915281ee60 100644 --- a/Mathlib/Data/Real/Pi/Bounds.lean +++ b/Mathlib/Data/Real/Pi/Bounds.lean @@ -23,7 +23,7 @@ namespace Real theorem pi_gt_sqrtTwoAddSeries (n : ℕ) : 2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n) < π := by have : √(2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) < π := by - rw [← lt_div_iff, ← sin_pi_over_two_pow_succ] + rw [← lt_div_iff₀, ← sin_pi_over_two_pow_succ] focus apply sin_lt apply div_pos pi_pos @@ -34,7 +34,7 @@ theorem pi_gt_sqrtTwoAddSeries (n : ℕ) : 2 ^ (n + 1) * √(2 - sqrtTwoAddSerie theorem pi_lt_sqrtTwoAddSeries (n : ℕ) : π < 2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n) + 1 / 4 ^ n := by have : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * (2 : ℝ) ^ (n + 2) := by - rw [← div_lt_iff (by norm_num), ← sin_pi_over_two_pow_succ] + rw [← div_lt_iff₀ (by norm_num), ← sin_pi_over_two_pow_succ] refine lt_of_lt_of_le (lt_add_of_sub_right_lt (sin_gt_sub_cube ?_ ?_)) ?_ · apply div_pos pi_pos; apply pow_pos; norm_num · rw [div_le_iff₀'] diff --git a/Mathlib/Data/Real/Pi/Irrational.lean b/Mathlib/Data/Real/Pi/Irrational.lean index 479d737a940f85..778010911a87f2 100644 --- a/Mathlib/Data/Real/Pi/Irrational.lean +++ b/Mathlib/Data/Real/Pi/Irrational.lean @@ -279,13 +279,13 @@ private lemma not_irrational_exists_rep {x : ℝ} : obtain ⟨a, b, hb, h⟩ := not_irrational_exists_rep h' have ha : (0 : ℝ) < a := by have : 0 < (a : ℝ) / b := h ▸ pi_div_two_pos - rwa [lt_div_iff (by positivity), zero_mul] at this + rwa [lt_div_iff₀ (by positivity), zero_mul] at this have k (n : ℕ) : 0 < (a : ℝ) ^ (2 * n + 1) / n ! := by positivity have j : ∀ᶠ n : ℕ in atTop, (a : ℝ) ^ (2 * n + 1) / n ! * I n (π / 2) < 1 := by have := eventually_lt_of_tendsto_lt (show (0 : ℝ) < 1 / 2 by norm_num) (tendsto_pow_div_factorial_at_top_aux a) filter_upwards [this] with n hn - rw [lt_div_iff (zero_lt_two : (0 : ℝ) < 2)] at hn + rw [lt_div_iff₀ (zero_lt_two : (0 : ℝ) < 2)] at hn exact hn.trans_le' (mul_le_mul_of_nonneg_left (I_le _) (by positivity)) obtain ⟨n, hn⟩ := j.exists have hn' : 0 < a ^ (2 * n + 1) / n ! * I n (π / 2) := mul_pos (k _) I_pos diff --git a/Mathlib/Data/Set/Pointwise/Interval.lean b/Mathlib/Data/Set/Pointwise/Interval.lean index 1b83b2cd5269f4..7ee860b81b0d15 100644 --- a/Mathlib/Data/Set/Pointwise/Interval.lean +++ b/Mathlib/Data/Set/Pointwise/Interval.lean @@ -509,12 +509,12 @@ variable [LinearOrderedField α] {a : α} @[simp] theorem preimage_mul_const_Iio (a : α) {c : α} (h : 0 < c) : (fun x => x * c) ⁻¹' Iio a = Iio (a / c) := - ext fun _x => (lt_div_iff h).symm + ext fun _x => (lt_div_iff₀ h).symm @[simp] theorem preimage_mul_const_Ioi (a : α) {c : α} (h : 0 < c) : (fun x => x * c) ⁻¹' Ioi a = Ioi (a / c) := - ext fun _x => (div_lt_iff h).symm + ext fun _x => (div_lt_iff₀ h).symm @[simp] theorem preimage_mul_const_Iic (a : α) {c : α} (h : 0 < c) : @@ -582,11 +582,11 @@ theorem preimage_mul_const_Icc_of_neg (a b : α) {c : α} (h : c < 0) : @[simp] theorem preimage_const_mul_Iio (a : α) {c : α} (h : 0 < c) : (c * ·) ⁻¹' Iio a = Iio (a / c) := - ext fun _x => (lt_div_iff' h).symm + ext fun _x => (lt_div_iff₀' h).symm @[simp] theorem preimage_const_mul_Ioi (a : α) {c : α} (h : 0 < c) : (c * ·) ⁻¹' Ioi a = Ioi (a / c) := - ext fun _x => (div_lt_iff' h).symm + ext fun _x => (div_lt_iff₀' h).symm @[simp] theorem preimage_const_mul_Iic (a : α) {c : α} (h : 0 < c) : (c * ·) ⁻¹' Iic a = Iic (a / c) := diff --git a/Mathlib/Geometry/Manifold/Instances/Sphere.lean b/Mathlib/Geometry/Manifold/Instances/Sphere.lean index 14fe8b165b42a7..6b82e8495e4196 100644 --- a/Mathlib/Geometry/Manifold/Instances/Sphere.lean +++ b/Mathlib/Geometry/Manifold/Instances/Sphere.lean @@ -185,7 +185,7 @@ theorem stereoInvFun_ne_north_pole (hv : ‖v‖ = 1) (w : (ℝ ∙ v)ᗮ) : rw [← inner_lt_one_iff_real_of_norm_one _ hv] · have hw : ⟪v, w⟫_ℝ = 0 := Submodule.mem_orthogonal_singleton_iff_inner_right.mp w.2 have hw' : (‖(w : E)‖ ^ 2 + 4)⁻¹ * (‖(w : E)‖ ^ 2 - 4) < 1 := by - rw [inv_mul_lt_iff'] + rw [inv_mul_lt_iff₀'] · linarith positivity simpa [real_inner_comm, inner_add_right, inner_smul_right, real_inner_self_eq_norm_mul_norm, hw, diff --git a/Mathlib/Geometry/Manifold/IntegralCurve.lean b/Mathlib/Geometry/Manifold/IntegralCurve.lean index 01130e726c4b7a..064e40fa40d71e 100644 --- a/Mathlib/Geometry/Manifold/IntegralCurve.lean +++ b/Mathlib/Geometry/Manifold/IntegralCurve.lean @@ -266,7 +266,7 @@ lemma IsIntegralCurveAt.comp_mul_ne_zero (hγ : IsIntegralCurveAt γ v t₀) {a convert h.comp_mul a ext t rw [mem_setOf_eq, Metric.mem_ball, Metric.mem_ball, Real.dist_eq, Real.dist_eq, - lt_div_iff (abs_pos.mpr ha), ← abs_mul, sub_mul, div_mul_cancel₀ _ ha] + lt_div_iff₀ (abs_pos.mpr ha), ← abs_mul, sub_mul, div_mul_cancel₀ _ ha] lemma isIntegralCurveAt_comp_mul_ne_zero {a : ℝ} (ha : a ≠ 0) : IsIntegralCurveAt γ v t₀ ↔ IsIntegralCurveAt (γ ∘ (· * a)) (a • v) (t₀ / a) := by diff --git a/Mathlib/LinearAlgebra/Matrix/Gershgorin.lean b/Mathlib/LinearAlgebra/Matrix/Gershgorin.lean index e6dd7b5af91ea3..06f6a65c35c43e 100644 --- a/Mathlib/LinearAlgebra/Matrix/Gershgorin.lean +++ b/Mathlib/LinearAlgebra/Matrix/Gershgorin.lean @@ -37,7 +37,7 @@ theorem eigenvalue_mem_ball {μ : K} (hμ : Module.End.HasEigenvalue (Matrix.toL refine (h_i ▸ Finset.le_sup' (fun i => ‖v i‖) (Finset.mem_univ j)).trans ?_ exact norm_le_zero_iff.mpr h_nz have h_le : ∀ j, ‖v j * (v i)⁻¹‖ ≤ 1 := fun j => by - rw [norm_mul, norm_inv, mul_inv_le_iff' (norm_pos_iff.mpr h_nz), one_mul] + rw [norm_mul, norm_inv, mul_inv_le_iff₀ (norm_pos_iff.mpr h_nz), one_mul] exact h_i ▸ Finset.le_sup' (fun i => ‖v i‖) (Finset.mem_univ j) simp_rw [mem_closedBall_iff_norm'] refine ⟨i, ?_⟩ diff --git a/Mathlib/MeasureTheory/Covering/DensityTheorem.lean b/Mathlib/MeasureTheory/Covering/DensityTheorem.lean index 51f94e3d8e12de..62c58768b78a65 100644 --- a/Mathlib/MeasureTheory/Covering/DensityTheorem.lean +++ b/Mathlib/MeasureTheory/Covering/DensityTheorem.lean @@ -123,7 +123,7 @@ theorem tendsto_closedBall_filterAt {K : ℝ} {x : α} {ι : Type*} {l : Filter apply (((Metric.tendsto_nhds.mp δlim _ (div_pos hε hK)).and δpos).and xmem).mono rintro j ⟨⟨hjε, hj₀ : 0 < δ j⟩, hx⟩ y hy replace hjε : (K + 1) * δ j < ε := by - simpa [abs_eq_self.mpr hj₀.le] using (lt_div_iff' hK).mp hjε + simpa [abs_eq_self.mpr hj₀.le] using (lt_div_iff₀' hK).mp hjε simp only [mem_closedBall] at hx hy ⊢ linarith [dist_triangle_right y x (w j)] diff --git a/Mathlib/MeasureTheory/Covering/Vitali.lean b/Mathlib/MeasureTheory/Covering/Vitali.lean index 5928bb689a9c9a..364031a842a496 100644 --- a/Mathlib/MeasureTheory/Covering/Vitali.lean +++ b/Mathlib/MeasureTheory/Covering/Vitali.lean @@ -112,7 +112,7 @@ theorem exists_disjoint_subfamily_covering_enlargment (B : ι → Set α) (t : S · refine ⟨a, ⟨hat, a_disj⟩, ?_⟩ simpa only [← mzero, zero_div] using δnonneg a hat · have I : m / τ < m := by - rw [div_lt_iff (zero_lt_one.trans hτ)] + rw [div_lt_iff₀ (zero_lt_one.trans hτ)] conv_lhs => rw [← mul_one m] exact (mul_lt_mul_left mpos).2 hτ rcases exists_lt_of_lt_csSup (Anonempty.image _) I with ⟨x, xA, hx⟩ diff --git a/Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean b/Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean index 31b0277e42b2fc..2d82b8b7e4d4e7 100644 --- a/Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean +++ b/Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean @@ -203,7 +203,7 @@ theorem TendstoInMeasure.exists_seq_tendsto_ae (hfg : TendstoInMeasure μ f atTo refine ⟨max N (k - 1), fun n hn_ge => lt_of_le_of_lt ?_ hk_lt_ε⟩ specialize hNx n ((le_max_left _ _).trans hn_ge) have h_inv_n_le_k : (2 : ℝ)⁻¹ ^ n ≤ 2 * (2 : ℝ)⁻¹ ^ k := by - rw [mul_comm, ← inv_mul_le_iff' (zero_lt_two' ℝ)] + rw [mul_comm, ← inv_mul_le_iff₀' (zero_lt_two' ℝ)] conv_lhs => congr rw [← pow_one (2 : ℝ)⁻¹] diff --git a/Mathlib/MeasureTheory/Integral/MeanInequalities.lean b/Mathlib/MeasureTheory/Integral/MeanInequalities.lean index 39a15c80e968f2..7b324585c63a52 100644 --- a/Mathlib/MeasureTheory/Integral/MeanInequalities.lean +++ b/Mathlib/MeasureTheory/Integral/MeanInequalities.lean @@ -312,7 +312,7 @@ theorem lintegral_Lp_mul_le_Lq_mul_Lr {α} [MeasurableSpace α] {p q r : ℝ} (h let p2 := q / p let q2 := p2.conjExponent have hp2q2 : p2.IsConjExponent q2 := - .conjExponent (by simp [p2, q2, _root_.lt_div_iff, hpq, hp0_lt]) + .conjExponent (by simp [p2, q2, _root_.lt_div_iff₀, hpq, hp0_lt]) calc (∫⁻ a : α, (f * g) a ^ p ∂μ) ^ (1 / p) = (∫⁻ a : α, f a ^ p * g a ^ p ∂μ) ^ (1 / p) := by simp_rw [Pi.mul_apply, ENNReal.mul_rpow_of_nonneg _ _ hp0] diff --git a/Mathlib/MeasureTheory/Integral/PeakFunction.lean b/Mathlib/MeasureTheory/Integral/PeakFunction.lean index 8db2aa64138ecd..df652367ebf111 100644 --- a/Mathlib/MeasureTheory/Integral/PeakFunction.lean +++ b/Mathlib/MeasureTheory/Integral/PeakFunction.lean @@ -438,7 +438,7 @@ theorem tendsto_integral_comp_smul_smul_of_integrable simp [norm_smul, abs_of_pos cpos, mul_pow]; ring _ < δ ^ finrank ℝ F * ε := by apply hM - rw [div_lt_iff δpos] at hc + rw [div_lt_iff₀ δpos] at hc simp only [mem_compl_iff, mem_closedBall, dist_zero_right, norm_smul, Real.norm_eq_abs, abs_of_nonneg cpos.le, not_le, gt_iff_lt] exact hc.trans_le (by gcongr) diff --git a/Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean b/Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean index a43d6a71335018..110086e7b67086 100644 --- a/Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean +++ b/Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean @@ -212,7 +212,7 @@ theorem MeasureTheory.volume_sum_rpow_lt [Nonempty ι] {p : ℝ} (hp : 1 ≤ p) simp_rw [← Set.preimage_smul_inv₀ (ne_of_gt hr), Set.preimage_setOf_eq, Pi.smul_apply, smul_eq_mul, abs_mul, mul_rpow (abs_nonneg _) (abs_nonneg _), abs_inv, inv_rpow (abs_nonneg _), ← Finset.mul_sum, abs_eq_self.mpr (le_of_lt hr), - inv_mul_lt_iff (rpow_pos_of_pos hr _), mul_one, ← rpow_lt_rpow_iff + inv_mul_lt_iff₀ (rpow_pos_of_pos hr _), mul_one, ← rpow_lt_rpow_iff (rpow_nonneg (h₁ _) _) (le_of_lt hr) (by linarith : 0 < p), ← rpow_mul (h₁ _), div_mul_cancel₀ _ (ne_of_gt (by linarith) : p ≠ 0), Real.rpow_one] @@ -284,7 +284,7 @@ theorem Complex.volume_sum_rpow_lt [Nonempty ι] {p : ℝ} (hp : 1 ≤ p) (r : convert addHaar_smul_of_nonneg volume (le_of_lt hr) {x : ι → ℂ | ∑ i, ‖x i‖ ^ p < 1} using 2 · simp_rw [← Set.preimage_smul_inv₀ (ne_of_gt hr), Set.preimage_setOf_eq, Pi.smul_apply, norm_smul, mul_rpow (norm_nonneg _) (norm_nonneg _), Real.norm_eq_abs, abs_inv, inv_rpow - (abs_nonneg _), ← Finset.mul_sum, abs_eq_self.mpr (le_of_lt hr), inv_mul_lt_iff + (abs_nonneg _), ← Finset.mul_sum, abs_eq_self.mpr (le_of_lt hr), inv_mul_lt_iff₀ (rpow_pos_of_pos hr _), mul_one, ← rpow_lt_rpow_iff (rpow_nonneg (h₁ _) _) (le_of_lt hr) (by linarith : 0 < p), ← rpow_mul (h₁ _), div_mul_cancel₀ _ (ne_of_gt (by linarith) : p ≠ 0), Real.rpow_one] diff --git a/Mathlib/NumberTheory/ClassNumber/AdmissibleAbs.lean b/Mathlib/NumberTheory/ClassNumber/AdmissibleAbs.lean index dd9d6a24088155..694594f1a0e408 100644 --- a/Mathlib/NumberTheory/ClassNumber/AdmissibleAbs.lean +++ b/Mathlib/NumberTheory/ClassNumber/AdmissibleAbs.lean @@ -38,7 +38,7 @@ theorem exists_partition_int (n : ℕ) {ε : ℝ} (hε : 0 < ε) {b : ℤ} (hb : refine ⟨fun i ↦ ⟨natAbs (floor ((A i % b : ℤ) / abs b • ε : ℝ)), ?_⟩, ?_⟩ · rw [← ofNat_lt, natAbs_of_nonneg (hfloor i), floor_lt] apply lt_of_lt_of_le _ (Nat.le_ceil _) - rw [Algebra.smul_def, eq_intCast, ← div_div, div_lt_div_right hε, div_lt_iff hb', one_mul, + rw [Algebra.smul_def, eq_intCast, ← div_div, div_lt_div_right hε, div_lt_iff₀ hb', one_mul, cast_lt] exact Int.emod_lt _ hb intro i₀ i₁ hi @@ -46,7 +46,7 @@ theorem exists_partition_int (n : ℕ) {ε : ℝ} (hε : 0 < ε) {b : ℤ} (hb : congr_arg ((↑) : ℕ → ℤ) (Fin.mk_eq_mk.mp hi) rw [natAbs_of_nonneg (hfloor i₀), natAbs_of_nonneg (hfloor i₁)] at hi have hi := abs_sub_lt_one_of_floor_eq_floor hi - rw [abs_sub_comm, ← sub_div, abs_div, abs_of_nonneg hbε.le, div_lt_iff hbε, one_mul] at hi + rw [abs_sub_comm, ← sub_div, abs_div, abs_of_nonneg hbε.le, div_lt_iff₀ hbε, one_mul] at hi rwa [Int.cast_abs, Int.cast_sub] /-- `abs : ℤ → ℤ` is an admissible absolute value. -/ diff --git a/Mathlib/NumberTheory/ClassNumber/AdmissibleCardPowDegree.lean b/Mathlib/NumberTheory/ClassNumber/AdmissibleCardPowDegree.lean index 7b6a30b0c651c4..c1fd34862bfb81 100644 --- a/Mathlib/NumberTheory/ClassNumber/AdmissibleCardPowDegree.lean +++ b/Mathlib/NumberTheory/ClassNumber/AdmissibleCardPowDegree.lean @@ -131,7 +131,7 @@ theorem exists_approx_polynomial {b : Fq[X]} (hb : b ≠ 0) {ε : ℝ} (hε : 0 cardPowDegree_nonzero _ h', cardPowDegree_nonzero _ hb, Algebra.smul_def, eq_intCast, Int.cast_pow, Int.cast_natCast, Int.cast_pow, Int.cast_natCast, log_mul (pow_ne_zero _ q_pos'.ne') hε.ne', ← rpow_natCast, ← rpow_natCast, log_rpow q_pos', - log_rpow q_pos', ← lt_div_iff (log_pos one_lt_q'), add_div, + log_rpow q_pos', ← lt_div_iff₀ (log_pos one_lt_q'), add_div, mul_div_cancel_right₀ _ (log_pos one_lt_q').ne'] -- And that result follows from manipulating the result from `exists_approx_polynomial_aux` -- to turn the `-⌈-stuff⌉₊` into `+ stuff`. diff --git a/Mathlib/NumberTheory/DiophantineApproximation.lean b/Mathlib/NumberTheory/DiophantineApproximation.lean index 77d109b6454200..946ac3af1f703a 100644 --- a/Mathlib/NumberTheory/DiophantineApproximation.lean +++ b/Mathlib/NumberTheory/DiophantineApproximation.lean @@ -235,7 +235,7 @@ theorem den_le_and_le_num_le_of_sub_lt_one_div_den_sq {ξ q : ℚ} · exact le_rfl · have hξ₀ : (0 : ℚ) < ξ.den := Nat.cast_pos.mpr ξ.pos rw [← Rat.num_div_den ξ, div_mul_eq_mul_div, div_sub' _ _ _ hξ₀.ne', abs_div, abs_of_pos hξ₀, - div_lt_iff hξ₀, div_mul_comm, mul_one] at h + div_lt_iff₀ hξ₀, div_mul_comm, mul_one] at h refine Nat.cast_le.mp ((one_lt_div hq₀).mp <| lt_of_le_of_lt ?_ h).le norm_cast rw [mul_comm _ q.num] @@ -422,9 +422,9 @@ private theorem aux₂ : 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v := by obtain ⟨hcop, _, h⟩ := h obtain ⟨hv₀, hv₀'⟩ := aux₀ (zero_lt_two.trans_le hv) have hv₁ : 0 < 2 * v - 1 := by linarith only [hv] - rw [← one_div, lt_div_iff (mul_pos hv₀ hv₀'), ← abs_of_pos (mul_pos hv₀ hv₀'), ← abs_mul, sub_mul, - ← mul_assoc, ← mul_assoc, div_mul_cancel₀ _ hv₀.ne', abs_sub_comm, abs_lt, lt_sub_iff_add_lt, - sub_lt_iff_lt_add, mul_assoc] at h + rw [← one_div, lt_div_iff₀ (mul_pos hv₀ hv₀'), ← abs_of_pos (mul_pos hv₀ hv₀'), ← abs_mul, + sub_mul, ← mul_assoc, ← mul_assoc, div_mul_cancel₀ _ hv₀.ne', abs_sub_comm, abs_lt, + lt_sub_iff_add_lt, sub_lt_iff_lt_add, mul_assoc] at h have hu₀ : 0 ≤ u - ⌊ξ⌋ * v := by -- Porting note: this abused the definitional equality `-1 + 1 = 0` -- refine' (mul_nonneg_iff_of_pos_right hv₁).mp ((lt_iff_add_one_le (-1 : ℤ) _).mp _) diff --git a/Mathlib/NumberTheory/Liouville/Basic.lean b/Mathlib/NumberTheory/Liouville/Basic.lean index e76ed12616deb9..04403810047a70 100644 --- a/Mathlib/NumberTheory/Liouville/Basic.lean +++ b/Mathlib/NumberTheory/Liouville/Basic.lean @@ -191,11 +191,11 @@ protected theorem transcendental {x : ℝ} (lx : Liouville x) : Transcendental -- recall, this is a proof by contradiction! refine lt_irrefl ((b : ℝ) ^ f.natDegree * |x - ↑a / ↑b|) ?_ -- clear denominators at `a1` - rw [lt_div_iff' (pow_pos b0 _), pow_add, mul_assoc] at a1 + rw [lt_div_iff₀' (pow_pos b0 _), pow_add, mul_assoc] at a1 -- split the inequality via `1 / A`. refine (?_ : (b : ℝ) ^ f.natDegree * |x - a / b| < 1 / A).trans_le ?_ -- This branch of the proof uses the Liouville condition and the Archimedean property - · refine (lt_div_iff' hA).mpr ?_ + · refine (lt_div_iff₀' hA).mpr ?_ refine lt_of_le_of_lt ?_ a1 gcongr refine hn.le.trans ?_ diff --git a/Mathlib/NumberTheory/Liouville/LiouvilleWith.lean b/Mathlib/NumberTheory/Liouville/LiouvilleWith.lean index 45980956c089ef..26c83fc23c3a59 100644 --- a/Mathlib/NumberTheory/Liouville/LiouvilleWith.lean +++ b/Mathlib/NumberTheory/Liouville/LiouvilleWith.lean @@ -53,7 +53,7 @@ theorem liouvilleWith_one (x : ℝ) : LiouvilleWith 1 x := by refine ((eventually_gt_atTop 0).mono fun n hn => ?_).frequently have hn' : (0 : ℝ) < n := by simpa have : x < ↑(⌊x * ↑n⌋ + 1) / ↑n := by - rw [lt_div_iff hn', Int.cast_add, Int.cast_one] + rw [lt_div_iff₀ hn', Int.cast_add, Int.cast_one] exact Int.lt_floor_add_one _ refine ⟨⌊x * n⌋ + 1, this.ne, ?_⟩ rw [abs_sub_comm, abs_of_pos (sub_pos.2 this), rpow_one, sub_lt_iff_lt_add', @@ -100,7 +100,7 @@ theorem frequently_lt_rpow_neg (h : LiouvilleWith p x) (hlt : q < p) : refine (this.and_frequently hC).mono ?_ rintro n ⟨hnC, hn, m, hne, hlt⟩ replace hn : (0 : ℝ) < n := Nat.cast_pos.2 hn - refine ⟨m, hne, hlt.trans <| (div_lt_iff <| rpow_pos_of_pos hn _).2 ?_⟩ + refine ⟨m, hne, hlt.trans <| (div_lt_iff₀ <| rpow_pos_of_pos hn _).2 ?_⟩ rwa [mul_comm, ← rpow_add hn, ← sub_eq_add_neg] /-- The product of a Liouville number and a nonzero rational number is again a Liouville number. -/ diff --git a/Mathlib/NumberTheory/Modular.lean b/Mathlib/NumberTheory/Modular.lean index 812b9760b6b678..0bc6a211e868ab 100644 --- a/Mathlib/NumberTheory/Modular.lean +++ b/Mathlib/NumberTheory/Modular.lean @@ -357,7 +357,7 @@ theorem normSq_S_smul_lt_one (h : 1 < normSq z) : normSq ↑(S • z) < 1 := by theorem im_lt_im_S_smul (h : normSq z < 1) : z.im < (S • z).im := by have : z.im < z.im / normSq (z : ℂ) := by have imz : 0 < z.im := im_pos z - apply (lt_div_iff z.normSq_pos).mpr + apply (lt_div_iff₀ z.normSq_pos).mpr nlinarith convert this simp only [ModularGroup.im_smul_eq_div_normSq] @@ -380,7 +380,7 @@ scoped[Modular] notation "𝒟ᵒ" => ModularGroup.fdo open scoped Modular theorem abs_two_mul_re_lt_one_of_mem_fdo (h : z ∈ 𝒟ᵒ) : |2 * z.re| < 1 := by - rw [abs_mul, abs_two, ← lt_div_iff' (zero_lt_two' ℝ)] + rw [abs_mul, abs_two, ← lt_div_iff₀' (zero_lt_two' ℝ)] exact h.2 theorem three_lt_four_mul_im_sq_of_mem_fdo (h : z ∈ 𝒟ᵒ) : 3 < 4 * z.im ^ 2 := by diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean index f5d474fad9d313..eb0293caf76953 100644 --- a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean +++ b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean @@ -403,7 +403,7 @@ theorem convexBodySum_volume : convert addHaar_smul volume B (convexBodySum K 1) · simp_rw [← Set.preimage_smul_inv₀ (ne_of_gt hB), Set.preimage_setOf_eq, convexBodySumFun, normAtPlace_smul, abs_inv, abs_eq_self.mpr (le_of_lt hB), ← mul_assoc, mul_comm, mul_assoc, - ← Finset.mul_sum, inv_mul_le_iff hB, mul_one] + ← Finset.mul_sum, inv_mul_le_iff₀ hB, mul_one] · rw [abs_pow, ofReal_pow (abs_nonneg _), abs_eq_self.mpr (le_of_lt hB), mixedEmbedding.finrank] · exact this.symm diff --git a/Mathlib/NumberTheory/NumberField/ClassNumber.lean b/Mathlib/NumberTheory/NumberField/ClassNumber.lean index c6726b41347b66..992a53910d4406 100644 --- a/Mathlib/NumberTheory/NumberField/ClassNumber.lean +++ b/Mathlib/NumberTheory/NumberField/ClassNumber.lean @@ -75,7 +75,7 @@ theorem _root_.RingOfIntegers.isPrincipalIdealRing_of_abs_discr_lt ((finrank ℚ K) ^ (finrank ℚ K) / (finrank ℚ K).factorial)) ^ 2) : IsPrincipalIdealRing (𝓞 K) := by have : 0 < finrank ℚ K := finrank_pos -- Lean needs to know that for positivity to succeed - rw [← Real.sqrt_lt (by positivity) (by positivity), mul_assoc, ← inv_mul_lt_iff' (by positivity), + rw [← Real.sqrt_lt (by positivity) (by positivity), mul_assoc, ← inv_mul_lt_iff₀' (by positivity), mul_inv, ← inv_pow, inv_div, inv_div, mul_assoc, Int.cast_abs] at h rw [← classNumber_eq_one_iff, classNumber, Fintype.card_eq_one_iff] refine ⟨1, fun C ↦ ?_⟩ diff --git a/Mathlib/NumberTheory/NumberField/Discriminant.lean b/Mathlib/NumberTheory/NumberField/Discriminant.lean index b93019fd9a8fb6..85e0a1770c6874 100644 --- a/Mathlib/NumberTheory/NumberField/Discriminant.lean +++ b/Mathlib/NumberTheory/NumberField/Discriminant.lean @@ -173,7 +173,7 @@ theorem abs_discr_ge (h : 1 < finrank ℚ K) : rw [← Algebra.coe_norm_int, ← Int.cast_one, ← Int.cast_abs, Rat.cast_intCast, Int.cast_le] exact Int.one_le_abs (Algebra.norm_ne_zero_iff.mpr h_nz) replace h_bd := le_trans h_nm h_bd - rw [← inv_mul_le_iff (by positivity), inv_div, mul_one, Real.le_sqrt (by positivity) + rw [← inv_mul_le_iff₀ (by positivity), inv_div, mul_one, Real.le_sqrt (by positivity) (by positivity), ← Int.cast_abs, div_pow, mul_pow, ← pow_mul, ← pow_mul] at h_bd refine le_trans ?_ h_bd -- The sequence `a n` is a lower bound for `|discr K|`. We prove below by induction an uniform @@ -277,7 +277,7 @@ theorem rank_le_rankOfDiscrBdd : refine fun h ↦ discr_ne_zero K ?_ rwa [h, Nat.cast_zero, abs_nonpos_iff] at hK have h₂ : 1 < 3 * π / 4 := by - rw [_root_.lt_div_iff (by positivity), ← _root_.div_lt_iff' (by positivity), one_mul] + rw [_root_.lt_div_iff₀ (by positivity), ← _root_.div_lt_iff₀' (by positivity), one_mul] linarith [Real.pi_gt_three] obtain h | h := lt_or_le 1 (finrank ℚ K) · apply le_max_of_le_right diff --git a/Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean b/Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean index 2f8a1d3a28cd81..636189cd1f51f7 100644 --- a/Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean +++ b/Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean @@ -304,7 +304,7 @@ theorem exists_unit (w₁ : InfinitePlace K) : _ = w (algebraMap (𝓞 K) K (seq K w₁ hB m)) * w (algebraMap (𝓞 K) K (seq K w₁ hB n))⁻¹ := _root_.map_mul _ _ _ _ < 1 := by - rw [map_inv₀, mul_inv_lt_iff (pos_iff.mpr (seq_ne_zero K w₁ hB n)), mul_one] + rw [map_inv₀, mul_inv_lt_iff₀ (pos_iff.mpr (seq_ne_zero K w₁ hB n)), one_mul] exact seq_decreasing K w₁ hB hnm w hw refine Set.Finite.exists_lt_map_eq_of_forall_mem (t := { I : Ideal (𝓞 K) | 1 ≤ Ideal.absNorm I ∧ Ideal.absNorm I ≤ B }) diff --git a/Mathlib/NumberTheory/Padics/Hensel.lean b/Mathlib/NumberTheory/Padics/Hensel.lean index 2d3a6893edd99c..0de565647f9eef 100644 --- a/Mathlib/NumberTheory/Padics/Hensel.lean +++ b/Mathlib/NumberTheory/Padics/Hensel.lean @@ -401,7 +401,7 @@ private theorem soln_dist_to_a : ‖soln - a‖ = ‖F.eval a‖ / ‖F.derivati tendsto_nhds_unique (newton_seq_dist_tendsto' hnorm) (newton_seq_dist_tendsto hnorm hnsol) private theorem soln_dist_to_a_lt_deriv : ‖soln - a‖ < ‖F.derivative.eval a‖ := by - rw [soln_dist_to_a, div_lt_iff (deriv_norm_pos _), ← sq] <;> assumption + rw [soln_dist_to_a, div_lt_iff₀ (deriv_norm_pos _), ← sq] <;> assumption private theorem soln_unique (z : ℤ_[p]) (hev : F.eval z = 0) (hnlt : ‖z - a‖ < ‖F.derivative.eval a‖) : z = soln := diff --git a/Mathlib/NumberTheory/Rayleigh.lean b/Mathlib/NumberTheory/Rayleigh.lean index d7a2e5f205472b..0e29615583c61a 100644 --- a/Mathlib/NumberTheory/Rayleigh.lean +++ b/Mathlib/NumberTheory/Rayleigh.lean @@ -63,9 +63,9 @@ private theorem no_collision (hrs : r.IsConjExponent s) : Disjoint {beattySeq r k | k} {beattySeq' s k | k} := by rw [Set.disjoint_left] intro j ⟨k, h₁⟩ ⟨m, h₂⟩ - rw [beattySeq, Int.floor_eq_iff, ← div_le_iff₀ hrs.pos, ← lt_div_iff hrs.pos] at h₁ + rw [beattySeq, Int.floor_eq_iff, ← div_le_iff₀ hrs.pos, ← lt_div_iff₀ hrs.pos] at h₁ rw [beattySeq', sub_eq_iff_eq_add, Int.ceil_eq_iff, Int.cast_add, Int.cast_one, - add_sub_cancel_right, ← div_lt_iff hrs.symm.pos, ← le_div_iff₀ hrs.symm.pos] at h₂ + add_sub_cancel_right, ← div_lt_iff₀ hrs.symm.pos, ← le_div_iff₀ hrs.symm.pos] at h₂ have h₃ := add_lt_add_of_le_of_lt h₁.1 h₂.1 have h₄ := add_lt_add_of_lt_of_le h₁.2 h₂.2 simp_rw [div_eq_inv_mul, ← right_distrib, hrs.inv_add_inv_conj, one_mul] at h₃ h₄ @@ -91,10 +91,10 @@ private theorem hit_or_miss (h : r > 0) : -- for both cases, the candidate is `k = ⌈(j + 1) / r⌉ - 1` cases lt_or_ge ((⌈(j + 1) / r⌉ - 1) * r) j · refine Or.inr ⟨⌈(j + 1) / r⌉ - 1, ?_⟩ - rw [Int.cast_sub, Int.cast_one, lt_div_iff h, sub_add_cancel] + rw [Int.cast_sub, Int.cast_one, lt_div_iff₀ h, sub_add_cancel] exact ⟨‹_›, Int.le_ceil _⟩ · refine Or.inl ⟨⌈(j + 1) / r⌉ - 1, ?_⟩ - rw [beattySeq, Int.floor_eq_iff, Int.cast_sub, Int.cast_one, ← lt_div_iff h, sub_lt_iff_lt_add] + rw [beattySeq, Int.floor_eq_iff, Int.cast_sub, Int.cast_one, ← lt_div_iff₀ h, sub_lt_iff_lt_add] exact ⟨‹_›, Int.ceil_lt_add_one _⟩ /-- Let `0 < r ∈ ℝ` and `j ∈ ℤ`. Then either `j ∈ B'_r` or `B'_r` jumps over `j`. -/ diff --git a/Mathlib/RingTheory/RootsOfUnity/Complex.lean b/Mathlib/RingTheory/RootsOfUnity/Complex.lean index ec561559512820..a11bd30bfad0a3 100644 --- a/Mathlib/RingTheory/RootsOfUnity/Complex.lean +++ b/Mathlib/RingTheory/RootsOfUnity/Complex.lean @@ -168,7 +168,7 @@ theorem IsPrimitiveRoot.arg {n : ℕ} {ζ : ℂ} (h : IsPrimitiveRoot ζ n) (hn exact mul_nonpos_of_nonpos_of_nonneg (sub_nonpos.mpr <| mod_cast h.le) (div_nonneg (by simp [Real.pi_pos.le]) <| by simp) rw [← mul_rotate', mul_div_assoc, neg_lt, ← mul_neg, mul_lt_iff_lt_one_right Real.pi_pos, ← - neg_div, ← neg_mul, neg_sub, div_lt_iff, one_mul, sub_mul, sub_lt_comm, ← mul_sub_one] + neg_div, ← neg_mul, neg_sub, div_lt_iff₀, one_mul, sub_mul, sub_lt_comm, ← mul_sub_one] · norm_num exact mod_cast not_le.mp h₂ · exact Nat.cast_pos.mpr hn.bot_lt diff --git a/Mathlib/Topology/Algebra/Module/FiniteDimension.lean b/Mathlib/Topology/Algebra/Module/FiniteDimension.lean index 04cdc12e8032bc..31b45d485cdb94 100644 --- a/Mathlib/Topology/Algebra/Module/FiniteDimension.lean +++ b/Mathlib/Topology/Algebra/Module/FiniteDimension.lean @@ -106,7 +106,7 @@ theorem unique_topology_of_t2 {t : TopologicalSpace 𝕜} (h₁ : @TopologicalAd -- For that, we use that `𝓑` is balanced : since `‖ξ₀‖ < ε < ‖ξ‖`, we have `‖ξ₀ / ξ‖ ≤ 1`, -- hence `ξ₀ = (ξ₀ / ξ) • ξ ∈ 𝓑` because `ξ ∈ 𝓑`. refine (balancedCore_balanced _).smul_mem ?_ hξ - rw [norm_mul, norm_inv, mul_inv_le_iff (norm_pos_iff.mpr hξ0), mul_one] + rw [norm_mul, norm_inv, mul_inv_le_iff₀ (norm_pos_iff.mpr hξ0), one_mul] exact (hξ₀ε.trans h).le · -- Finally, to show `𝓣₀ ≤ 𝓣`, we simply argue that `id = (fun x ↦ x • 1)` is continuous from -- `(𝕜, 𝓣₀)` to `(𝕜, 𝓣)` because `(•) : (𝕜, 𝓣₀) × (𝕜, 𝓣) → (𝕜, 𝓣)` is continuous. diff --git a/Mathlib/Topology/Algebra/PontryaginDual.lean b/Mathlib/Topology/Algebra/PontryaginDual.lean index f34d6b2a026ac7..fe184b35a5fa5c 100644 --- a/Mathlib/Topology/Algebra/PontryaginDual.lean +++ b/Mathlib/Topology/Algebra/PontryaginDual.lean @@ -60,9 +60,9 @@ instance [LocallyCompactSpace G] : LocallyCompactSpace (PontryaginDual G) := by · intro n x h1 h2 rw [hVn] at h1 h2 ⊢ rwa [Circle.coe_mul, Complex.arg_mul x.coe_ne_zero x.coe_ne_zero, - ← two_mul, abs_mul, abs_two, ← lt_div_iff' two_pos, div_div, ← pow_succ] at h2 + ← two_mul, abs_mul, abs_two, ← lt_div_iff₀' two_pos, div_div, ← pow_succ] at h2 apply Set.Ioo_subset_Ioc_self - rw [← two_mul, Set.mem_Ioo, ← abs_lt, abs_mul, abs_two, ← lt_div_iff' two_pos] + rw [← two_mul, Set.mem_Ioo, ← abs_lt, abs_mul, abs_two, ← lt_div_iff₀' two_pos] exact h1.trans_le (div_le_div_of_nonneg_left Real.pi_nonneg two_pos (le_self_pow one_le_two n.succ_ne_zero)) · rw [← Circle.exp_zero, ← isLocalHomeomorph_circleExp.map_nhds_eq 0] diff --git a/Mathlib/Topology/ContinuousMap/Ideals.lean b/Mathlib/Topology/ContinuousMap/Ideals.lean index ead82fefc127ce..5edb4350d52746 100644 --- a/Mathlib/Topology/ContinuousMap/Ideals.lean +++ b/Mathlib/Topology/ContinuousMap/Ideals.lean @@ -169,7 +169,7 @@ theorem exists_mul_le_one_eqOn_ge (f : C(X, ℝ≥0)) {c : ℝ≥0} (hc : 0 < c) continuous_toFun := ((map_continuous f).sup <| map_continuous _).inv₀ fun _ => (hc.trans_le le_sup_right).ne' }, fun x => - (inv_mul_le_iff (hc.trans_le le_sup_right)).mpr ((mul_one (f x ⊔ c)).symm ▸ le_sup_left), + (inv_mul_le_iff₀ (hc.trans_le le_sup_right)).mpr ((mul_one (f x ⊔ c)).symm ▸ le_sup_left), fun x hx => by simpa only [coe_const, mul_apply, coe_mk, Pi.inv_apply, Pi.sup_apply, Function.const_apply, sup_eq_left.mpr (Set.mem_setOf.mp hx), ne_eq, Pi.one_apply]