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.1940240
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
r : ℝ
hr : 0 ≤ r
s : Set E
⊢ ↑↑μ (r • s) = ENNReal.ofReal (r ^ finrank ℝ E) * ↑↑μ s
rw [add_haar_smul, abs_pow, abs_of_nonneg hr]