case inl
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.1982183
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
s✝ : Set E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
s : ℝ
h : 0 = r
⊢ ↑↑μ (ball x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * ↑↑μ (ball 0 s)

case inr
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.1982183
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
s✝ : Set E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
s : ℝ
h : 0 < r
⊢ ↑↑μ (ball x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * ↑↑μ (ball 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.1982183
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
s✝ : Set E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
s : ℝ
⊢ ↑↑μ (ball x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * ↑↑μ (ball 0 s)
rcases LE.le.eq_or_lt hr with (h | h)
no goals
case inl
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.1982183
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
s✝ : Set E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
s : ℝ
h : 0 = r
⊢ ↑↑μ (ball x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * ↑↑μ (ball 0 s)
simp only [← h, zero_pow (finrank_pos (K := ℝ) (V := E)), measure_empty, zero_mul,
  ENNReal.ofReal_zero, ball_zero]
no goals
case inr
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.1982183
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
s✝ : Set E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
s : ℝ
h : 0 < r
⊢ ↑↑μ (ball x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * ↑↑μ (ball 0 s)
exact add_haar_ball_mul_of_pos μ x h s