no goals
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LocallyCompactSpace α
inst✝ : T2Space α
x y : α
h : x ≠ y
⊢ ∃ u v, u ∈ 𝓝 x ∧ v ∈ 𝓝 y ∧ IsCompact u ∧ IsCompact v ∧ Disjoint u v
simpa only [exists_prop, ← exists_and_left, and_comm, and_assoc, and_left_comm] using
  ((compact_basis_nhds x).disjoint_iff (compact_basis_nhds y)).1 (disjoint_nhds_nhds.2 h)