no goals
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : RegularSpace α
a : α
s : Set α
⊢ IsClosed {p | p.fst ⤳ p.snd}
simp only [← isOpen_compl_iff, compl_setOf, ← disjoint_nhds_nhds_iff_not_specializes,
  isOpen_setOf_disjoint_nhds_nhds]