no goals
α : Type u_1
β : Type ?u.57128
γ : Type ?u.57131
ι : Sort ?u.57134
ι' : Sort ?u.57137
l l' : Filter α
p : ι → Prop
s✝ : ι → Set α
t✝ : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
s t : Set α
⊢ Disjoint (𝓟 s) (𝓟 t) ↔ Disjoint s t
rw [← subset_compl_iff_disjoint_left, disjoint_principal_left, mem_principal]