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