no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.102736
ι : Sort x
f g : Filter α
s t : Set α
f₁ f₂ : Filter (Filter α)
x : Set α
⊢ x ∈ join f₁ ⊔ join f₂ ↔ x ∈ join (f₁ ⊔ f₂)
simp only [mem_sup, mem_join]