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.1994959
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s✝ : Set E
x : E
r : ℝ
hr : 0 ≤ r
s : ℝ
hs : 0 ≤ s
this : closedBall 0 (r * s) = r • closedBall 0 s
⊢ ↑↑μ (closedBall x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * ↑↑μ (closedBall 0 s)
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.1994959
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s✝ : Set E
x : E
r : ℝ
hr : 0 ≤ r
s : ℝ
hs : 0 ≤ s
⊢ ↑↑μ (closedBall x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * ↑↑μ (closedBall 0 s)
have : closedBall (0 : E) (r * s) = r • closedBall (0 : E) s := by
  simp [smul_closedBall r (0 : E) hs, abs_of_nonneg hr]
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.1994959
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s✝ : Set E
x : E
r : ℝ
hr : 0 ≤ r
s : ℝ
hs : 0 ≤ s
this : closedBall 0 (r * s) = r • closedBall 0 s
⊢ ↑↑μ (closedBall x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * ↑↑μ (closedBall 0 s)
simp only [this, add_haar_smul, abs_of_nonneg hr, add_haar_closedBall_center, abs_pow]
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.1994959
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s✝ : Set E
x : E
r : ℝ
hr : 0 ≤ r
s : ℝ
hs : 0 ≤ s
⊢ closedBall 0 (r * s) = r • closedBall 0 s
simp [smul_closedBall r (0 : E) hs, abs_of_nonneg hr]