no goals
X : Type u_1
Y : Type ?u.31736
Z : Type ?u.31739
α : Type ?u.31742
ι : Type ?u.31745
π : ι → Type ?u.31750
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
⊢ (x ~ᵢ y) ↔ closure {x} = closure {y}
simp only [inseparable_iff_specializes_and, specializes_iff_closure_subset, ← subset_antisymm_iff,
  eq_comm]