no goals
α : Type u_1
β : Type u_2
γ : Type ?u.99982
ι : Sort u_3
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : Nonempty ι
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
hf : BddAbove (range f)
⊢ l (⨆ (i : ι), f i) = ⨆ (i : ι), l (f i)
rw [iSup, gc.l_csSup (range_nonempty _) hf, iSup_range']