awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
inst_6 : MeasurableSpace H
inst_7 : SeminormedGroup H
inst_8 : OpensMeasurableSpace H
f : G →* H
hf : Measurable.{u_1, u_2} (α := G) (β := H) (⇑f : (a : G) → H)
x : G
K : PositiveCompacts G := Classical.arbitrary (PositiveCompacts G)
n : ℕ
hn :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    (((haar : Measure G) : (a : Set G) → ℝ≥0∞)
        (interior (↑K : Set G) ∩ preimage.{u_1, u_2} (β := H) (⇑f : (a : G) → H) (ball 1 (↑n : ℝ))) :
      ℝ≥0∞)
this :
  Bornology.IsBounded.{u_2} (α := H)
    ((⇑f : (a : G) → H) '' (interior (↑K : Set G) ∩ preimage.{u_1, u_2} (β := H) (⇑f : (a : G) → H) (ball 1 (↑n : ℝ))))
rw :
  Bornology.IsBounded
    (HSMul.hSMul (α := H) ((f : (a : G) → H) x : H)
      (HDiv.hDiv (α := Set H)
        ((⇑f : (a : G) → H) ''
          (interior (↑K : Set G) ∩ preimage.{u_1, u_2} (β := H) (⇑f : (a : G) → H) (ball 1 (↑n : ℝ))))
        ((⇑f : (a : G) → H) ''
          (interior (↑K : Set G) ∩ preimage.{u_1, u_2} (β := H) (⇑f : (a : G) → H) (ball 1 (↑n : ℝ))))))
⊢ Bornology.IsBounded.{u_2} (α := H)
    ((⇑f : (a : G) → H) ''
      (x •
        (interior (↑K : Set G) ∩ preimage.{u_1, u_2} (β := H) (⇑f : (a : G) → H) (ball 1 (↑n : ℝ)) /
          (interior (↑K : Set G) ∩ preimage.{u_1, u_2} (β := H) (⇑f : (a : G) → H) (ball 1 (↑n : ℝ))))))

Tactic:
rw [image_smul_distrib, image_div]

Premises used: Set.image_smul_distrib, Set.image_div
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
inst_6 : MeasurableSpace H
inst_7 : SeminormedGroup H
inst_8 : OpensMeasurableSpace H
f : G →* H
hf : Measurable.{u_1, u_2} (α := G) (β := H) (⇑f : (a : G) → H)
x : G
K : PositiveCompacts G := Classical.arbitrary (PositiveCompacts G)
n : ℕ
hn :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    (((haar : Measure G) : (a : Set G) → ℝ≥0∞)
        (interior (↑K : Set G) ∩ preimage.{u_1, u_2} (β := H) (⇑f : (a : G) → H) (ball 1 (↑n : ℝ))) :
      ℝ≥0∞)
this :
  Bornology.IsBounded.{u_2} (α := H)
    ((⇑f : (a : G) → H) '' (interior (↑K : Set G) ∩ preimage.{u_1, u_2} (β := H) (⇑f : (a : G) → H) (ball 1 (↑n : ℝ))))
⊢ Bornology.IsBounded
    (HSMul.hSMul (α := H) ((f : (a : G) → H) x : H)
      (HDiv.hDiv (α := Set H)
        ((⇑f : (a : G) → H) ''
          (interior (↑K : Set G) ∩ preimage.{u_1, u_2} (β := H) (⇑f : (a : G) → H) (ball 1 (↑n : ℝ))))
        ((⇑f : (a : G) → H) ''
          (interior (↑K : Set G) ∩ preimage.{u_1, u_2} (β := H) (⇑f : (a : G) → H) (ball 1 (↑n : ℝ))))))

Tactic:
(this.div this).smul _

