no goals
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : DiscreteTopology ↑s
x : α
hx : x ∈ s
V : Set α
h : V ∈ 𝓝 x
h' : V ∩ s = {x}
⊢ {x}ᶜ ∩ V ∩ s = ∅
rw [inter_assoc, h', compl_inter_self]