no goals
α : Type u_1
β : Type ?u.8192
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α
x : α
⊢ Disjoint (𝓟 s) (𝓝ˢ t) ↔ Disjoint (closure s) t
rw [disjoint_principal_left, ← subset_interior_iff_mem_nhdsSet, interior_compl,
  subset_compl_iff_disjoint_left]