no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort ?u.37330
a✝ a₁ a₂ : α
b✝ b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
gi : GaloisInsertion l u
a b : β
⊢ l (u a) ⊔ l (u b) = a ⊔ b
simp only [gi.l_u_eq]