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