no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort ?u.39544
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
s : Set β
⊢ l (sSup (u '' s)) = sSup s
rw [sSup_image, gi.l_biSup_u, sSup_eq_iSup]