awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E ≃ₗ[ℝ] E
s : Set E
A : Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑f : E →ₗ[ℝ] E) : ℝ) (0 : ℝ)
⊢ (μ : (a : Set E) → ℝ≥0∞) ((⇑f : (a : E) → E) ⁻¹' s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑f.symm : E →ₗ[ℝ] E)|)
      ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑f.symm : E →ₗ[ℝ] E) : ℝ)
  (((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑f : E →ₗ[ℝ] E))⁻¹ : ℝ)
Tactic: convert! addHaar_preimage_linearMap μ A s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
s : Set E
⊢ (μ : (a : Set E) → ℝ≥0∞) ((⇑f : (a : E) → E) '' s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have inl : ∀ (hf : Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)),
  (μ : (a : Set E) → ℝ≥0∞) ((⇑f : (a : E) → E) '' s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rcases ne_or_eq (LinearMap.det f) 0 with (hf | hf)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
s : Set E
inl :
  ∀ (hf : Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)),
    (μ : (a : Set E) → ℝ≥0∞) ((⇑f : (a : E) → E) '' s) =
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f|)
        ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) ((⇑f : (a : E) → E) '' s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have inr : ∀ (hf : Eq (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)),
  (μ : (a : Set E) → ℝ≥0∞) ((⇑f : (a : E) → E) '' s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rcases ne_or_eq (LinearMap.det f) 0 with (hf | hf)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
s : Set E
hf : Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)
g : E ≃L[ℝ] E := (f.equivOfDetNeZero hf).toContinuousLinearEquiv
⊢ (μ : (a : Set E) → ℝ≥0∞) ((⇑f : (a : E) → E) '' s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have inl : (μ : (a : Set E) → ℝ≥0∞) ((⇑g : (a : E) → E) '' s) =
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: change μ (g '' s) = _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
s : Set E
hf : Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)
g : E ≃L[ℝ] E := (f.equivOfDetNeZero hf).toContinuousLinearEquiv
⊢ (μ : (a : Set E) → ℝ≥0∞) ((⇑g : (a : E) → E) '' s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have inl : HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑(↑g.symm.symm : E ≃ₗ[ℝ] E) : E →ₗ[ℝ] E)|)
    ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [ContinuousLinearEquiv.image_eq_preimage_symm g s, addHaar_preimage_continuousLinearEquiv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)
