no goals
α : Type u
β : Type v
X : Type ?u.549105
ι : Type ?u.549108
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
x y : γ
⊢ dist x y ≠ 0 ↔ x ≠ y
simpa only [not_iff_not] using dist_eq_zero