no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort ?u.20627
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
⊢ l (sSup s) = ⨆ (a : α) (_ : a ∈ s), l a
simp only [sSup_eq_iSup, gc.l_iSup]