no goals
α : Type u
β : Type v
X : Type ?u.23021
ι : Type ?u.23024
inst✝ : PseudoMetricSpace α
x y : α
r : ℝ
hr : 0 ≤ r
⊢ edist x y ≤ ENNReal.ofReal r ↔ dist x y ≤ r
rw [edist_dist, ENNReal.ofReal_le_ofReal_iff hr]