Premises used: Bornology.IsBounded.div, Bornology.IsBounded.smul
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
inst_6 : MeasurableSpace H
inst_7 : SeminormedGroup H
inst_8 : OpensMeasurableSpace H
f : G →* H
hf : Measurable.{u_1, u_2} (α := G) (β := H) (⇑f : (a : G) → H)
x : G
K : PositiveCompacts G := Classical.arbitrary (PositiveCompacts G)
n : ℕ
hn :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    (((haar : Measure G) : (a : Set G) → ℝ≥0∞)
        (interior (↑K : Set G) ∩ preimage.{u_1, u_2} (β := H) (⇑f : (a : G) → H) (ball 1 (↑n : ℝ))) :
      ℝ≥0∞)
this :
  Bornology.IsBounded.{u_2} (α := H)
    ((⇑f : (a : G) → H) '' (interior (↑K : Set G) ∩ preimage.{u_1, u_2} (β := H) (⇑f : (a : G) → H) (ball 1 (↑n : ℝ))))
⊢ Bornology.IsBounded
    (HSMul.hSMul (α := H) ((f : (a : G) → H) x : H)
      (HDiv.hDiv (α := Set H)
        ((⇑f : (a : G) → H) ''
          (interior (↑K : Set G) ∩ preimage.{u_1, u_2} (β := H) (⇑f : (a : G) → H) (ball 1 (↑n : ℝ))))
        ((⇑f : (a : G) → H) ''
          (interior (↑K : Set G) ∩ preimage.{u_1, u_2} (β := H) (⇑f : (a : G) → H) (ball 1 (↑n : ℝ))))))

Tactic:
exact (this.div this).smul _

Premises used: Bornology.IsBounded.div, Bornology.IsBounded.smul
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
Goal:
G : Type u_1
H : Type u_2
inst : SeminormedAddCommGroup G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : LocallyCompactSpace G
inst_4 : SeminormedAddCommGroup H
inst_5 : MeasurableSpace H
inst_6 : OpensMeasurableSpace H
inst_7 : NormedSpace ℝ H
f : G →+ H
hf : Measurable.{u_1, u_2} (α := G) (β := H) (⇑f : (a : G) → H)
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑f : (a : G) → H)

Tactic:
let ⟨_s, hs, hbdd⟩ := f.exists_nhds_isBounded hf 0; f.continuous_of_isBounded_nhds_zero hs hbdd

Premises used: Continuous, AddMonoidHom.continuous_of_isBounded_nhds_zero, _private.0.MeasureTheory.Measure.AddMonoidHom.continuous_of_measurable.match_1, AddMonoidHom.exists_nhds_isBounded, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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 : ℝ
pos : ∀ (hF : CompleteSpace F), ∫ (x : E), f (R • x) ∂μ = HSMul.hSMul (β := F) |(R ^ finrank ℝ E)⁻¹| (∫ (x : E), f x ∂μ)
neg :
  ∀ (hF : ¬CompleteSpace F), ∫ (x : E), f (R • 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 ∂μ)

Tactic:
by_cases hF : CompleteSpace F

Premises used: CompleteSpace
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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
⊢ ∫ (x : E), f (R • x) ∂μ = HSMul.hSMul (β := F) |(R ^ finrank ℝ E)⁻¹| (∫ (x : E), f x ∂μ)

Tactic:
simp [integral, hF]

Premises used: MeasureTheory.integral
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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
pos :
  ∫ (x : E), f (HSMul.hSMul (α := ℝ) 0 x) ∂μ =
    HSMul.hSMul (β := F) |(HPow.hPow (α := ℝ) 0 (finrank ℝ E))⁻¹| (∫ (x : E), f x ∂μ)
pos₁ : ∀ (hR : R ≠ 0), ∫ (x : E), f (R • 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 ∂μ)

Tactic:
rcases eq_or_ne R 0 with (rfl | hR)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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
pos : μ.real univ • f 0 = HSMul.hSMul (β := F) |(HPow.hPow (α := ℝ) 0 (finrank ℝ E))⁻¹| (∫ (x : E), f x ∂μ)
⊢ ∫ (x : E), f (HSMul.hSMul (α := ℝ) 0 x) ∂μ =
    HSMul.hSMul (β := F) |(HPow.hPow (α := ℝ) 0 (finrank ℝ E))⁻¹| (∫ (x : E), f x ∂μ)

