no goals
α : Type u
β : Type v
X : Type ?u.166352
ι : Type ?u.166355
inst✝ : PseudoMetricSpace α
x y : α
⊢ Inseparable x y ↔ dist x y = 0
rw [EMetric.inseparable_iff, edist_nndist, dist_nndist, ENNReal.coe_eq_zero, NNReal.coe_eq_zero]