no goals
α : Type u
β : Type v
X : Type ?u.549373
ι : Type ?u.549376
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
x y : γ
⊢ dist x y ≤ 0 ↔ x = y
simpa [le_antisymm_iff, dist_nonneg] using @dist_eq_zero _ _ x y