no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort ?u.42081
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
s : Set β
⊢ l (sInf (u '' s)) = sInf s
rw [sInf_image, gi.l_biInf_u, sInf_eq_iInf]