case tfae_1_to_2
α : Type u_1
β : Type ?u.5660
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
n : ℕ
⊢ ↑n ≤ chainHeight s → ∃ l, l ∈ subchain s ∧ length l = n

α : Type u_1
β : Type ?u.5660
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
n : ℕ
tfae_1_to_2 : ↑n ≤ chainHeight s → ∃ l, l ∈ subchain s ∧ length l = n
⊢ TFAE [↑n ≤ chainHeight s, ∃ l, l ∈ subchain s ∧ length l = n, ∃ l, l ∈ subchain s ∧ n ≤ length l]
α : Type u_1
β : Type ?u.5660
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
n : ℕ
⊢ TFAE [↑n ≤ chainHeight s, ∃ l, l ∈ subchain s ∧ length l = n, ∃ l, l ∈ subchain s ∧ n ≤ length l]
tfae_have 1 → 2
case tfae_2_to_3
α : Type u_1
β : Type ?u.5660
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
n : ℕ
tfae_1_to_2 : ↑n ≤ chainHeight s → ∃ l, l ∈ subchain s ∧ length l = n
⊢ (∃ l, l ∈ subchain s ∧ length l = n) → ∃ l, l ∈ subchain s ∧ n ≤ length l

α : Type u_1
β : Type ?u.5660
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
n : ℕ
tfae_1_to_2 : ↑n ≤ chainHeight s → ∃ l, l ∈ subchain s ∧ length l = n
tfae_2_to_3 : (∃ l, l ∈ subchain s ∧ length l = n) → ∃ l, l ∈ subchain s ∧ n ≤ length l
⊢ TFAE [↑n ≤ chainHeight s, ∃ l, l ∈ subchain s ∧ length l = n, ∃ l, l ∈ subchain s ∧ n ≤ length l]
α : Type u_1
β : Type ?u.5660
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
n : ℕ
tfae_1_to_2 : ↑n ≤ chainHeight s → ∃ l, l ∈ subchain s ∧ length l = n
⊢ TFAE [↑n ≤ chainHeight s, ∃ l, l ∈ subchain s ∧ length l = n, ∃ l, l ∈ subchain s ∧ n ≤ length l]
tfae_have 2 → 3
case tfae_3_to_1
α : Type u_1
β : Type ?u.5660
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
n : ℕ
tfae_1_to_2 : ↑n ≤ chainHeight s → ∃ l, l ∈ subchain s ∧ length l = n
tfae_2_to_3 : (∃ l, l ∈ subchain s ∧ length l = n) → ∃ l, l ∈ subchain s ∧ n ≤ length l
⊢ (∃ l, l ∈ subchain s ∧ n ≤ length l) → ↑n ≤ chainHeight s

