-- Mathlib/Order/Height.lean
theorem exists_chain_of_le_chainHeight {n : ℕ} (hn : ↑n ≤ s.chainHeight) :
    ∃ l ∈ s.subchain, length l = n

Proof state:
case inl.intro.intro.intro.mk.intro
α : Type u_1
inst✝ : LT α
s : Set α
n : ℕ
hn : ↑n ≤ s.chainHeight
ha : ⨆ l, ↑(↑l).length = ⊤
l : List α
h₁ : Chain' (fun x1 x2 => x1 < x2) l
h₂ : ∀ i ∈ l, i ∈ s
h₃ : ¬(fun x => (↑x).length) ⟨l, ⋯⟩ ≤ n
⊢ ∃ l ∈ s.subchain, l.length = n

Tactic:
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₃⟩

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝ : LT α
s : Set α
n : ℕ
hn : ↑n ≤ s.chainHeight
ha : ⨆ l, ↑(↑l).length < ⊤
⊢ ∃ l ∈ s.subchain, l.length = n

Tactic:
rw [ENat.iSup_coe_lt_top] at ha

Result:
case inr
α : Type u_1
inst✝ : LT α
s : Set α
n : ℕ
hn : ↑n ≤ s.chainHeight
ha : BddAbove (range fun l => (↑l).length)
⊢ ∃ l ∈ s.subchain, l.length = n

Proof state:
case inr.intro.mk.intro
α : Type u_1
inst✝ : LT α
s : Set α
n : ℕ
hn : ↑n ≤ s.chainHeight
ha : BddAbove (range fun l => (↑l).length)
l : List α
h₁ : Chain' (fun x1 x2 => x1 < x2) l
h₂ : ∀ i ∈ l, i ∈ s
e : l.length = sSup (range fun l => (↑l).length)
⊢ n ≤ l.length

Tactic:
rwa [e, ← Nat.cast_le (α := ℕ∞), sSup_range, ENat.coe_iSup ha, ← chainHeight_eq_iSup_subtype]

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝ : LT α
s : Set α
n : ℕ
hn : ↑n ≤ s.chainHeight
ha : BddAbove (range fun l => (↑l).length)
⊢ ∃ l ∈ s.subchain, l.length = n

Tactic:
obtain ⟨⟨l, h₁, h₂⟩, e : l.length = _⟩ := Nat.sSup_mem (Set.range_nonempty _) ha

Result:
case inr.intro.mk.intro
α : Type u_1
inst✝ : LT α
s : Set α
n : ℕ
hn : ↑n ≤ s.chainHeight
ha : BddAbove (range fun l => (↑l).length)
l : List α
h₁ : Chain' (fun x1 x2 => x1 < x2) l
h₂ : ∀ i ∈ l, i ∈ s
e : l.length = sSup (range fun l => (↑l).length)
⊢ ∃ l ∈ s.subchain, l.length = n

Proof state:
case inr.intro.mk.intro
α : Type u_1
inst✝ : LT α
s : Set α
n : ℕ
hn : ↑n ≤ s.chainHeight
ha : BddAbove (range fun l => (↑l).length)
l : List α
h₁ : Chain' (fun x1 x2 => x1 < x2) l
h₂ : ∀ i ∈ l, i ∈ s
e : l.length = sSup (range fun l => (↑l).length)
⊢ ∃ l ∈ s.subchain, l.length = n

Tactic:
refine
  ⟨l.take n, ⟨h₁.take _, fun x h ↦ h₂ _ <| take_subset _ _ h⟩,
    (l.length_take n).trans <| min_eq_left <| ?_⟩

Result:
case inr.intro.mk.intro
α : Type u_1
inst✝ : LT α
s : Set α
n : ℕ
hn : ↑n ≤ s.chainHeight
ha : BddAbove (range fun l => (↑l).length)
l : List α
h₁ : Chain' (fun x1 x2 => x1 < x2) l
h₂ : ∀ i ∈ l, i ∈ s
e : l.length = sSup (range fun l => (↑l).length)
⊢ n ≤ l.length

Proof state:
case inl
α : Type u_1
inst✝ : LT α
s : Set α
n : ℕ
hn : ↑n ≤ s.chainHeight
ha : ⨆ l, ↑(↑l).length = ⊤
⊢ ∃ l ∈ s.subchain, l.length = n

Tactic:
obtain ⟨_, ⟨⟨l, h₁, h₂⟩, rfl⟩, h₃⟩ :=
  not_bddAbove_iff'.mp (WithTop.iSup_coe_eq_top.1 ha) n

Result:
case inl.intro.intro.intro.mk.intro
α : Type u_1
inst✝ : LT α
s : Set α
n : ℕ
hn : ↑n ≤ s.chainHeight
ha : ⨆ l, ↑(↑l).length = ⊤
l : List α
h₁ : Chain' (fun x1 x2 => x1 < x2) l
h₂ : ∀ i ∈ l, i ∈ s
h₃ : ¬(fun x => (↑x).length) ⟨l, ⋯⟩ ≤ n
⊢ ∃ l ∈ s.subchain, l.length = n

Proof state:
α : Type u_1
inst✝ : LT α
s : Set α
n : ℕ
hn : ↑n ≤ s.chainHeight
⊢ ∃ l ∈ s.subchain, l.length = n

Tactic:
rcases (le_top : s.chainHeight ≤ ⊤).eq_or_lt with ha | ha <;>
  rw [chainHeight_eq_iSup_subtype] at ha

Result:
case inl
α : Type u_1
inst✝ : LT α
s : Set α
n : ℕ
hn : ↑n ≤ s.chainHeight
ha : ⨆ l, ↑(↑l).length = ⊤
⊢ ∃ l ∈ s.subchain, l.length = n

case inr
α : Type u_1
inst✝ : LT α
s : Set α
n : ℕ
hn : ↑n ≤ s.chainHeight
ha : ⨆ l, ↑(↑l).length < ⊤
⊢ ∃ l ∈ s.subchain, l.length = n