case inl
ι : Type ?u.131283
inst✝ : Fintype ι
a : ℝ
⊢ ↑↑volume (EMetric.ball a ⊤) = 2 * ⊤

case inr
ι : Type ?u.131283
inst✝ : Fintype ι
a : ℝ
r : ℝ≥0∞
hr : r ≠ ⊤
⊢ ↑↑volume (EMetric.ball a r) = 2 * r
ι : Type ?u.131283
inst✝ : Fintype ι
a : ℝ
r : ℝ≥0∞
⊢ ↑↑volume (EMetric.ball a r) = 2 * r
rcases eq_or_ne r ∞ with (rfl | hr)
no goals
case inl
ι : Type ?u.131283
inst✝ : Fintype ι
a : ℝ
⊢ ↑↑volume (EMetric.ball a ⊤) = 2 * ⊤
rw [Metric.emetric_ball_top, volume_univ, two_mul, _root_.top_add]
case inr.intro
ι : Type ?u.131283
inst✝ : Fintype ι
a : ℝ
r : ℝ≥0
⊢ ↑↑volume (EMetric.ball a ↑r) = 2 * ↑r
case inr
ι : Type ?u.131283
inst✝ : Fintype ι
a : ℝ
r : ℝ≥0∞
hr : r ≠ ⊤
⊢ ↑↑volume (EMetric.ball a r) = 2 * r
lift r to ℝ≥0 using hr
no goals
case inr.intro
ι : Type ?u.131283
inst✝ : Fintype ι
a : ℝ
r : ℝ≥0
⊢ ↑↑volume (EMetric.ball a ↑r) = 2 * ↑r
rw [Metric.emetric_ball_nnreal, volume_ball, two_mul, ← NNReal.coe_add,
  ENNReal.ofReal_coe_nnreal, ENNReal.coe_add, two_mul]