⊢ QuasiMeasurePreserving (⇑f : (a : E) → E) μ μ
have refine : map (⇑f : (a : E) → E) μ ≪ μ
Tactic: refine ⟨f.continuous_of_finiteDimensional.measurable, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)
⊢ map (⇑f : (a : E) → E) μ ≪ μ
have rw : ENNReal.ofReal |((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f)⁻¹| • μ ≪ μ
Tactic: rw [map_linearMap_addHaar_eq_smul_addHaar μ hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hr : r ≠ 0
f : E →ₗ[ℝ] E := HSMul.hSMul (β := E →ₗ[ℝ] E) r 1
⊢ map (fun (x : E) ↦ r • x) μ = ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹| • μ
have change : map (⇑f : (a : E) → E) μ = ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹| • μ
Tactic: change Measure.map f μ = _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hr : r ≠ 0
f : E →ₗ[ℝ] E := HSMul.hSMul (β := E →ₗ[ℝ] E) r 1
⊢ Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)
have simp : ¬r ^ finrank ℝ E = 0
Tactic: simp only [f, mul_one, LinearMap.det_smul, Ne, map_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hr : r ≠ 0
f : E →ₗ[ℝ] E := HSMul.hSMul (β := E →ₗ[ℝ] E) r 1
⊢ map (⇑f : (a : E) → E) μ = ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹| • μ
have hf : Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)
Tactic: have hf : LinearMap.det f ≠ 0 := by
    simp only [f, mul_one, LinearMap.det_smul, Ne, map_one]
    exact pow_ne_zero _ hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hr : r ≠ 0
⊢ QuasiMeasurePreserving (fun (x : E) ↦ r • x) μ μ
have refine : map (fun (x : E) ↦ r • x) μ ≪ μ
Tactic: refine ⟨measurable_const_smul r, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hr : r ≠ 0
⊢ map (fun (x : E) ↦ r • x) μ ≪ μ
have rw : ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹| • μ ≪ μ
Tactic: rw [map_addHaar_smul μ hr]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hr : r ≠ 0
s : Set E
⊢ ((map (fun (x : E) ↦ r • x) μ : Measure E) : (a : Set E) → ℝ≥0∞) s =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have rw : (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹| • μ : (a : Set E) → ℝ≥0∞) s =
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [map_addHaar_smul μ hr, coe_smul, Pi.smul_apply, smul_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hr : r ≠ 0
s : Set E
rw :
  (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹| • μ : (a : Set E) → ℝ≥0∞) s =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ((map (fun (x : E) ↦ r • x) μ : Measure E) : (a : Set E) → ℝ≥0∞) s =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have rw₁ : HSMul.hSMul (β := (a : Set E) → ℝ≥0∞) (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹|) (⇑μ : (a : Set E) → ℝ≥0∞) s =
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [map_addHaar_smul μ hr, coe_smul, Pi.smul_apply, smul_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hr : r ≠ 0
s : Set E
rw :
  (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹| • μ : (a : Set E) → ℝ≥0∞) s =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ :
  HSMul.hSMul (β := (a : Set E) → ℝ≥0∞) (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹|) (⇑μ : (a : Set E) → ℝ≥0∞) s =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ((map (fun (x : E) ↦ r • x) μ : Measure E) : (a : Set E) → ℝ≥0∞) s =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have rw₂ : HSMul.hSMul (β := ℝ≥0∞) (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [map_addHaar_smul μ hr, coe_smul, Pi.smul_apply, smul_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hr : r ≠ 0
s : Set E
rw :
  (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹| • μ : (a : Set E) → ℝ≥0∞) s =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ :
  HSMul.hSMul (β := (a : Set E) → ℝ≥0∞) (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹|) (⇑μ : (a : Set E) → ℝ≥0∞) s =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
rw₂ :
  HSMul.hSMul (β := ℝ≥0∞) (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ((map (fun (x : E) ↦ r • x) μ : Measure E) : (a : Set E) → ℝ≥0∞) s =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have rw₃ : HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [map_addHaar_smul μ hr, coe_smul, Pi.smul_apply, smul_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
s : Set E
⊢ (μ : (a : Set E) → ℝ≥0∞) (r • s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |r ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have inl : ∀ (h : r ≠ 0),
  (μ : (a : Set E) → ℝ≥0∞) (r • s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |r ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rcases ne_or_eq r 0 with (h | rfl)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
s : Set E
inl :
  ∀ (h : r ≠ 0),
    (μ : (a : Set E) → ℝ≥0∞) (r • s) =
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |r ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) (r • s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |r ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have inr : (μ : (a : Set E) → ℝ≥0∞) (HSMul.hSMul (α := ℝ) 0 s) =
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |HPow.hPow (α := ℝ) 0 (finrank ℝ E)|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rcases ne_or_eq r 0 with (h | rfl)
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
s : Set E
h : r ≠ 0
⊢ (μ : (a : Set E) → ℝ≥0∞) (r • s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |r ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have inl : (μ : (a : Set E) → ℝ≥0∞) ((fun (x : E) ↦ r⁻¹ • x) ⁻¹' s) =
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |r ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← preimage_smul_inv₀ h, addHaar_preimage_smul μ (inv_ne_zero h), inv_pow, inv_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
s : Set E
h : r ≠ 0
inl :
  (μ : (a : Set E) → ℝ≥0∞) ((fun (x : E) ↦ r⁻¹ • x) ⁻¹' s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |r ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) (r • s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |r ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have inl₁ : HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(r⁻¹ ^ finrank ℝ E)⁻¹|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |r ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← preimage_smul_inv₀ h, addHaar_preimage_smul μ (inv_ne_zero h), inv_pow, inv_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
s : Set E
h : r ≠ 0
inl :
  (μ : (a : Set E) → ℝ≥0∞) ((fun (x : E) ↦ r⁻¹ • x) ⁻¹' s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |r ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
inl₁ :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(r⁻¹ ^ finrank ℝ E)⁻¹|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |r ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) (r • s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |r ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have inl₂ : HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹⁻¹|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |r ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← preimage_smul_inv₀ h, addHaar_preimage_smul μ (inv_ne_zero h), inv_pow, inv_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
s : Set E
h : r ≠ 0
inl :
  (μ : (a : Set E) → ℝ≥0∞) ((fun (x : E) ↦ r⁻¹ • x) ⁻¹' s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |r ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
inl₁ :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(r⁻¹ ^ finrank ℝ E)⁻¹|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |r ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
inl₂ :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹⁻¹|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |r ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) (r • s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |r ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have inl₃ : HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |r ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |r ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← preimage_smul_inv₀ h, addHaar_preimage_smul μ (inv_ne_zero h), inv_pow, inv_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
⊢ (μ : (a : Set E) → ℝ≥0∞) (HSMul.hSMul (α := ℝ) 0 s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |HPow.hPow (α := ℝ) 0 (finrank ℝ E)|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have inr : (μ : (a : Set E) → ℝ≥0∞) (HSMul.hSMul (α := ℝ) (β := Set E) 0 ∅) =
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |HPow.hPow (α := ℝ) 0 (finrank ℝ E)|) ((μ : (a : Set E) → ℝ≥0∞) ∅ : ℝ≥0∞)
Tactic: rcases eq_empty_or_nonempty s with (rfl | hs)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
inr :
  (μ : (a : Set E) → ℝ≥0∞) (HSMul.hSMul (α := ℝ) (β := Set E) 0 ∅) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |HPow.hPow (α := ℝ) 0 (finrank ℝ E)|) ((μ : (a : Set E) → ℝ≥0∞) ∅ : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) (HSMul.hSMul (α := ℝ) 0 s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |HPow.hPow (α := ℝ) 0 (finrank ℝ E)|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have inr₁ : ∀ (hs : s.Nonempty),
  (μ : (a : Set E) → ℝ≥0∞) (HSMul.hSMul (α := ℝ) 0 s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |HPow.hPow (α := ℝ) 0 (finrank ℝ E)|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rcases eq_empty_or_nonempty s with (rfl | hs)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
hs : s.Nonempty
⊢ (μ : (a : Set E) → ℝ≥0∞) (HSMul.hSMul (α := ℝ) 0 s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |HPow.hPow (α := ℝ) 0 (finrank ℝ E)|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have inr : (μ : (a : Set E) → ℝ≥0∞) {0} =
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |HPow.hPow (α := ℝ) 0 (finrank ℝ E)|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [zero_smul_set hs, ← singleton_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
hs : s.Nonempty
⊢ (μ : (a : Set E) → ℝ≥0∞) {0} =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |HPow.hPow (α := ℝ) 0 (finrank ℝ E)|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have pos : ∀ (h : finrank ℝ E = 0),
  (μ : (a : Set E) → ℝ≥0∞) {0} =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |HPow.hPow (α := ℝ) 0 (finrank ℝ E)|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: by_cases h : finrank ℝ E = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
hs : s.Nonempty
pos :
  ∀ (h : finrank ℝ E = 0),
    (μ : (a : Set E) → ℝ≥0∞) {0} =
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |HPow.hPow (α := ℝ) 0 (finrank ℝ E)|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) {0} =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |HPow.hPow (α := ℝ) 0 (finrank ℝ E)|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have neg : ∀ (h : ¬finrank ℝ E = 0),
  (μ : (a : Set E) → ℝ≥0∞) {0} =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |HPow.hPow (α := ℝ) 0 (finrank ℝ E)|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: by_cases h : finrank ℝ E = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
hs : s.Nonempty
h : finrank ℝ E = 0
⊢ (μ : (a : Set E) → ℝ≥0∞) {0} =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |HPow.hPow (α := ℝ) 0 (finrank ℝ E)|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have this : Subsingleton E
Tactic: haveI : Subsingleton E := finrank_zero_iff.1 h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
hs : s.Nonempty
h : ¬finrank ℝ E = 0
⊢ (μ : (a : Set E) → ℝ≥0∞) {0} =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |HPow.hPow (α := ℝ) 0 (finrank ℝ E)|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have this : Nontrivial E
Tactic: haveI : Nontrivial E := nontrivial_of_finrank_pos (bot_lt_iff_ne_bot.2 h)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hr : 0 ≤ r
s : Set E
⊢ (μ : (a : Set E) → ℝ≥0∞) (r • s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have rw : HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |r ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [addHaar_smul, abs_pow, abs_of_nonneg hr]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hr : 0 ≤ r
s : Set E
rw :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |r ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) (r • s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have rw₁ : HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (|r| ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [addHaar_smul, abs_pow, abs_of_nonneg hr]