no goals
ι : Type ?u.476
α : Type u
β : Type v
γ : Type w
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
⊢ Isometry f ↔ ∀ (x y : α), dist (f x) (f y) = dist x y
simp only [isometry_iff_nndist_eq, ← coe_nndist, NNReal.coe_eq]