α : Type u_1
β : Type ?u.37265
s t : Set α
inst✝ : Preorder α
a : α
ha : ∀ (b : α), b ∈ s → b < a
⊢ chainHeight (↑ofDual ⁻¹' insert a s) = chainHeight (↑ofDual ⁻¹' s) + 1
α : Type u_1
β : Type ?u.37265
s t : Set α
inst✝ : Preorder α
a : α
ha : ∀ (b : α), b ∈ s → b < a
⊢ chainHeight (insert a s) = chainHeight s + 1
rw [← chainHeight_dual, ← chainHeight_dual s]
no goals
α : Type u_1
β : Type ?u.37265
s t : Set α
inst✝ : Preorder α
a : α
ha : ∀ (b : α), b ∈ s → b < a
⊢ chainHeight (↑ofDual ⁻¹' insert a s) = chainHeight (↑ofDual ⁻¹' s) + 1
exact chainHeight_insert_of_forall_gt _ ha