no goals
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
⊢ T0Space α ↔ ∀ (x y : α), x ≠ y → ¬Inseparable x y
simp only [t0Space_iff_inseparable, Ne.def, not_imp_not]