no goals
α : Type u
β : Type v
inst✝ : TopologicalSpace α
s t : Set α
⊢ SeparatedNhds s t ↔ Disjoint (𝓝ˢ s) (𝓝ˢ t)
simp only [(hasBasis_nhdsSet s).disjoint_iff (hasBasis_nhdsSet t), SeparatedNhds, exists_prop, ←
  exists_and_left, and_assoc, and_comm, and_left_comm]