α : Type u_1
β : Type ?u.7005
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
h : ∀ (n : ℕ), ∃ l, l ∈ subchain s ∧ length l = n
⊢ chainHeight s = ⊤
α : Type u_1
β : Type ?u.7005
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
⊢ chainHeight s = ⊤ ↔ ∀ (n : ℕ), ∃ l, l ∈ subchain s ∧ length l = n
refine' ⟨fun h n ↦ le_chainHeight_iff.1 (le_top.trans_eq h.symm), fun h ↦ _⟩
α : Type u_1
β : Type ?u.7005
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
h : chainHeight s ≠ ⊤
⊢ ∃ n, ∀ (l : List α), l ∈ subchain s → length l ≠ n
α : Type u_1
β : Type ?u.7005
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
h : ∀ (n : ℕ), ∃ l, l ∈ subchain s ∧ length l = n
⊢ chainHeight s = ⊤
contrapose! h
case intro
α : Type u_1
β : Type ?u.7005
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
h : chainHeight s ≠ ⊤
n : ℕ
hn : ↑n = chainHeight s
⊢ ∃ n, ∀ (l : List α), l ∈ subchain s → length l ≠ n
α : Type u_1
β : Type ?u.7005
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
h : chainHeight s ≠ ⊤
⊢ ∃ n, ∀ (l : List α), l ∈ subchain s → length l ≠ n
obtain ⟨n, hn⟩ := WithTop.ne_top_iff_exists.1 h
no goals
case intro
α : Type u_1
β : Type ?u.7005
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
h : chainHeight s ≠ ⊤
n : ℕ
hn : ↑n = chainHeight s
⊢ ∃ n, ∀ (l : List α), l ∈ subchain s → length l ≠ n
exact ⟨n + 1, fun l hs ↦ (Nat.lt_succ_iff.2 <| Nat.cast_le.1 <|
  (length_le_chainHeight_of_mem_subchain hs).trans_eq hn.symm).ne⟩