no goals
α : Type u
β : Type v
γ : Type w
ι✝ : Sort x
κ : ι✝ → Sort ?u.38746
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
ι : Sort x
p : ι → Prop
f : (i : ι) → p i → β
⊢ l (⨆ (i : ι) (hi : p i), u (f i hi)) = ⨆ (i : ι) (hi : p i), f i hi
simp only [iSup_subtype', gi.l_iSup_u]