Tactic:
simp only [zero_smul, integral_const]

Premises used: zero_smul, MeasureTheory.integral_const
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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
pos :
  ∀ (hE : finrank ℝ E = 0),
    μ.real univ • f 0 = HSMul.hSMul (β := F) |(HPow.hPow (α := ℝ) 0 (finrank ℝ E))⁻¹| (∫ (x : E), f x ∂μ)
pos₁ :
  ∀ (hE : finrank ℝ E > 0),
    μ.real univ • f 0 = HSMul.hSMul (β := F) |(HPow.hPow (α := ℝ) 0 (finrank ℝ E))⁻¹| (∫ (x : E), f x ∂μ)
⊢ μ.real univ • f 0 = HSMul.hSMul (β := F) |(HPow.hPow (α := ℝ) 0 (finrank ℝ E))⁻¹| (∫ (x : E), f x ∂μ)

Tactic:
rcases Nat.eq_zero_or_pos (finrank ℝ E) with (hE | hE)

Premises used: Real, Nat.eq_zero_or_pos, Module.finrank
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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
⊢ Subsingleton E

Tactic:
have : Subsingleton E := finrank_zero_iff.1 hE
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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
h : ∀ (x : E), f x = f 0
⊢ f = fun (x : E) ↦ f 0

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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
x : E
h h₁ : f 0 = f 0
⊢ f x = f 0

Tactic:
rw [Subsingleton.elim x 0]

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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
⊢ f = fun (x : E) ↦ f 0

Tactic:
have : f = fun _ => f 0 := by ext x; rw [Subsingleton.elim x 0]
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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
rw : HSMul.hSMul (β := F) |(HPow.hPow (α := ℝ) 0 (finrank ℝ E))⁻¹| (∫ (x : E), (fun (x : E) ↦ f 0) x ∂μ)
| HSMul.hSMul (β := F) |(HPow.hPow (α := ℝ) 0 (finrank ℝ E))⁻¹| (∫ (x : E), f x ∂μ)

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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
pos :
  μ.real univ • f 0 =
    HSMul.hSMul (β := F) |(HPow.hPow (α := ℝ) 0 (finrank ℝ E))⁻¹| (∫ (x : E), (fun (x : E) ↦ f 0) x ∂μ)
⊢ μ.real univ • f 0 = HSMul.hSMul (β := F) |(HPow.hPow (α := ℝ) 0 (finrank ℝ E))⁻¹| (∫ (x : E), f x ∂μ)

Tactic:
conv_rhs => rw [this]
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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), (fun (x : E) ↦ f 0) x ∂μ)

Tactic:
simp only [hE, pow_zero, inv_one, abs_one, one_smul, integral_const]

Premises used: inv_one, pow_zero, one_smul, MeasureTheory.integral_const, abs_one
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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
⊢ Nontrivial E

Tactic:
have : Nontrivial E := finrank_pos_iff.1 hE
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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 : Nontrivial E
⊢ μ.real univ • f 0 = HSMul.hSMul (β := F) |(HPow.hPow (α := ℝ) 0 (finrank ℝ E))⁻¹| (∫ (x : E), f x ∂μ)

Tactic:
simp [zero_pow hE.ne', measure_univ_of_isAddLeftInvariant, measureReal_def]

Premises used: MeasureTheory.measure_univ_of_isAddLeftInvariant, LT.lt.ne', MeasureTheory.measureReal_def, zero_pow
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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
⊢ Eq.{u_2 + 1} (α := F) (∫ (x : E), f (R • x) ∂μ)
    (@integral _ _ _ _ inst_2 (map (fun (x : E) ↦ R • x) μ) fun (y : E) ↦ f y)

Tactic:
(integral_map_equiv (Homeomorph.smul (isUnit_iff_ne_zero.2 hR).unit).toMeasurableEquiv
            f).symm

Premises used: Iff.mpr, Homeomorph.smul, MeasureTheory.integral_map_equiv, isUnit_iff_ne_zero, Homeomorph.toMeasurableEquiv, IsUnit.unit, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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
⊢ (@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:
simp only [map_addHaar_smul μ hR, integral_smul_measure, ENNReal.toReal_ofReal, abs_nonneg]

Premises used: ENNReal.toReal_ofReal, MeasureTheory.Measure.map_addHaar_smul, abs_nonneg, MeasureTheory.integral_smul_measure
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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
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 ∂μ)
⊢ ∫ (x : E), f (R • x) ∂μ = 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]

