no goals
α : Type u_1
β : Type ?u.9871
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
n m : ℕ
⊢ ↑n ≤ chainHeight s + ↑m ↔ ∃ l, l ∈ subchain s ∧ n ≤ length l + m
simp_rw [← tsub_le_iff_right, ← ENat.coe_sub, (le_chainHeight_TFAE s (n - m)).out 0 2]