no goals
α : Type u_1
β : Type u_2
γ : Type ?u.99502
ι : Sort ?u.99505
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : Nonempty ι
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
hne : Set.Nonempty s
hbdd : BddAbove s
⊢ l (sSup s) = sSup (l '' s)
rw [gc.l_csSup hne hbdd, sSup_image']