α : Type u_1
β : Type ?u.33523
s t : Set α
inst✝ : Preorder α
⊢ chainHeight s = ⨆ (i : α) (_ : i ∈ s), chainHeight (↑ofDual ⁻¹' (s ∩ Iic i))
α : Type u_1
β : Type ?u.33523
s t : Set α
inst✝ : Preorder α
⊢ chainHeight s = ⨆ (i : α) (_ : i ∈ s), chainHeight (s ∩ Iic i)
simp_rw [← chainHeight_dual (_ ∩ _)]
α : Type u_1
β : Type ?u.33523
s t : Set α
inst✝ : Preorder α
⊢ (⨆ (i : αᵒᵈ) (_ : i ∈ ↑ofDual ⁻¹' s), chainHeight (↑ofDual ⁻¹' s ∩ Ici i)) =
    ⨆ (i : α) (_ : i ∈ s), chainHeight (↑ofDual ⁻¹' (s ∩ Iic i))
α : Type u_1
β : Type ?u.33523
s t : Set α
inst✝ : Preorder α
⊢ chainHeight s = ⨆ (i : α) (_ : i ∈ s), chainHeight (↑ofDual ⁻¹' (s ∩ Iic i))
rw [← chainHeight_dual, chainHeight_eq_iSup_Ici]
no goals
α : Type u_1
β : Type ?u.33523
s t : Set α
inst✝ : Preorder α
⊢ (⨆ (i : αᵒᵈ) (_ : i ∈ ↑ofDual ⁻¹' s), chainHeight (↑ofDual ⁻¹' s ∩ Ici i)) =
    ⨆ (i : α) (_ : i ∈ s), chainHeight (↑ofDual ⁻¹' (s ∩ Iic i))
rfl