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.1927122
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
r : ℝ
s : Set E
h : r ≠ 0
⊢ ↑↑μ (r • s) = ENNReal.ofReal (abs (r ^ finrank ℝ E)) * ↑↑μ 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.1927122
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
⊢ ↑↑μ (0 • s) = ENNReal.ofReal (abs (0 ^ finrank ℝ E)) * ↑↑μ 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.1927122
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
r : ℝ
s : Set E
⊢ ↑↑μ (r • s) = ENNReal.ofReal (abs (r ^ finrank ℝ E)) * ↑↑μ s
rcases ne_or_eq r 0 with (h | rfl)
case inr.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.1927122
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
⊢ ↑↑μ (0 • ∅) = ENNReal.ofReal (abs (0 ^ finrank ℝ E)) * ↑↑μ ∅

case inr.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.1927122
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
hs : Set.Nonempty s
⊢ ↑↑μ (0 • s) = ENNReal.ofReal (abs (0 ^ finrank ℝ E)) * ↑↑μ 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.1927122
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
⊢ ↑↑μ (0 • s) = ENNReal.ofReal (abs (0 ^ finrank ℝ E)) * ↑↑μ s
rcases eq_empty_or_nonempty s with (rfl | hs)
case inr.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.1927122
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
hs : Set.Nonempty s
⊢ ↑↑μ {0} = ENNReal.ofReal (abs (0 ^ finrank ℝ E)) * ↑↑μ s
case inr.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.1927122
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
hs : Set.Nonempty s
⊢ ↑↑μ (0 • s) = ENNReal.ofReal (abs (0 ^ finrank ℝ E)) * ↑↑μ s
rw [zero_smul_set hs, ← singleton_zero]
case pos
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.1927122
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
hs : Set.Nonempty s
h : finrank ℝ E = 0
⊢ ↑↑μ {0} = ENNReal.ofReal (abs (0 ^ finrank ℝ E)) * ↑↑μ s

case neg
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.1927122
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
hs : Set.Nonempty s
h : ¬finrank ℝ E = 0
⊢ ↑↑μ {0} = ENNReal.ofReal (abs (0 ^ finrank ℝ E)) * ↑↑μ s
case inr.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.1927122
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
hs : Set.Nonempty s
⊢ ↑↑μ {0} = ENNReal.ofReal (abs (0 ^ finrank ℝ E)) * ↑↑μ s
by_cases h : finrank ℝ E = 0
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.1927122
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
r : ℝ
s : Set E
h : r ≠ 0
⊢ ↑↑μ (r • s) = ENNReal.ofReal (abs (r ^ finrank ℝ E)) * ↑↑μ s
rw [← preimage_smul_inv₀ h, add_haar_preimage_smul μ (inv_ne_zero h), inv_pow, inv_inv]
no goals
case inr.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.1927122
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
⊢ ↑↑μ (0 • ∅) = ENNReal.ofReal (abs (0 ^ finrank ℝ E)) * ↑↑μ ∅
simp only [measure_empty, mul_zero, smul_set_empty]
case pos
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.1927122
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
hs : Set.Nonempty s
h : finrank ℝ E = 0
this : Subsingleton E
⊢ ↑↑μ {0} = ENNReal.ofReal (abs (0 ^ finrank ℝ E)) * ↑↑μ s
case pos
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.1927122
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
hs : Set.Nonempty s
h : finrank ℝ E = 0
⊢ ↑↑μ {0} = ENNReal.ofReal (abs (0 ^ finrank ℝ E)) * ↑↑μ s
haveI : Subsingleton E := finrank_zero_iff.1 h
no goals
case pos
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.1927122
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
hs : Set.Nonempty s
h : finrank ℝ E = 0
this : Subsingleton E
⊢ ↑↑μ {0} = ENNReal.ofReal (abs (0 ^ finrank ℝ E)) * ↑↑μ s
simp only [h, one_mul, ENNReal.ofReal_one, abs_one, Subsingleton.eq_univ_of_nonempty hs,
  pow_zero, Subsingleton.eq_univ_of_nonempty (singleton_nonempty (0 : E))]
case neg
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.1927122
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
hs : Set.Nonempty s
h : ¬finrank ℝ E = 0
this : Nontrivial E
⊢ ↑↑μ {0} = ENNReal.ofReal (abs (0 ^ finrank ℝ E)) * ↑↑μ s
case neg
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.1927122
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
hs : Set.Nonempty s
h : ¬finrank ℝ E = 0
⊢ ↑↑μ {0} = ENNReal.ofReal (abs (0 ^ finrank ℝ E)) * ↑↑μ s
haveI : Nontrivial E := nontrivial_of_finrank_pos (bot_lt_iff_ne_bot.2 h)
no goals
case neg
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.1927122
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
hs : Set.Nonempty s
h : ¬finrank ℝ E = 0
this : Nontrivial E
⊢ ↑↑μ {0} = ENNReal.ofReal (abs (0 ^ finrank ℝ E)) * ↑↑μ s
simp only [h, zero_mul, ENNReal.ofReal_zero, abs_zero, Ne.def, not_false_iff,
  zero_pow', measure_singleton]