diff --git a/Mathlib/Algebra/GroupPower/Order.lean b/Mathlib/Algebra/GroupPower/Order.lean index eede6d323e187d..50bb6b8c521179 100644 --- a/Mathlib/Algebra/GroupPower/Order.lean +++ b/Mathlib/Algebra/GroupPower/Order.lean @@ -5,7 +5,6 @@ Authors: Jeremy Avigad, Robert Y. Lewis -/ import Mathlib.Algebra.GroupPower.CovariantClass import Mathlib.Algebra.GroupPower.Ring -import Mathlib.Algebra.Order.WithZero #align_import algebra.group_power.order from "leanprover-community/mathlib"@"00f91228655eecdcd3ac97a7fd8dbcb139fe990a" @@ -508,31 +507,6 @@ lemma pow_four_le_pow_two_of_pow_two_le (h : a ^ 2 ≤ b) : a ^ 4 ≤ b ^ 2 := end LinearOrderedRing -section LinearOrderedCommMonoidWithZero - -variable [LinearOrderedCommMonoidWithZero M] [NoZeroDivisors M] {a : M} {n : ℕ} - -theorem pow_pos_iff (hn : n ≠ 0) : 0 < a ^ n ↔ 0 < a := by simp_rw [zero_lt_iff, pow_ne_zero_iff hn] -#align pow_pos_iff pow_pos_iff - -end LinearOrderedCommMonoidWithZero - -section LinearOrderedCommGroupWithZero - -variable [LinearOrderedCommGroupWithZero M] {a : M} {m n : ℕ} - -theorem pow_lt_pow_succ (ha : 1 < a) : a ^ n < a ^ n.succ := by - rw [← one_mul (a ^ n), pow_succ] - exact mul_lt_right₀ _ ha (pow_ne_zero _ (zero_lt_one.trans ha).ne') -#align pow_lt_pow_succ pow_lt_pow_succ - -theorem pow_lt_pow_right₀ (ha : 1 < a) (hmn : m < n) : a ^ m < a ^ n := by - induction' hmn with n _ ih - exacts [pow_lt_pow_succ ha, lt_trans ih (pow_lt_pow_succ ha)] -#align pow_lt_pow₀ pow_lt_pow_right₀ - -end LinearOrderedCommGroupWithZero - namespace MonoidHom variable [Ring R] [Monoid M] [LinearOrder M] [CovariantClass M M (· * ·) (· ≤ ·)] (f : R →* M) @@ -571,5 +545,4 @@ Those lemmas have been deprecated on 2023-12-23. @[deprecated] alias pow_lt_pow_of_lt_one := pow_lt_pow_right_of_lt_one @[deprecated] alias lt_of_pow_lt_pow := lt_of_pow_lt_pow_left @[deprecated] alias le_of_pow_le_pow := le_of_pow_le_pow_left -@[deprecated] alias pow_lt_pow₀ := pow_lt_pow_right₀ @[deprecated] alias self_le_pow := le_self_pow diff --git a/Mathlib/Algebra/Order/Field/Basic.lean b/Mathlib/Algebra/Order/Field/Basic.lean index 8460526d8a74c9..3736dea3ef40dd 100644 --- a/Mathlib/Algebra/Order/Field/Basic.lean +++ b/Mathlib/Algebra/Order/Field/Basic.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Robert Lewis, Leonardo de Moura, Mario Carneiro, Floris van Doorn -/ import Mathlib.Algebra.Field.Basic +import Mathlib.Algebra.GroupWithZero.Units.Equiv import Mathlib.Algebra.Order.Field.Defs import Mathlib.Algebra.Order.Ring.Abs import Mathlib.Order.Bounds.OrderIso diff --git a/Mathlib/Algebra/Order/Floor.lean b/Mathlib/Algebra/Order/Floor.lean index 2d20ecb9e691bf..58a6dcdc91badf 100644 --- a/Mathlib/Algebra/Order/Floor.lean +++ b/Mathlib/Algebra/Order/Floor.lean @@ -334,7 +334,7 @@ theorem ceil_one : ⌈(1 : α)⌉₊ = 1 := by rw [← Nat.cast_one, ceil_natCas #align nat.ceil_one Nat.ceil_one @[simp] -theorem ceil_eq_zero : ⌈a⌉₊ = 0 ↔ a ≤ 0 := by rw [← le_zero_iff, ceil_le, Nat.cast_zero] +theorem ceil_eq_zero : ⌈a⌉₊ = 0 ↔ a ≤ 0 := by rw [← Nat.le_zero, ceil_le, Nat.cast_zero] #align nat.ceil_eq_zero Nat.ceil_eq_zero @[simp] diff --git a/Mathlib/Algebra/Order/WithZero.lean b/Mathlib/Algebra/Order/WithZero.lean index 3b27e0f310fc24..7e238d962e5c42 100644 --- a/Mathlib/Algebra/Order/WithZero.lean +++ b/Mathlib/Algebra/Order/WithZero.lean @@ -36,8 +36,7 @@ class LinearOrderedCommGroupWithZero (α : Type*) extends LinearOrderedCommMonoi CommGroupWithZero α #align linear_ordered_comm_group_with_zero LinearOrderedCommGroupWithZero -variable {α : Type*} -variable {a b c d x y z : α} +variable {α : Type*} {a b c d x y z : α} instance instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual [LinearOrderedAddCommMonoidWithTop α] : @@ -67,9 +66,8 @@ instance instLinearOrderedCommMonoidWithZeroWithZero [LinearOrderedCommMonoid α instance [LinearOrderedCommGroup α] : LinearOrderedCommGroupWithZero (WithZero α) := { instLinearOrderedCommMonoidWithZeroWithZero, WithZero.commGroupWithZero with } -section LinearOrderedCommMonoid - -variable [LinearOrderedCommMonoidWithZero α] +section LinearOrderedCommMonoidWithZero +variable [LinearOrderedCommMonoidWithZero α] {n : ℕ} /- The following facts are true more generally in a (linearly) ordered commutative monoid. @@ -117,9 +115,14 @@ instance instLinearOrderedAddCommMonoidWithTopAdditiveOrderDual : le_top := fun _ ↦ zero_le' } #align additive.linear_ordered_add_comm_monoid_with_top instLinearOrderedAddCommMonoidWithTopAdditiveOrderDual -end LinearOrderedCommMonoid +variable [NoZeroDivisors α] + +lemma pow_pos_iff (hn : n ≠ 0) : 0 < a ^ n ↔ 0 < a := by simp_rw [zero_lt_iff, pow_ne_zero_iff hn] +#align pow_pos_iff pow_pos_iff + +end LinearOrderedCommMonoidWithZero -variable [LinearOrderedCommGroupWithZero α] +variable [LinearOrderedCommGroupWithZero α] {m n : ℕ} -- TODO: Do we really need the following two? /-- Alias of `mul_le_one'` for unification. -/ @@ -285,3 +288,15 @@ instance : LinearOrderedAddCommGroupWithTop (Additive αᵒᵈ) := Additive.instNontrivial with neg_top := @inv_zero _ (_) add_neg_cancel := fun a ha ↦ mul_inv_cancel (G₀ := α) (id ha : Additive.toMul a ≠ 0) } + +lemma pow_lt_pow_succ (ha : 1 < a) : a ^ n < a ^ n.succ := by + rw [← one_mul (a ^ n), pow_succ]; + exact mul_lt_right₀ _ ha (pow_ne_zero _ (zero_lt_one.trans ha).ne') +#align pow_lt_pow_succ pow_lt_pow_succ + +lemma pow_lt_pow_right₀ (ha : 1 < a) (hmn : m < n) : a ^ m < a ^ n := by + induction' hmn with n _ ih; exacts [pow_lt_pow_succ ha, lt_trans ih (pow_lt_pow_succ ha)] +#align pow_lt_pow₀ pow_lt_pow_right₀ + +-- 2023-12-23 +@[deprecated] alias pow_lt_pow₀ := pow_lt_pow_right₀ diff --git a/Mathlib/Data/Ordmap/Ordset.lean b/Mathlib/Data/Ordmap/Ordset.lean index 2f1c6fbadc75c2..69f6983163c810 100644 --- a/Mathlib/Data/Ordmap/Ordset.lean +++ b/Mathlib/Data/Ordmap/Ordset.lean @@ -681,7 +681,7 @@ theorem balance_eq_balance' {l x r} (hl : Balanced l) (hr : Balanced r) (sl : Si · rfl · have : size rrl = 0 ∧ size rrr = 0 := by have := balancedSz_zero.1 hr.1.symm - rwa [size, sr.2.2.1, Nat.succ_le_succ_iff, le_zero_iff, add_eq_zero_iff] at this + rwa [size, sr.2.2.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero_iff] at this cases sr.2.2.2.1.size_eq_zero.1 this.1 cases sr.2.2.2.2.size_eq_zero.1 this.2 obtain rfl : rrs = 1 := sr.2.2.1 @@ -689,7 +689,7 @@ theorem balance_eq_balance' {l x r} (hl : Balanced l) (hr : Balanced r) (sl : Si all_goals dsimp only [size]; decide · have : size rll = 0 ∧ size rlr = 0 := by have := balancedSz_zero.1 hr.1 - rwa [size, sr.2.1.1, Nat.succ_le_succ_iff, le_zero_iff, add_eq_zero_iff] at this + rwa [size, sr.2.1.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero_iff] at this cases sr.2.1.2.1.size_eq_zero.1 this.1 cases sr.2.1.2.2.size_eq_zero.1 this.2 obtain rfl : rls = 1 := sr.2.1.1 @@ -708,7 +708,7 @@ theorem balance_eq_balance' {l x r} (hl : Balanced l) (hr : Balanced r) (sl : Si · rfl · have : size lrl = 0 ∧ size lrr = 0 := by have := balancedSz_zero.1 hl.1.symm - rwa [size, sl.2.2.1, Nat.succ_le_succ_iff, le_zero_iff, add_eq_zero_iff] at this + rwa [size, sl.2.2.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero_iff] at this cases sl.2.2.2.1.size_eq_zero.1 this.1 cases sl.2.2.2.2.size_eq_zero.1 this.2 obtain rfl : lrs = 1 := sl.2.2.1 @@ -716,7 +716,7 @@ theorem balance_eq_balance' {l x r} (hl : Balanced l) (hr : Balanced r) (sl : Si all_goals dsimp only [size]; decide · have : size lll = 0 ∧ size llr = 0 := by have := balancedSz_zero.1 hl.1 - rwa [size, sl.2.1.1, Nat.succ_le_succ_iff, le_zero_iff, add_eq_zero_iff] at this + rwa [size, sl.2.1.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero_iff] at this cases sl.2.1.2.1.size_eq_zero.1 this.1 cases sl.2.1.2.2.size_eq_zero.1 this.2 obtain rfl : lls = 1 := sl.2.1.1 @@ -766,7 +766,7 @@ theorem balanceL_eq_balance {l x r} (sl : Sized l) (sr : Sized r) (H1 : size l = · cases' l with ls ll lx lr · have : size rl = 0 ∧ size rr = 0 := by have := H1 rfl - rwa [size, sr.1, Nat.succ_le_succ_iff, le_zero_iff, add_eq_zero_iff] at this + rwa [size, sr.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero_iff] at this cases sr.2.1.size_eq_zero.1 this.1 cases sr.2.2.size_eq_zero.1 this.2 rw [sr.eq_node']; rfl @@ -1196,7 +1196,7 @@ theorem Valid'.node4L {l} {x : α} {m} {y : α} {r o₁ o₂} (hl : Valid' o₁ · rw [Nat.succ_add] at mm; rcases mm with (_ | ⟨⟨⟩⟩) rcases hm.3.1.resolve_left mm with ⟨mm₁, mm₂⟩ rcases Nat.eq_zero_or_pos (size ml) with ml0 | ml0 - · rw [ml0, mul_zero, le_zero_iff] at mm₂ + · rw [ml0, mul_zero, Nat.le_zero] at mm₂ rw [ml0, mm₂] at mm; cases mm (by decide) have : 2 * size l ≤ size ml + size mr + 1 := by have := Nat.mul_le_mul_left ratio lr₁ @@ -1275,9 +1275,9 @@ theorem Valid'.rotateL {l} {x : α} {r o₁ o₂} (hl : Valid' o₁ l x) (hr : V le_trans hb₂ (Nat.mul_le_mul_left _ <| le_trans (Nat.le_add_left _ _) (Nat.le_add_right _ _)) · rcases Nat.eq_zero_or_pos (size rl) with rl0 | rl0 - · rw [rl0, not_lt, le_zero_iff, Nat.mul_eq_zero] at h + · rw [rl0, not_lt, Nat.le_zero, Nat.mul_eq_zero] at h replace h := h.resolve_left (by decide) - erw [rl0, h, le_zero_iff, Nat.mul_eq_zero] at H2 + erw [rl0, h, Nat.le_zero, Nat.mul_eq_zero] at H2 rw [hr.2.size_eq, rl0, h, H2.resolve_left (by decide)] at H1 cases H1 (by decide) refine' hl.node4L hr.left hr.right rl0 _ diff --git a/Mathlib/Order/RelSeries.lean b/Mathlib/Order/RelSeries.lean index 36e083be847e41..3b3fb63aefe89d 100644 --- a/Mathlib/Order/RelSeries.lean +++ b/Mathlib/Order/RelSeries.lean @@ -453,11 +453,9 @@ lemma smash_succ_castAdd {p q : RelSeries r} (h : p.last = q.head) lemma smash_natAdd {p q : RelSeries r} (h : p.last = q.head) (i : Fin q.length) : smash p q h (Fin.castSucc <| i.natAdd p.length) = q (Fin.castSucc i) := by - rw [smash_toFun] - split_ifs with H - · simp only [Fin.coe_castSucc, Fin.coe_natAdd, add_lt_iff_neg_left, not_lt_zero'] at H - · congr - exact Nat.add_sub_self_left _ _ + rw [smash_toFun, dif_neg (by simp)] + congr + exact Nat.add_sub_self_left _ _ lemma smash_succ_natAdd {p q : RelSeries r} (h : p.last = q.head) (i : Fin q.length) : smash p q h (i.natAdd p.length).succ = q i.succ := by