Skip to content

Commit

Permalink
chore: Move pow_lt_pow_succ to Algebra.Order.WithZero (#11507)
Browse files Browse the repository at this point in the history
These lemmas can be defined earlier, ridding us of an import in `Algebra.GroupPower.Order`
  • Loading branch information
YaelDillies committed Mar 19, 2024
1 parent aa398a0 commit 82c89cd
Show file tree
Hide file tree
Showing 6 changed files with 35 additions and 48 deletions.
27 changes: 0 additions & 27 deletions Mathlib/Algebra/GroupPower/Order.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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"

Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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
1 change: 1 addition & 0 deletions Mathlib/Algebra/Order/Field/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Algebra/Order/Floor.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down
29 changes: 22 additions & 7 deletions Mathlib/Algebra/Order/WithZero.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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 α] :
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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. -/
Expand Down Expand Up @@ -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₀
16 changes: 8 additions & 8 deletions Mathlib/Data/Ordmap/Ordset.lean
Original file line number Diff line number Diff line change
Expand Up @@ -681,15 +681,15 @@ 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
rw [if_neg, if_pos, rotateL, if_pos]; · rfl
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
Expand All @@ -708,15 +708,15 @@ 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
rw [if_neg, if_neg, if_pos, rotateR, if_neg]; · rfl
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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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₁
Expand Down Expand Up @@ -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 _
Expand Down
8 changes: 3 additions & 5 deletions Mathlib/Order/RelSeries.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 82c89cd

Please sign in to comment.