no goals
α : Type u
β : Type v
inst✝ : TopologicalSpace α
⊢ T2Space α ↔ IsClosed (diagonal α)
simp only [t2Space_iff_disjoint_nhds, ← isOpen_compl_iff, isOpen_iff_mem_nhds, Prod.forall,
  nhds_prod_eq, compl_diagonal_mem_prod, mem_compl_iff, mem_diagonal_iff]