no goals
α : Type u
β : Type v
X : Type ?u.551874
ι : Type ?u.551877
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
x y : γ
⊢ nndist x y = 0 ↔ x = y
simp only [← NNReal.eq_iff, ← dist_nndist, imp_self, NNReal.coe_zero, dist_eq_zero]