no goals
α : Type u
β : Type v
inst✝ : TopologicalSpace α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ SeparatedNhds s u → SeparatedNhds t u → SeparatedNhds (s ∪ t) u
simpa only [separatedNhds_iff_disjoint, nhdsSet_union, disjoint_sup_left] using And.intro