no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.299672
ι : Sort x
s : Set α
f : α → Filter β
⊢ join (map f (𝓟 s)) = ⨆ (x : α) (_ : x ∈ s), f x
simp only [sSup_image, join_principal_eq_sSup, map_principal, eq_self_iff_true]