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.1985564
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
s : Set E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
⊢ ↑↑μ (ball x r) = ENNReal.ofReal (r ^ finrank ℝ E) * ↑↑μ (ball 0 1)
rw [← add_haar_ball_mul μ x hr, mul_one]