awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (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
F : Type u_2
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace ℝ F
f : E → F
hF : CompleteSpace F
hE : finrank ℝ E = 0
this : Subsingleton E
⊢ μ.real univ • f 0 = HSMul.hSMul (β := F) |(HPow.hPow (α := ℝ) 0 (finrank ℝ E))⁻¹| (∫ (x : E), f x ∂μ)
have this₁ : f = fun (x : E) ↦ f 0
Tactic: have : f = fun _ => f 0 := by ext x; rw [Subsingleton.elim x 0]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (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 : Type u_2
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace ℝ F
f : E → F
hF : CompleteSpace F
hE : finrank ℝ E = 0
this_1 : Subsingleton E
this : f = fun (x : E) ↦ f 0
| HSMul.hSMul (β := F) |(HPow.hPow (α := ℝ) 0 (finrank ℝ E))⁻¹| (∫ (x : E), f x ∂μ)
have rw : HSMul.hSMul (β := F) |(HPow.hPow (α := ℝ) 0 (finrank ℝ E))⁻¹| (∫ (x : E), (fun (x : E) ↦ f 0) x ∂μ)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (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 : Type u_2
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace ℝ F
f : E → F
hF : CompleteSpace F
hE : finrank ℝ E = 0
this_1 : Subsingleton E
this : f = fun (x : E) ↦ f 0
⊢ μ.real univ • f 0 = HSMul.hSMul (β := F) |(HPow.hPow (α := ℝ) 0 (finrank ℝ E))⁻¹| (∫ (x : E), f x ∂μ)
have pos : μ.real univ • f 0 = HSMul.hSMul (β := F) |(HPow.hPow (α := ℝ) 0 (finrank ℝ E))⁻¹| (∫ (x : E), (fun (x : E) ↦ f 0) x ∂μ)
Tactic: conv_rhs => rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (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
F : Type u_2
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace ℝ F
f : E → F
hF : CompleteSpace F
hE : finrank ℝ E > 0
⊢ μ.real univ • f 0 = HSMul.hSMul (β := F) |(HPow.hPow (α := ℝ) 0 (finrank ℝ E))⁻¹| (∫ (x : E), f x ∂μ)
have this : Nontrivial E
Tactic: have : Nontrivial E := finrank_pos_iff.1 hE
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (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 : Type u_2
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace ℝ F
f : E → F
R : ℝ
hF : CompleteSpace F
hR : R ≠ 0
⊢ ∫ (x : E), f (R • x) ∂μ = HSMul.hSMul (β := F) |(R ^ finrank ℝ E)⁻¹| (∫ (x : E), f x ∂μ)
have f₁ : (@integral _ _ _ _ inst_2 (map (fun (x : E) ↦ R • x) μ) fun (y : E) ↦ f y) =
  HSMul.hSMul (β := F) |(R ^ finrank ℝ E)⁻¹| (∫ (x : E), f x ∂μ)
Tactic: calc
      (∫ x, f (R • x) ∂μ) = ∫ y, f y ∂Measure.map (fun x => R • x) μ :=
        (integral_map_equiv (Homeomorph.smul (isUnit_iff_ne_zero.2 hR).unit).toMeasurableEquiv
            f).symm
      _ = |(R ^ finrank ℝ E)⁻¹| • ∫ x, f x ∂μ := by
        simp only [map_addHaar_smul μ hR, integral_smul_measure, ENNReal.toReal_ofReal, abs_nonneg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (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 : Type u_2
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace ℝ F
f : E → F
R : ℝ
hR : 0 ≤ R
⊢ ∫ (x : E), f (R • x) ∂μ = HSMul.hSMul (β := F) (R ^ finrank ℝ E)⁻¹ (∫ (x : E), f x ∂μ)
have rw : HSMul.hSMul (β := F) |(R ^ finrank ℝ E)⁻¹| (∫ (x : E), f x ∂μ) =
  HSMul.hSMul (β := F) (R ^ finrank ℝ E)⁻¹ (∫ (x : E), f x ∂μ)
Tactic: rw [integral_comp_smul μ f R, abs_of_nonneg (inv_nonneg.2 (pow_nonneg hR _))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (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 : Type u_2
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace ℝ F
f : E → F
R : ℝ
hR : 0 ≤ R
rw :
  HSMul.hSMul (β := F) |(R ^ finrank ℝ E)⁻¹| (∫ (x : E), f x ∂μ) =
    HSMul.hSMul (β := F) (R ^ finrank ℝ E)⁻¹ (∫ (x : E), f x ∂μ)
⊢ ∫ (x : E), f (R • x) ∂μ = HSMul.hSMul (β := F) (R ^ finrank ℝ E)⁻¹ (∫ (x : E), f x ∂μ)
have rw₁ : HSMul.hSMul (β := F) (R ^ finrank ℝ E)⁻¹ (∫ (x : E), f x ∂μ) =
  HSMul.hSMul (β := F) (R ^ finrank ℝ E)⁻¹ (∫ (x : E), f x ∂μ)
Tactic: rw [integral_comp_smul μ f R, abs_of_nonneg (inv_nonneg.2 (pow_nonneg hR _))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (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 : Type u_2
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace ℝ F
f : E → F
R : ℝ
⊢ ∫ (x : E), f (R⁻¹ • x) ∂μ = HSMul.hSMul (β := F) |R ^ finrank ℝ E| (∫ (x : E), f x ∂μ)
have rw : HSMul.hSMul (β := F) |(R⁻¹ ^ finrank ℝ E)⁻¹| (∫ (x : E), f x ∂μ) =
  HSMul.hSMul (β := F) |R ^ finrank ℝ E| (∫ (x : E), f x ∂μ)
Tactic: rw [integral_comp_smul μ f R⁻¹, inv_pow, inv_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (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 : Type u_2
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace ℝ F
f : E → F
R : ℝ
rw :
  HSMul.hSMul (β := F) |(R⁻¹ ^ finrank ℝ E)⁻¹| (∫ (x : E), f x ∂μ) =
    HSMul.hSMul (β := F) |R ^ finrank ℝ E| (∫ (x : E), f x ∂μ)
⊢ ∫ (x : E), f (R⁻¹ • x) ∂μ = HSMul.hSMul (β := F) |R ^ finrank ℝ E| (∫ (x : E), f x ∂μ)
have rw₁ : HSMul.hSMul (β := F) |(R ^ finrank ℝ E)⁻¹⁻¹| (∫ (x : E), f x ∂μ) =
  HSMul.hSMul (β := F) |R ^ finrank ℝ E| (∫ (x : E), f x ∂μ)
Tactic: rw [integral_comp_smul μ f R⁻¹, inv_pow, inv_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (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 : Type u_2
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace ℝ F
f : E → F
R : ℝ
rw :
  HSMul.hSMul (β := F) |(R⁻¹ ^ finrank ℝ E)⁻¹| (∫ (x : E), f x ∂μ) =
    HSMul.hSMul (β := F) |R ^ finrank ℝ E| (∫ (x : E), f x ∂μ)
rw₁ :
  HSMul.hSMul (β := F) |(R ^ finrank ℝ E)⁻¹⁻¹| (∫ (x : E), f x ∂μ) =
    HSMul.hSMul (β := F) |R ^ finrank ℝ E| (∫ (x : E), f x ∂μ)
⊢ ∫ (x : E), f (R⁻¹ • x) ∂μ = HSMul.hSMul (β := F) |R ^ finrank ℝ E| (∫ (x : E), f x ∂μ)
have rw₂ : HSMul.hSMul (β := F) |R ^ finrank ℝ E| (∫ (x : E), f x ∂μ) = HSMul.hSMul (β := F) |R ^ finrank ℝ E| (∫ (x : E), f x ∂μ)
Tactic: rw [integral_comp_smul μ f R⁻¹, inv_pow, inv_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (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 : Type u_2
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace ℝ F
f : E → F
R : ℝ
hR : 0 ≤ R
⊢ ∫ (x : E), f (R⁻¹ • x) ∂μ = HSMul.hSMul (β := F) (R ^ finrank ℝ E) (∫ (x : E), f x ∂μ)
have rw : HSMul.hSMul (β := F) |R ^ finrank ℝ E| (∫ (x : E), f x ∂μ) = HSMul.hSMul (β := F) (R ^ finrank ℝ E) (∫ (x : E), f x ∂μ)
Tactic: rw [integral_comp_inv_smul μ f R, abs_of_nonneg (pow_nonneg hR _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (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 : Type u_2
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace ℝ F
f : E → F
R : ℝ
hR : 0 ≤ R
rw :
  HSMul.hSMul (β := F) |R ^ finrank ℝ E| (∫ (x : E), f x ∂μ) =
    HSMul.hSMul (β := F) (R ^ finrank ℝ E) (∫ (x : E), f x ∂μ)
⊢ ∫ (x : E), f (R⁻¹ • x) ∂μ = HSMul.hSMul (β := F) (R ^ finrank ℝ E) (∫ (x : E), f x ∂μ)
have rw₁ : HSMul.hSMul (β := F) (R ^ finrank ℝ E) (∫ (x : E), f x ∂μ) = HSMul.hSMul (β := F) (R ^ finrank ℝ E) (∫ (x : E), f x ∂μ)
Tactic: rw [integral_comp_inv_smul μ f R, abs_of_nonneg (pow_nonneg hR _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (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 : Type u_2
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace ℝ F
f : E → F
R : ℝ
s : Set E
hR : R ≠ 0
e : E ≃ᵐ E := Homeomorph.toMeasurableEquiv (Homeomorph.smul (Units.mk0 R hR))
⊢ Eq.{u_2 + 1} (α := F) (∫ (x : E) in s, f (R • x) ∂μ)
    (∫ (x : E) in preimage (β := E) (⇑e : (a : E) → E) ((⇑e.symm : (a : E) → E) ⁻¹' s), f ((e : (a : E) → E) x) ∂μ)
have simp : Eq.{u_2 + 1} (α := F) (∫ (x : E) in s, f (R • x) ∂μ) (∫ (x : E) in s, f ((e : (a : E) → E) x) ∂μ)
Tactic: simp [← preimage_comp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (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 : Type u_2
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace ℝ F
f : E → F
R : ℝ
s : Set E
hR : R ≠ 0
e : E ≃ᵐ E := Homeomorph.toMeasurableEquiv (Homeomorph.smul (Units.mk0 R hR))
⊢ HSMul.hSMul (β := F) |(R ^ finrank ℝ E)⁻¹| (∫ (y : E) in (⇑e.symm : (a : E) → E) ⁻¹' s, f y ∂μ) =
    HSMul.hSMul (β := F) |(R ^ finrank ℝ E)⁻¹| (∫ (x : E) in R • s, f x ∂μ)
have e_a : (⇑e.symm : (a : E) → E) ⁻¹' s = R • s
Tactic: congr 3
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (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 : Type u_2
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace ℝ F
f : E → F
R : ℝ
s : Set E
hR : R ≠ 0
e : E ≃ᵐ E := Homeomorph.toMeasurableEquiv (Homeomorph.smul (Units.mk0 R hR))
⊢ (⇑e.symm : (a : E) → E) ⁻¹' s = R • s
have e_a : ∀ (y : E), Membership.mem (γ := Set E) ((⇑e.symm : (a : E) → E) ⁻¹' s) y ↔ y ∈ R • s
Tactic: ext y
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (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 : Type u_2
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace ℝ F
f : E → F
R : ℝ
s : Set E
hR : R ≠ 0
e : E ≃ᵐ E := Homeomorph.toMeasurableEquiv (Homeomorph.smul (Units.mk0 R hR))
y : E
⊢ Membership.mem (γ := Set E) ((⇑e.symm : (a : E) → E) ⁻¹' s) y ↔ y ∈ R • s
have e_a : Membership.mem (γ := Set E) ((⇑e.symm : (a : E) → E) ⁻¹' s) y ↔ R⁻¹ • y ∈ s
Tactic: rw [mem_smul_set_iff_inv_smul_mem₀ hR]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (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 : Type u_2
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace ℝ F
f : E → F
R : ℝ
s : Set E
hR : R ≠ 0
e : E ≃ᵐ E := Homeomorph.toMeasurableEquiv (Homeomorph.smul (Units.mk0 R hR))
⊢ ∫ (x : E) in s, f (R • x) ∂μ = HSMul.hSMul (β := F) |(R ^ finrank ℝ E)⁻¹| (∫ (x : E) in R • s, f x ∂μ)
have x : Eq.{u_2 + 1} (α := F) (∫ (x : E) in s, f (R • x) ∂μ)
  (∫ (x : E) in preimage (β := E) (⇑e : (a : E) → E) ((⇑e.symm : (a : E) → E) ⁻¹' s), f ((e : (a : E) → E) x) ∂μ)
Tactic: calc
  ∫ x in s, f (R • x) ∂μ
    = ∫ x in e ⁻¹' e.symm ⁻¹' s, f (e x) ∂μ := by simp [← preimage_comp]; rfl
  _ = ∫ y in e.symm ⁻¹' s, f y ∂map (fun x ↦ R • x) μ := (setIntegral_map_equiv _ _ _).symm
  _ = |(R ^ finrank ℝ E)⁻¹| • ∫ y in e.symm ⁻¹' s, f y ∂μ := by
    simp [map_addHaar_smul μ hR, integral_smul_measure, ENNReal.toReal_ofReal, abs_nonneg]
  _ = |(R ^ finrank ℝ E)⁻¹| • ∫ x in R • s, f x ∂μ := by
    congr 3
    ext y
    rw [mem_smul_set_iff_inv_smul_mem₀ hR]
    rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (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 : Type u_2
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace ℝ F
f : E → F
R : ℝ
s : Set E
hR : R ≠ 0
e : E ≃ᵐ E := Homeomorph.toMeasurableEquiv (Homeomorph.smul (Units.mk0 R hR))
x :
  Eq.{u_2 + 1} (α := F) (∫ (x : E) in s, f (R • x) ∂μ)
    (∫ (x : E) in preimage (β := E) (⇑e : (a : E) → E) ((⇑e.symm : (a : E) → E) ⁻¹' s), f ((e : (a : E) → E) x) ∂μ)
⊢ ∫ (x : E) in s, f (R • x) ∂μ = HSMul.hSMul (β := F) |(R ^ finrank ℝ E)⁻¹| (∫ (x : E) in R • s, f x ∂μ)
have x₁ : (@integral _ _ _ _ inst_2 (restrict (map (fun (x : E) ↦ R • x) μ) ((⇑e.symm : (a : E) → E) ⁻¹' s)) fun (y : E) ↦ f y) =
  HSMul.hSMul (β := F) |(R ^ finrank ℝ E)⁻¹| (∫ (y : E) in (⇑e.symm : (a : E) → E) ⁻¹' s, f y ∂μ)
Tactic: calc
  ∫ x in s, f (R • x) ∂μ
    = ∫ x in e ⁻¹' e.symm ⁻¹' s, f (e x) ∂μ := by simp [← preimage_comp]; rfl
  _ = ∫ y in e.symm ⁻¹' s, f y ∂map (fun x ↦ R • x) μ := (setIntegral_map_equiv _ _ _).symm
  _ = |(R ^ finrank ℝ E)⁻¹| • ∫ y in e.symm ⁻¹' s, f y ∂μ := by
    simp [map_addHaar_smul μ hR, integral_smul_measure, ENNReal.toReal_ofReal, abs_nonneg]
  _ = |(R ^ finrank ℝ E)⁻¹| • ∫ x in R • s, f x ∂μ := by
    congr 3
    ext y
    rw [mem_smul_set_iff_inv_smul_mem₀ hR]
    rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (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 : Type u_2
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace ℝ F
f : E → F
R : ℝ
s : Set E
hR : R ≠ 0
e : E ≃ᵐ E := Homeomorph.toMeasurableEquiv (Homeomorph.smul (Units.mk0 R hR))
x :
  Eq.{u_2 + 1} (α := F) (∫ (x : E) in s, f (R • x) ∂μ)
    (∫ (x : E) in preimage (β := E) (⇑e : (a : E) → E) ((⇑e.symm : (a : E) → E) ⁻¹' s), f ((e : (a : E) → E) x) ∂μ)
x₁ :
  (@integral _ _ _ _ inst_2 (restrict (map (fun (x : E) ↦ R • x) μ) ((⇑e.symm : (a : E) → E) ⁻¹' s)) fun (y : E) ↦
      f y) =
    HSMul.hSMul (β := F) |(R ^ finrank ℝ E)⁻¹| (∫ (y : E) in (⇑e.symm : (a : E) → E) ⁻¹' s, f y ∂μ)
⊢ ∫ (x : E) in s, f (R • x) ∂μ = HSMul.hSMul (β := F) |(R ^ finrank ℝ E)⁻¹| (∫ (x : E) in R • s, f x ∂μ)
have x₂ : HSMul.hSMul (β := F) |(R ^ finrank ℝ E)⁻¹| (∫ (y : E) in (⇑e.symm : (a : E) → E) ⁻¹' s, f y ∂μ) =
  HSMul.hSMul (β := F) |(R ^ finrank ℝ E)⁻¹| (∫ (x : E) in R • s, f x ∂μ)
Tactic: calc
  ∫ x in s, f (R • x) ∂μ
    = ∫ x in e ⁻¹' e.symm ⁻¹' s, f (e x) ∂μ := by simp [← preimage_comp]; rfl
  _ = ∫ y in e.symm ⁻¹' s, f y ∂map (fun x ↦ R • x) μ := (setIntegral_map_equiv _ _ _).symm
  _ = |(R ^ finrank ℝ E)⁻¹| • ∫ y in e.symm ⁻¹' s, f y ∂μ := by
    simp [map_addHaar_smul μ hR, integral_smul_measure, ENNReal.toReal_ofReal, abs_nonneg]
  _ = |(R ^ finrank ℝ E)⁻¹| • ∫ x in R • s, f x ∂μ := by
    congr 3
    ext y
    rw [mem_smul_set_iff_inv_smul_mem₀ hR]
    rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (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 : Type u_2
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace ℝ F
f : E → F
R : ℝ
s : Set E
hR : 0 < R
⊢ ∫ (x : E) in s, f (R • x) ∂μ = HSMul.hSMul (β := F) (R ^ finrank ℝ E)⁻¹ (∫ (x : E) in R • s, f x ∂μ)
have rw : HSMul.hSMul (β := F) |(R ^ finrank ℝ E)⁻¹| (∫ (x : E) in R • s, f x ∂μ) =
  HSMul.hSMul (β := F) (R ^ finrank ℝ E)⁻¹ (∫ (x : E) in R • s, f x ∂μ)
Tactic: rw [setIntegral_comp_smul μ f s hR.ne', abs_of_nonneg (inv_nonneg.2 (pow_nonneg hR.le _))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (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 : Type u_2
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace ℝ F
f : E → F
R : ℝ
s : Set E
hR : 0 < R
rw :
  HSMul.hSMul (β := F) |(R ^ finrank ℝ E)⁻¹| (∫ (x : E) in R • s, f x ∂μ) =
    HSMul.hSMul (β := F) (R ^ finrank ℝ E)⁻¹ (∫ (x : E) in R • s, f x ∂μ)
⊢ ∫ (x : E) in s, f (R • x) ∂μ = HSMul.hSMul (β := F) (R ^ finrank ℝ E)⁻¹ (∫ (x : E) in R • s, f x ∂μ)
have rw₁ : HSMul.hSMul (β := F) (R ^ finrank ℝ E)⁻¹ (∫ (x : E) in R • s, f x ∂μ) =
  HSMul.hSMul (β := F) (R ^ finrank ℝ E)⁻¹ (∫ (x : E) in R • s, f x ∂μ)
Tactic: rw [setIntegral_comp_smul μ f s hR.ne', abs_of_nonneg (inv_nonneg.2 (pow_nonneg hR.le _))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
g : ℝ → F
a : ℝ
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ g (a * x)) =
    HSMul.hSMul (β := F) |a⁻¹| (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : ℝ) ↦ g y)
have simp_rw : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ g (a • x)) =
  HSMul.hSMul (β := F) |a⁻¹| (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : ℝ) ↦ g y)
Tactic: simp_rw [← smul_eq_mul, Measure.integral_comp_smul, Module.finrank_self, pow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
g : ℝ → F
a : ℝ
simp_rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ g (a • x)) =
    HSMul.hSMul (β := F) |a⁻¹| (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : ℝ) ↦ g y)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ g (a * x)) =
    HSMul.hSMul (β := F) |a⁻¹| (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : ℝ) ↦ g y)
have simp_rw₁ : HSMul.hSMul (β := F) |(a ^ finrank ℝ ℝ)⁻¹| (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ g x) =
  HSMul.hSMul (β := F) |a⁻¹| (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ g x)
Tactic: simp_rw [← smul_eq_mul, Measure.integral_comp_smul, Module.finrank_self, pow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
g : ℝ → F
a : ℝ
simp_rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ g (a • x)) =
    HSMul.hSMul (β := F) |a⁻¹| (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : ℝ) ↦ g y)
simp_rw₁ :
  HSMul.hSMul (β := F) |(a ^ finrank ℝ ℝ)⁻¹|
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ g x) =
    HSMul.hSMul (β := F) |a⁻¹| (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ g x)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ g (a * x)) =
    HSMul.hSMul (β := F) |a⁻¹| (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : ℝ) ↦ g y)
have simp_rw₂ : HSMul.hSMul (β := F) |(HPow.hPow (β := ℕ) a 1)⁻¹|
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ g x) =
  HSMul.hSMul (β := F) |a⁻¹| (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ g x)
Tactic: simp_rw [← smul_eq_mul, Measure.integral_comp_smul, Module.finrank_self, pow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
g : ℝ → F
a : ℝ
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ g (a⁻¹ * x)) =
    HSMul.hSMul (β := F) |a| (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : ℝ) ↦ g y)
have simp_rw : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ g (a⁻¹ • x)) =
  HSMul.hSMul (β := F) |a| (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : ℝ) ↦ g y)
Tactic: simp_rw [← smul_eq_mul, Measure.integral_comp_inv_smul, Module.finrank_self, pow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
g : ℝ → F
a : ℝ
simp_rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ g (a⁻¹ • x)) =
    HSMul.hSMul (β := F) |a| (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : ℝ) ↦ g y)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ g (a⁻¹ * x)) =
    HSMul.hSMul (β := F) |a| (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : ℝ) ↦ g y)
have simp_rw₁ : HSMul.hSMul (β := F) |a ^ finrank ℝ ℝ| (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ g x) =
  HSMul.hSMul (β := F) |a| (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ g x)
Tactic: simp_rw [← smul_eq_mul, Measure.integral_comp_inv_smul, Module.finrank_self, pow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
g : ℝ → F
a : ℝ
simp_rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ g (a⁻¹ • x)) =
    HSMul.hSMul (β := F) |a| (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : ℝ) ↦ g y)
simp_rw₁ :
  HSMul.hSMul (β := F) |a ^ finrank ℝ ℝ| (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ g x) =
    HSMul.hSMul (β := F) |a| (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ g x)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ g (a⁻¹ * x)) =
    HSMul.hSMul (β := F) |a| (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : ℝ) ↦ g y)
have simp_rw₂ : HSMul.hSMul (β := F) |HPow.hPow (β := ℕ) a 1|
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ g x) =
  HSMul.hSMul (β := F) |a| (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ g x)
Tactic: simp_rw [← smul_eq_mul, Measure.integral_comp_inv_smul, Module.finrank_self, pow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
f : E → F
R : ℝ
hR : R ≠ 0
this : ∀ {g : E → F}, Integrable g μ → ∀ {S : ℝ}, S ≠ 0 → Integrable.{u_1, u_2} (ε := F) (fun (x : E) ↦ g (S • x)) μ
⊢ Integrable.{u_1, u_2} (ε := F) (fun (x : E) ↦ f (R • x)) μ ↔ Integrable f μ
have refine : ∀ (hf : Integrable.{u_1, u_2} (ε := F) (fun (x : E) ↦ f (R • x)) μ), Integrable f μ
Tactic: refine ⟨fun hf => ?_, fun hf => this hf hR⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
f : E → F
R : ℝ
hR : R ≠ 0
this : ∀ {g : E → F}, Integrable g μ → ∀ {S : ℝ}, S ≠ 0 → Integrable.{u_1, u_2} (ε := F) (fun (x : E) ↦ g (S • x)) μ
hf : Integrable.{u_1, u_2} (ε := F) (fun (x : E) ↦ f (R • x)) μ
⊢ Integrable f μ
have h : ∀ (x : E), x = R • R⁻¹ • x
Tactic: convert! this hf (inv_ne_zero hR)