-- Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
theorem addHaar_smul (r : ℝ) (s : Set E) :
    μ (r • s) = ENNReal.ofReal (abs (r ^ finrank ℝ E)) * μ s

Proof state:
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
s : Set E
hs : s.Nonempty
h : ¬finrank ℝ E = 0
this : Nontrivial E
⊢ μ {0} = ENNReal.ofReal |0 ^ finrank ℝ E| * μ s

Tactic:
simp only [h, zero_mul, ENNReal.ofReal_zero, abs_zero, Ne, not_false_iff,
  zero_pow, measure_singleton]

Result:
no goals

Proof state:
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
s : Set E
hs : s.Nonempty
h : finrank ℝ E = 0
this : Subsingleton E
⊢ μ {0} = ENNReal.ofReal |0 ^ finrank ℝ E| * μ s

Tactic:
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))]

Result:
no goals

Proof state:
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
s : Set E
hs : s.Nonempty
⊢ μ (0 • s) = ENNReal.ofReal |0 ^ finrank ℝ E| * μ s

Tactic:
rw [zero_smul_set hs, ← singleton_zero]

Result:
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
s : Set E
hs : s.Nonempty
⊢ μ {0} = ENNReal.ofReal |0 ^ finrank ℝ E| * μ s

Proof state:
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
r : ℝ
s : Set E
h : r ≠ 0
⊢ μ (r • s) = ENNReal.ofReal |r ^ finrank ℝ E| * μ s

Tactic:
rw [← preimage_smul_inv₀ h, addHaar_preimage_smul μ (inv_ne_zero h), inv_pow, inv_inv]

Result:
no goals

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
s : Set E
⊢ μ (r • s) = ENNReal.ofReal |r ^ finrank ℝ E| * μ s

Tactic:
rcases ne_or_eq r 0 with (h | rfl)

Result:
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
r : ℝ
s : Set E
h : r ≠ 0
⊢ μ (r • s) = ENNReal.ofReal |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
s : Set E
⊢ μ (0 • s) = ENNReal.ofReal |0 ^ finrank ℝ E| * μ s

Proof state:
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
s : Set E
hs : s.Nonempty
h : finrank ℝ E = 0
⊢ μ {0} = ENNReal.ofReal |0 ^ finrank ℝ E| * μ s

Tactic:
haveI : Subsingleton E := finrank_zero_iff.1 h

Result:
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
s : Set E
hs : s.Nonempty
h : finrank ℝ E = 0
this : Subsingleton E
⊢ μ {0} = ENNReal.ofReal |0 ^ finrank ℝ E| * μ s

Proof state:
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
⊢ μ (0 • ∅) = ENNReal.ofReal |0 ^ finrank ℝ E| * μ ∅

Tactic:
simp only [measure_empty, mul_zero, smul_set_empty]

Result:
no goals

Proof state:
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
s : Set E
hs : s.Nonempty
h : ¬finrank ℝ E = 0
⊢ μ {0} = ENNReal.ofReal |0 ^ finrank ℝ E| * μ s

Tactic:
haveI : Nontrivial E := nontrivial_of_finrank_pos (bot_lt_iff_ne_bot.2 h)

Result:
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
s : Set E
hs : s.Nonempty
h : ¬finrank ℝ E = 0
this : Nontrivial E
⊢ μ {0} = ENNReal.ofReal |0 ^ finrank ℝ E| * μ s

Proof state:
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
s : Set E
⊢ μ (0 • s) = ENNReal.ofReal |0 ^ finrank ℝ E| * μ s

Tactic:
rcases eq_empty_or_nonempty s with (rfl | hs)

Result:
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
⊢ μ (0 • ∅) = ENNReal.ofReal |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
s : Set E
hs : s.Nonempty
⊢ μ (0 • s) = ENNReal.ofReal |0 ^ finrank ℝ E| * μ s

Proof state:
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
s : Set E
hs : s.Nonempty
⊢ μ {0} = ENNReal.ofReal |0 ^ finrank ℝ E| * μ s

Tactic:
by_cases h : finrank ℝ E = 0

Result:
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
s : Set E
hs : s.Nonempty
h : finrank ℝ E = 0
⊢ μ {0} = ENNReal.ofReal |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
s : Set E
hs : s.Nonempty
h : ¬finrank ℝ E = 0
⊢ μ {0} = ENNReal.ofReal |0 ^ finrank ℝ E| * μ s