no goals
α : Type u_1
β : Type u_2
γ : Type ?u.101991
ι : Sort ?u.101994
κ : ι → Sort ?u.101999
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f✝ : α ≃o β
s✝ t : LowerSet α
a : α
b : β
f : α ≃o β
s : LowerSet β
⊢ ↑(↑(OrderIso.symm (map f)) s) = ↑(↑(map (OrderIso.symm f)) s)
convert Set.preimage_equiv_eq_image_symm s f.toEquiv