no goals
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T25Space α
x y : α
h : Disjoint (Filter.lift' (𝓝 x) closure) (Filter.lift' (𝓝 y) closure)
hxy : x = y
⊢ False
simp [hxy, nhds_neBot.ne] at h