no goals
α : Type u
β : Type v
X : Type ?u.165907
ι : Type ?u.165910
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ≥0
⊢ EMetric.closedBall x ↑ε = closedBall x ↑ε
rw [← Metric.emetric_closedBall ε.coe_nonneg, ENNReal.ofReal_coe_nnreal]