Premises used: Iff.mpr, Real, Homeomorph.smul, MeasureTheory.integral_map_equiv, isUnit_iff_ne_zero, Homeomorph.toMeasurableEquiv, HPow.hPow, MeasureTheory.integral, MeasureTheory.Measure.map, IsUnit.unit, HSMul.hSMul, Eq.symm, Module.finrank
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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 ∂μ)
rw₁ 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 ∂μ)

Tactic:
rw [integral_comp_smul μ f R, abs_of_nonneg (inv_nonneg.2 (pow_nonneg hR _))]

Premises used: Iff.mpr, pow_nonneg, MeasureTheory.Measure.integral_comp_smul, inv_nonneg, abs_of_nonneg
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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 ∂μ)
rw₂ 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 ∂μ)

Tactic:
rw [integral_comp_smul μ f R⁻¹, inv_pow, inv_inv]

Premises used: MeasureTheory.Measure.integral_comp_smul, inv_pow, Inv.inv, inv_inv
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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 ∂μ)
rw₁ 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 ∂μ)

Tactic:
rw [integral_comp_inv_smul μ f R, abs_of_nonneg (pow_nonneg hR _)]

Premises used: MeasureTheory.Measure.integral_comp_inv_smul, pow_nonneg, abs_of_nonneg
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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))
simp : Eq.{u_2 + 1} (α := F) (∫ (x : E) in s, f (R • x) ∂μ) (∫ (x : E) in s, f ((e : (a : E) → E) 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:
simp [← preimage_comp]

Premises used: Set.preimage_comp
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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 s, f ((e : (a : E) → E) x) ∂μ)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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 preimage (β := E) (⇑e : (a : E) → E) ((⇑e.symm : (a : E) → E) ⁻¹' s), f ((e : (a : E) → E) x) ∂μ)
    (@integral _ _ _ _ inst_2 (restrict (map (fun (x : E) ↦ R • x) μ) ((⇑e.symm : (a : E) → E) ⁻¹' s)) fun (y : E) ↦
      f y)

Tactic:
(setIntegral_map_equiv _ _ _).symm

Premises used: MeasureTheory.setIntegral_map_equiv, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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))
⊢ (@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:
simp [map_addHaar_smul μ hR, integral_smul_measure, ENNReal.toReal_ofReal, abs_nonneg]

Premises used: ENNReal.toReal_ofReal, MeasureTheory.Measure.map_addHaar_smul, abs_nonneg, MeasureTheory.integral_smul_measure
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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_a : (⇑e.symm : (a : E) → E) ⁻¹' s = R • s
⊢ 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:
congr 3
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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_a : ∀ (y : E), Membership.mem (γ := Set E) ((⇑e.symm : (a : E) → E) ⁻¹' s) y ↔ y ∈ R • s
⊢ (⇑e.symm : (a : E) → E) ⁻¹' s = R • s

Tactic:
ext y
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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
e_a : Membership.mem (γ := Set E) ((⇑e.symm : (a : E) → E) ⁻¹' s) y ↔ R⁻¹ • y ∈ s
⊢ Membership.mem (γ := Set E) ((⇑e.symm : (a : E) → E) ⁻¹' s) y ↔ y ∈ R • s

Tactic:
rw [mem_smul_set_iff_inv_smul_mem₀ hR]

Premises used: Set.mem_smul_set_iff_inv_smul_mem₀