no goals
α : Type u_1
β : Type ?u.56071
γ : Type ?u.56074
ι : Sort ?u.56077
ι' : Sort ?u.56080
l l' : Filter α
p : ι → Prop
s✝ : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
f : Filter α
s : Set α
⊢ Disjoint f (𝓟 s) ↔ sᶜ ∈ f
rw [mem_iff_inf_principal_compl, compl_compl, disjoint_iff]