no goals
α : Type u_3
β : Type u_1
γ : Type ?u.109072
ι : Type u_2
inst✝ : CompleteLattice α
p : ι → Prop
s : ι → Set β
f : Filter β
u : β → α
h : HasBasis f p s
⊢ (⨅ (i : ι) (_ : p i), sSup (u '' s i)) = ⨅ (i : ι) (_ : p i), ⨆ (a : β) (_ : a ∈ s i), u a
simp only [sSup_image, id]