no goals
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2012353
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
x : E
r : ℝ
hr : 0 ≤ r
⊢ ↑↑μ (closedBall x r) = ENNReal.ofReal (r ^ finrank ℝ E) * ↑↑μ (ball 0 1)
rw [add_haar_closedBall' μ x hr, add_haar_closed_unit_ball_eq_add_haar_unit_ball]