case inl
α : Type u_1
β : Type ?u.3758
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
n : ℕ
hn : ↑n ≤ chainHeight s
ha : (⨆ (l : ↑(subchain s)), ↑(length ↑l)) = ⊤
⊢ ∃ l, l ∈ subchain s ∧ length l = n

case inr
α : Type u_1
β : Type ?u.3758
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
n : ℕ
hn : ↑n ≤ chainHeight s
ha : (⨆ (l : ↑(subchain s)), ↑(length ↑l)) < ⊤
⊢ ∃ l, l ∈ subchain s ∧ length l = n
α : Type u_1
β : Type ?u.3758
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
n : ℕ
hn : ↑n ≤ chainHeight s
⊢ ∃ l, l ∈ subchain s ∧ length l = n
cases' (le_top : s.chainHeight ≤ ⊤).eq_or_lt with ha ha <;>
  rw [chainHeight_eq_iSup_subtype] at ha
case inl.intro.intro.intro.mk.intro
α : Type u_1
β : Type ?u.3758
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l✝ : List α
a : α
n : ℕ
hn : ↑n ≤ chainHeight s
ha : (⨆ (l : ↑(subchain s)), ↑(length ↑l)) = ⊤
l : List α
h₁ : Chain' (fun x x_1 => x < x_1) l
h₂ : ∀ (i : α), i ∈ l → i ∈ s
h₃ :
  ¬(fun x => ↑(length ↑x)) { val := l, property := (_ : Chain' (fun x x_1 => x < x_1) l ∧ ∀ (i : α), i ∈ l → i ∈ s) } ≤
      n
⊢ ∃ l, l ∈ subchain s ∧ length l = n
case inl
α : Type u_1
β : Type ?u.3758
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
n : ℕ
hn : ↑n ≤ chainHeight s
ha : (⨆ (l : ↑(subchain s)), ↑(length ↑l)) = ⊤
⊢ ∃ l, l ∈ subchain s ∧ length l = n
obtain ⟨_, ⟨⟨l, h₁, h₂⟩, rfl⟩, h₃⟩ :=
  not_bddAbove_iff'.mp ((WithTop.iSup_coe_eq_top _).mp ha) n
no goals
case inl.intro.intro.intro.mk.intro
α : Type u_1
β : Type ?u.3758
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l✝ : List α
a : α
n : ℕ
hn : ↑n ≤ chainHeight s
ha : (⨆ (l : ↑(subchain s)), ↑(length ↑l)) = ⊤
l : List α
h₁ : Chain' (fun x x_1 => x < x_1) l
h₂ : ∀ (i : α), i ∈ l → i ∈ s
h₃ :
  ¬(fun x => ↑(length ↑x)) { val := l, property := (_ : Chain' (fun x x_1 => x < x_1) l ∧ ∀ (i : α), i ∈ l → i ∈ s) } ≤
      n
⊢ ∃ l, l ∈ subchain s ∧ length l = n
exact ⟨l.take n, ⟨h₁.take _, fun x h ↦ h₂ _ <| take_subset _ _ h⟩,
  (l.length_take n).trans <| min_eq_left <| le_of_not_ge h₃⟩
case inr
α : Type u_1
β : Type ?u.3758
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
n : ℕ
hn : ↑n ≤ chainHeight s
ha : BddAbove (range fun l => length ↑l)
⊢ ∃ l, l ∈ subchain s ∧ length l = n
case inr
α : Type u_1
β : Type ?u.3758
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
n : ℕ
hn : ↑n ≤ chainHeight s
ha : (⨆ (l : ↑(subchain s)), ↑(length ↑l)) < ⊤
⊢ ∃ l, l ∈ subchain s ∧ length l = n
rw [ENat.iSup_coe_lt_top] at ha
case inr.intro.mk.intro
α : Type u_1
β : Type ?u.3758
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l✝ : List α
a : α
n : ℕ
hn : ↑n ≤ chainHeight s
ha : BddAbove (range fun l => length ↑l)
l : List α
h₁ : Chain' (fun x x_1 => x < x_1) l
h₂ : ∀ (i : α), i ∈ l → i ∈ s
e : length l = sSup (range fun l => length ↑l)
⊢ ∃ l, l ∈ subchain s ∧ length l = n
case inr
α : Type u_1
β : Type ?u.3758
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
n : ℕ
hn : ↑n ≤ chainHeight s
ha : BddAbove (range fun l => length ↑l)
⊢ ∃ l, l ∈ subchain s ∧ length l = n
obtain ⟨⟨l, h₁, h₂⟩, e : l.length = _⟩ := Nat.sSup_mem (Set.range_nonempty _) ha
case inr.intro.mk.intro
α : Type u_1
β : Type ?u.3758
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l✝ : List α
a : α
n : ℕ
hn : ↑n ≤ chainHeight s
ha : BddAbove (range fun l => length ↑l)
l : List α
h₁ : Chain' (fun x x_1 => x < x_1) l
h₂ : ∀ (i : α), i ∈ l → i ∈ s
e : length l = sSup (range fun l => length ↑l)
⊢ n ≤ length l
case inr.intro.mk.intro
α : Type u_1
β : Type ?u.3758
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l✝ : List α
a : α
n : ℕ
hn : ↑n ≤ chainHeight s
ha : BddAbove (range fun l => length ↑l)
l : List α
h₁ : Chain' (fun x x_1 => x < x_1) l
h₂ : ∀ (i : α), i ∈ l → i ∈ s
e : length l = sSup (range fun l => length ↑l)
⊢ ∃ l, l ∈ subchain s ∧ length l = n
refine'
  ⟨l.take n, ⟨h₁.take _, fun x h ↦ h₂ _ <| take_subset _ _ h⟩,
    (l.length_take n).trans <| min_eq_left <| _⟩
no goals
case inr.intro.mk.intro
α : Type u_1
β : Type ?u.3758
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l✝ : List α
a : α
n : ℕ
hn : ↑n ≤ chainHeight s
ha : BddAbove (range fun l => length ↑l)
l : List α
h₁ : Chain' (fun x x_1 => x < x_1) l
h₂ : ∀ (i : α), i ∈ l → i ∈ s
e : length l = sSup (range fun l => length ↑l)
⊢ n ≤ length l
rwa [e, ← Nat.cast_le (α := ℕ∞), sSup_range, ENat.coe_iSup ha, ← chainHeight_eq_iSup_subtype]