English
There exists a chain of height equal to the chain height for any n.
Русский
Существует цепь такой высоты, равной высоте цепи, для любого n.
LaTeX
$$$ \\exists \\text{l}, \\ \\text{l} \\in s.\\mathrm{subchain} \\land \\operatorname{length}(\\text{l}) = n. $$$
Lean4
theorem exists_chain_of_le_chainHeight {n : ℕ} (hn : ↑n ≤ s.chainHeight) : ∃ l ∈ s.subchain, length l = n :=
by
rcases (le_top : s.chainHeight ≤ ⊤).eq_or_lt with ha | ha <;> rw [chainHeight_eq_iSup_subtype] at ha
· obtain ⟨_, ⟨⟨l, h₁, h₂⟩, rfl⟩, h₃⟩ := not_bddAbove_iff'.mp (WithTop.iSup_coe_eq_top.1 ha) n
exact
⟨l.take n, ⟨h₁.take _, fun x h ↦ h₂ _ <| take_subset _ _ h⟩,
(l.length_take).trans <| min_eq_left <| le_of_not_ge h₃⟩
· rw [ENat.iSup_coe_lt_top] at ha
obtain ⟨⟨l, h₁, h₂⟩, e : l.length = _⟩ := Nat.sSup_mem (Set.range_nonempty _) ha
refine ⟨l.take n, ⟨h₁.take _, fun x h ↦ h₂ _ <| take_subset _ _ h⟩, (l.length_take).trans <| min_eq_left <| ?_⟩
rwa [e, ← Nat.cast_le (α := ℕ∞), sSup_range, ENat.coe_iSup ha, ← chainHeight_eq_iSup_subtype]
