α : Type u_1
inst✝ : CompleteLattice α
h : WellFounded fun x x_1 => x > x_1
a : ℕ →o α
m : ℕ
⊢ ↑a m ≤ monotonicSequenceLimit a
α : Type u_1
inst✝ : CompleteLattice α
h : WellFounded fun x x_1 => x > x_1
a : ℕ →o α
⊢ iSup ↑a = monotonicSequenceLimit a
refine' (iSup_le fun m => _).antisymm (le_iSup a _)
case inl
α : Type u_1
inst✝ : CompleteLattice α
h : WellFounded fun x x_1 => x > x_1
a : ℕ →o α
m : ℕ
hm : m ≤ monotonicSequenceLimitIndex a
⊢ ↑a m ≤ monotonicSequenceLimit a

case inr
α : Type u_1
inst✝ : CompleteLattice α
h : WellFounded fun x x_1 => x > x_1
a : ℕ →o α
m : ℕ
hm : monotonicSequenceLimitIndex a < m
⊢ ↑a m ≤ monotonicSequenceLimit a
α : Type u_1
inst✝ : CompleteLattice α
h : WellFounded fun x x_1 => x > x_1
a : ℕ →o α
m : ℕ
⊢ ↑a m ≤ monotonicSequenceLimit a
cases' le_or_lt m (monotonicSequenceLimitIndex a) with hm hm
no goals
case inl
α : Type u_1
inst✝ : CompleteLattice α
h : WellFounded fun x x_1 => x > x_1
a : ℕ →o α
m : ℕ
hm : m ≤ monotonicSequenceLimitIndex a
⊢ ↑a m ≤ monotonicSequenceLimit a
exact a.monotone hm
case inr.intro
α : Type u_1
inst✝ : CompleteLattice α
h : WellFounded fun x x_1 => x > x_1
a : ℕ →o α
m : ℕ
hm : monotonicSequenceLimitIndex a < m
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → ¬↑a n < ↑a m
⊢ ↑a m ≤ monotonicSequenceLimit a
case inr
α : Type u_1
inst✝ : CompleteLattice α
h : WellFounded fun x x_1 => x > x_1
a : ℕ →o α
m : ℕ
hm : monotonicSequenceLimitIndex a < m
⊢ ↑a m ≤ monotonicSequenceLimit a
cases' WellFounded.monotone_chain_condition'.1 h a with n hn
case inr.intro
α : Type u_1
inst✝ : CompleteLattice α
h : WellFounded fun x x_1 => x > x_1
a : ℕ →o α
m : ℕ
hm : monotonicSequenceLimitIndex a < m
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → ¬↑a n < ↑a m
this : n ∈ {n | ∀ (m : ℕ), n ≤ m → ↑a n = ↑a m}
⊢ ↑a m ≤ monotonicSequenceLimit a
case inr.intro
α : Type u_1
inst✝ : CompleteLattice α
h : WellFounded fun x x_1 => x > x_1
a : ℕ →o α
m : ℕ
hm : monotonicSequenceLimitIndex a < m
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → ¬↑a n < ↑a m
⊢ ↑a m ≤ monotonicSequenceLimit a
have : n ∈ {n | ∀ m, n ≤ m → a n = a m} := fun k hk => (a.mono hk).eq_of_not_lt (hn k hk)
no goals
case inr.intro
α : Type u_1
inst✝ : CompleteLattice α
h : WellFounded fun x x_1 => x > x_1
a : ℕ →o α
m : ℕ
hm : monotonicSequenceLimitIndex a < m
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → ¬↑a n < ↑a m
this : n ∈ {n | ∀ (m : ℕ), n ≤ m → ↑a n = ↑a m}
⊢ ↑a m ≤ monotonicSequenceLimit a
exact (Nat.sInf_mem ⟨n, this⟩ m hm.le).ge