case a
α : Type u_1
β : Type ?u.31224
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
⊢ ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain (↑ofDual ⁻¹' s) ∧ length l = length l'
case a
α : Type u_1
β : Type ?u.31224
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
⊢ chainHeight s ≤ chainHeight (↑ofDual ⁻¹' s)
rw [chainHeight_le_chainHeight_iff]
case a.intro
α : Type u_1
β : Type ?u.31224
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l✝ : List α
a : α
l : List α
h₁ : Chain' (fun x x_1 => x < x_1) l
h₂ : ∀ (i : α), i ∈ l → i ∈ s
⊢ ∃ l', l' ∈ subchain (↑ofDual ⁻¹' s) ∧ length l = length l'
case a
α : Type u_1
β : Type ?u.31224
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
⊢ ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain (↑ofDual ⁻¹' s) ∧ length l = length l'
rintro l ⟨h₁, h₂⟩
no goals
case a.intro
α : Type u_1
β : Type ?u.31224
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l✝ : List α
a : α
l : List α
h₁ : Chain' (fun x x_1 => x < x_1) l
h₂ : ∀ (i : α), i ∈ l → i ∈ s
⊢ ∃ l', l' ∈ subchain (↑ofDual ⁻¹' s) ∧ length l = length l'
exact ⟨l.reverse, ⟨chain'_reverse.mpr h₁, fun i h ↦ h₂ i ((mem_reverse i l).mp h)⟩,
  (length_reverse _).symm⟩