no goals
α : Type u_2
β : Type u_1
β₂ : Type ?u.81152
γ : Type ?u.81155
ι : Sort ?u.81158
ι' : Sort ?u.81161
κ : ι → Sort ?u.81166
κ' : ι' → Sort ?u.81171
inst✝¹ : CompleteLattice α
f✝ g s✝ t : ι → α
a b : α
inst✝ : CompleteLattice β
f : α ≃o β
s : Set α
⊢ ↑f (sSup s) = ⨆ (a : α) (_ : a ∈ s), ↑f a
simp only [sSup_eq_iSup, OrderIso.map_iSup]