α : Type u_1
β : Type ?u.5660
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
n : ℕ
tfae_1_to_2 : ↑n ≤ chainHeight s → ∃ l, l ∈ subchain s ∧ length l = n
tfae_2_to_3 : (∃ l, l ∈ subchain s ∧ length l = n) → ∃ l, l ∈ subchain s ∧ n ≤ length l
tfae_3_to_1 : (∃ l, l ∈ subchain s ∧ n ≤ length l) → ↑n ≤ chainHeight s
⊢ TFAE [↑n ≤ chainHeight s, ∃ l, l ∈ subchain s ∧ length l = n, ∃ l, l ∈ subchain s ∧ n ≤ length l]
α : Type u_1
β : Type ?u.5660
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
n : ℕ
tfae_1_to_2 : ↑n ≤ chainHeight s → ∃ l, l ∈ subchain s ∧ length l = n
tfae_2_to_3 : (∃ l, l ∈ subchain s ∧ length l = n) → ∃ l, l ∈ subchain s ∧ n ≤ length l
⊢ TFAE [↑n ≤ chainHeight s, ∃ l, l ∈ subchain s ∧ length l = n, ∃ l, l ∈ subchain s ∧ n ≤ length l]
tfae_have 3 → 1
no goals
α : Type u_1
β : Type ?u.5660
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
n : ℕ
tfae_1_to_2 : ↑n ≤ chainHeight s → ∃ l, l ∈ subchain s ∧ length l = n
tfae_2_to_3 : (∃ l, l ∈ subchain s ∧ length l = n) → ∃ l, l ∈ subchain s ∧ n ≤ length l
tfae_3_to_1 : (∃ l, l ∈ subchain s ∧ n ≤ length l) → ↑n ≤ chainHeight s
⊢ TFAE [↑n ≤ chainHeight s, ∃ l, l ∈ subchain s ∧ length l = n, ∃ l, l ∈ subchain s ∧ n ≤ length l]
tfae_finish
no goals
case tfae_1_to_2
α : Type u_1
β : Type ?u.5660
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
n : ℕ
⊢ ↑n ≤ chainHeight s → ∃ l, l ∈ subchain s ∧ length l = n
exact s.exists_chain_of_le_chainHeight
case tfae_2_to_3.intro.intro
α : Type u_1
β : Type ?u.5660
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l✝ : List α
a : α
n : ℕ
tfae_1_to_2 : ↑n ≤ chainHeight s → ∃ l, l ∈ subchain s ∧ length l = n
l : List α
hls : l ∈ subchain s
he : length l = n
⊢ ∃ l, l ∈ subchain s ∧ n ≤ length l
case tfae_2_to_3
α : Type u_1
β : Type ?u.5660
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
n : ℕ
tfae_1_to_2 : ↑n ≤ chainHeight s → ∃ l, l ∈ subchain s ∧ length l = n
⊢ (∃ l, l ∈ subchain s ∧ length l = n) → ∃ l, l ∈ subchain s ∧ n ≤ length l
rintro ⟨l, hls, he⟩
no goals
case tfae_2_to_3.intro.intro
α : Type u_1
β : Type ?u.5660
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l✝ : List α
a : α
n : ℕ
tfae_1_to_2 : ↑n ≤ chainHeight s → ∃ l, l ∈ subchain s ∧ length l = n
l : List α
hls : l ∈ subchain s
he : length l = n
⊢ ∃ l, l ∈ subchain s ∧ n ≤ length l
exact ⟨l, hls, he.ge⟩
case tfae_3_to_1.intro.intro
α : Type u_1
β : Type ?u.5660
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l✝ : List α
a : α
n : ℕ
tfae_1_to_2 : ↑n ≤ chainHeight s → ∃ l, l ∈ subchain s ∧ length l = n
tfae_2_to_3 : (∃ l, l ∈ subchain s ∧ length l = n) → ∃ l, l ∈ subchain s ∧ n ≤ length l
l : List α
hs : l ∈ subchain s
hn : n ≤ length l
⊢ ↑n ≤ chainHeight s
case tfae_3_to_1
α : Type u_1
β : Type ?u.5660
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
n : ℕ
tfae_1_to_2 : ↑n ≤ chainHeight s → ∃ l, l ∈ subchain s ∧ length l = n
tfae_2_to_3 : (∃ l, l ∈ subchain s ∧ length l = n) → ∃ l, l ∈ subchain s ∧ n ≤ length l
⊢ (∃ l, l ∈ subchain s ∧ n ≤ length l) → ↑n ≤ chainHeight s
rintro ⟨l, hs, hn⟩
no goals
case tfae_3_to_1.intro.intro
α : Type u_1
β : Type ?u.5660
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l✝ : List α
a : α
n : ℕ
tfae_1_to_2 : ↑n ≤ chainHeight s → ∃ l, l ∈ subchain s ∧ length l = n
tfae_2_to_3 : (∃ l, l ∈ subchain s ∧ length l = n) → ∃ l, l ∈ subchain s ∧ n ≤ length l
l : List α
hs : l ∈ subchain s
hn : n ≤ length l
⊢ ↑n ≤ chainHeight s
exact le_iSup₂_of_le l hs (WithTop.coe_le_coe.2 hn)