no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.116529
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Sort w
s : ι → Set α
x : Set α
⊢ (x ∈ ⨆ (x : ι), 𝓟 (s x)) ↔ x ∈ 𝓟 (⋃ (i : ι), s i)
simp only [mem_iSup, mem_principal, iUnion_subset_iff]