awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ Membership.mem (γ := Set E) ((⇑e.symm : (a : E) → E) ⁻¹' s) y ↔ R⁻¹ • y ∈ s

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))
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₂ :
  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 ∂μ)
⊢ ∫ (x : E) in s, f (R • x) ∂μ = 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

Premises used: Real, MeasureTheory.setIntegral_map_equiv, MeasurableEquiv.symm, HPow.hPow, MeasureTheory.Measure.map, 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 : ℝ
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 ∂μ)
rw₁ 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 ∂μ)

Tactic:
rw [setIntegral_comp_smul μ f s hR.ne', abs_of_nonneg (inv_nonneg.2 (pow_nonneg hR.le _))]

Premises used: Iff.mpr, pow_nonneg, LT.lt.le, LT.lt.ne', inv_nonneg, MeasureTheory.Measure.setIntegral_comp_smul, abs_of_nonneg
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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)
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)
⊢ (@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]

Premises used: MeasureTheory.Measure.integral_comp_smul, pow_one, Module.finrank_self, smul_eq_mul
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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)
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)
⊢ (@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]

Premises used: MeasureTheory.Measure.integral_comp_inv_smul, pow_one, Module.finrank_self, smul_eq_mul
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
g : ℝ → F
a : ℝ
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ g (x * a)) =
    HSMul.hSMul (β := F) |a⁻¹| (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : ℝ) ↦ g y)

Tactic:
simpa only [mul_comm] using integral_comp_mul_left g a

Premises used: MeasureTheory.Measure.integral_comp_mul_left, mul_comm
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
g : ℝ → F
a : ℝ
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ g (x * a⁻¹)) =
    HSMul.hSMul (β := F) |a| (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : ℝ) ↦ g y)

Tactic:
simpa only [mul_comm] using integral_comp_inv_mul_left g a

Premises used: MeasureTheory.Measure.integral_comp_inv_mul_left, mul_comm
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
g : ℝ → F
a : ℝ
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ g (x / a)) =
    HSMul.hSMul (β := F) |a| (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : ℝ) ↦ g y)

Tactic:
integral_comp_inv_mul_right g a

Premises used: DivInvMonoid.div', MeasureTheory.Measure.integral_comp_inv_mul_right
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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 μ

Tactic:
⟨fun hf => ?_, fun hf => this hf hR⟩

Premises used: Iff.intro
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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)) μ
refine : ∀ (hf : Integrable.{u_1, u_2} (ε := F) (fun (x : E) ↦ f (R • x)) μ), Integrable f μ
⊢ Integrable.{u_1, u_2} (ε := F) (fun (x : E) ↦ f (R • x)) μ ↔ Integrable f μ

Tactic:
refine ⟨fun hf => ?_, fun hf => this hf hR⟩
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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.{u_1, u_2} (ε := F) (fun (x : E) ↦ f (R • R⁻¹ • x)) μ

Tactic:
this hf (inv_ne_zero hR)

Premises used: inv_ne_zero
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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)) μ
h : ∀ (x : E), x = R • R⁻¹ • x
⊢ Integrable f μ

Tactic:
convert! this hf (inv_ne_zero hR)

Premises used: inv_ne_zero
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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)) μ
x : E
h : x = (R * R⁻¹) • x
h₁ : x = HSMul.hSMul (α := ℝ) 1 x
h₂ h₃ : x = x
⊢ x = R • R⁻¹ • x

Tactic:
rw [← mul_smul, mul_inv_cancel₀ hR, one_smul]

Premises used: mul_inv_cancel₀, one_smul, SemigroupAction.mul_smul
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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
E₁ : ∀ {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 μ

Tactic:
suffices
    ∀ {g : E → F} (_ : Integrable g μ) {S : ℝ} (_ : S ≠ 0), Integrable (fun x => g (S • x)) μ by
    refine ⟨fun hf => ?_, fun hf => this hf hR⟩
    convert! this hf (inv_ne_zero hR)
    rw [← mul_smul, mul_inv_cancel₀ hR, one_smul]
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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
g : E → F
hg : Integrable g μ
S : ℝ
hS : S ≠ 0
t : E ≃ᵐ E := Homeomorph.toMeasurableEquiv (Homeomorph.smul ⋯.unit)
⊢ Integrable.{u_1, u_2} (ε := F) (fun (x : E) ↦ g (S • x)) μ

Tactic:
(integrable_map_equiv t g).mp (?_ : Integrable g (map (S • ·) μ))

Premises used: MeasureTheory.integrable_map_equiv, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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
g : E → F
hg : Integrable g μ
S : ℝ
hS : S ≠ 0
t : E ≃ᵐ E := Homeomorph.toMeasurableEquiv (Homeomorph.smul ⋯.unit)
refine : @Integrable _ _ _ _ inst_3 g (Measure.map (fun (x : E) ↦ S • x) μ)
⊢ Integrable.{u_1, u_2} (ε := F) (fun (x : E) ↦ g (S • x)) μ

Tactic:
refine (integrable_map_equiv t g).mp (?_ : Integrable g (map (S • ·) μ))

Premises used: MeasureTheory.integrable_map_equiv, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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
g : E → F
hg : Integrable g μ
S : ℝ
hS : S ≠ 0
t : E ≃ᵐ E := Homeomorph.toMeasurableEquiv (Homeomorph.smul ⋯.unit)
rwa : ENNReal.ofReal |(S ^ finrank ℝ E)⁻¹| ≠ 0
⊢ @Integrable _ _ _ _ inst_3 g (Measure.map (fun (x : E) ↦ S • x) μ)

Tactic:
rwa [map_addHaar_smul μ hS, integrable_smul_measure _ ENNReal.ofReal_ne_top]

Premises used: MeasureTheory.integrable_smul_measure, MeasureTheory.Measure.map_addHaar_smul, ENNReal.ofReal_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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
g : E → F
hg : Integrable g μ
S : ℝ
hS : S ≠ 0
t : E ≃ᵐ E := Homeomorph.toMeasurableEquiv (Homeomorph.smul ⋯.unit)
⊢ ENNReal.ofReal |(S ^ finrank ℝ E)⁻¹| ≠ 0

Tactic:
simpa only [Ne, ENNReal.ofReal_eq_zero, not_le, abs_pos] using inv_ne_zero (pow_ne_zero _ hS)

Premises used: not_le, ENNReal.ofReal_eq_zero, pow_ne_zero, Ne, abs_pos, inv_ne_zero
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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
hf : Integrable f μ
R : ℝ
hR : R ≠ 0
⊢ Integrable.{u_1, u_2} (ε := F) (fun (x : E) ↦ f (R • x)) μ

Tactic:
(integrable_comp_smul_iff μ f hR).2 hf

Premises used: Iff.mpr, MeasureTheory.integrable_comp_smul_iff
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
Goal:
F : Type u_1
inst : NormedAddCommGroup F
g : ℝ → F
R : ℝ
hR : R ≠ 0
⊢ @Integrable.{u_1, 0} F _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ g (R * x)) volume ↔
    @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume

Tactic:
simpa only [smul_eq_mul] using integrable_comp_smul_iff volume g hR

Premises used: MeasureTheory.MeasureSpace.volume, MeasureTheory.integrable_comp_smul_iff, smul_eq_mul
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
Goal:
F : Type u_1
inst : NormedAddCommGroup F
g : ℝ → F
hg : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume
R : ℝ
hR : R ≠ 0
⊢ @Integrable.{u_1, 0} F _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ g (R * x)) volume

Tactic:
(integrable_comp_mul_left_iff g hR).2 hg

Premises used: Iff.mpr, MeasureTheory.integrable_comp_mul_left_iff
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
Goal:
F : Type u_1
inst : NormedAddCommGroup F
g : ℝ → F
R : ℝ
hR : R ≠ 0
⊢ @Integrable.{u_1, 0} F _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ g (x * R)) volume ↔
    @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume

Tactic:
simpa only [mul_comm] using integrable_comp_mul_left_iff g hR

Premises used: MeasureTheory.integrable_comp_mul_left_iff, mul_comm
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
Goal:
F : Type u_1
inst : NormedAddCommGroup F
g : ℝ → F
hg : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume
R : ℝ
hR : R ≠ 0
⊢ @Integrable.{u_1, 0} F _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ g (x * R)) volume

Tactic:
(integrable_comp_mul_right_iff g hR).2 hg

Premises used: Iff.mpr, MeasureTheory.integrable_comp_mul_right_iff
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
Goal:
F : Type u_1
inst : NormedAddCommGroup F
g : ℝ → F
R : ℝ
hR : R ≠ 0
⊢ @Integrable.{u_1, 0} F _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ g (x / R)) volume ↔
    @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume

Tactic:
integrable_comp_mul_right_iff g (inv_ne_zero hR)

Premises used: DivInvMonoid.div', MeasureTheory.integrable_comp_mul_right_iff, inv_ne_zero
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
Goal:
F : Type u_1
inst : NormedAddCommGroup F
g : ℝ → F
hg : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume
R : ℝ
hR : R ≠ 0
⊢ @Integrable.{u_1, 0} F _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ g (x / R)) volume

Tactic:
(integrable_comp_div_iff g hR).2 hg

Premises used: Iff.mpr, MeasureTheory.integrable_comp_div_iff
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
Goal:
E' : Type u_2
F' : Type u_3
A : Type u_4
inst : NormedAddCommGroup E'
inst_1 : InnerProductSpace ℝ E'
inst_2 : FiniteDimensional ℝ E'
inst_3 : MeasurableSpace E'
inst_4 : BorelSpace E'
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : FiniteDimensional ℝ F'
inst_8 : MeasurableSpace F'
inst_9 : BorelSpace F'
f : E' ≃ₗᵢ[ℝ] F'
inst_10 : NormedAddCommGroup A
g : F' → A
⊢ @Integrable.{u_4, u_2} _ _ _ E' MeasureSpace.toMeasurableSpace (g ∘ (⇑f : (a : E') → F')) volume ↔
    @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume

Tactic:
f.measurePreserving.integrable_comp_emb f.toMeasurableEquiv.measurableEmbedding

Premises used: MeasurableEquiv.measurableEmbedding, LinearIsometryEquiv.measurePreserving, MeasureTheory.MeasurePreserving.integrable_comp_emb, LinearIsometryEquiv.toMeasurableEquiv
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
Goal:
E' : Type u_2
F' : Type u_3
A : Type u_4
inst : NormedAddCommGroup E'
inst_1 : InnerProductSpace ℝ E'
inst_2 : FiniteDimensional ℝ E'
inst_3 : MeasurableSpace E'
inst_4 : BorelSpace E'
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : FiniteDimensional ℝ F'
inst_8 : MeasurableSpace F'
inst_9 : BorelSpace F'
f : E' ≃ₗᵢ[ℝ] F'
inst_10 : NormedAddCommGroup A
inst_11 : NormedSpace ℝ A
g : F' → A
⊢ Eq.{u_4 + 1} (α := A)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E') ↦ g ((f : (a : E') → F') x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : F') ↦ g y)

Tactic:
f.measurePreserving.integral_comp' (f := f.toMeasurableEquiv) g

Premises used: LinearIsometryEquiv.measurePreserving, MeasureTheory.MeasurePreserving.integral_comp'
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
E : Type u_3
inst : Fintype ι
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
v : ι → E
x : E
⊢ x ∈ parallelepiped v ↔ ∃ (t : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) (Icc 0 1) t ∧ x = ∑ i : ι, t i • v i

Tactic:
simp [parallelepiped, eq_comm]

Premises used: eq_comm, parallelepiped
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
E : Type u_3
inst : Fintype ι
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
b : Basis ι ℝ E
h :
  ∀ (x : E),
    Membership.mem (γ := Set E) (parallelepiped.{u_1, u_3} (ι := ι) (⇑b : (a : ι) → E)) x ↔
      Membership.mem (γ := Set E)
        {x : E |
          ∀ (i : ι),
            Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
              ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ)}
        x
⊢ Eq.{u_3 + 1} (α := Set E) (parallelepiped.{u_1, u_3} (ι := ι) (⇑b : (a : ι) → E))
    {x : E |
      ∀ (i : ι),
        Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ)}

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
E : Type u_3
inst : Fintype ι
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
b : Basis ι ℝ E
x : E
h :
  (∃ (t : ι → ℝ),
      ∀ (x_1 : ι), (0 ≤ t x_1 ∧ t x_1 ≤ 1) ∧ (((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) x_1 = t x_1) ↔
    ∀ (i : ι),
      LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) ∧
        LE.le (α := ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) (1 : ℝ)
⊢ Membership.mem (γ := Set E) (parallelepiped.{u_1, u_3} (ι := ι) (⇑b : (a : ι) → E)) x ↔
    Membership.mem (γ := Set E)
      {x : E |
        ∀ (i : ι),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
            ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ)}
      x

Tactic:
simp_rw [mem_parallelepiped_iff, mem_setOf_eq, b.ext_elem_iff, _root_.map_sum,
    map_smul, Finset.sum_apply', Basis.repr_self, Finsupp.smul_single, smul_eq_mul,
    mul_one, Finsupp.single_apply, Finset.sum_ite_eq', Finset.mem_univ, ite_true, mem_Icc,
    Pi.le_def, Pi.zero_apply, Pi.one_apply, ← forall_and]

Premises used: Finset.mem_univ, Finset.sum_ite_eq', Pi.one_apply, Finset.sum_apply', Pi.zero_apply, Set.mem_setOf_eq, ite_true, map_sum, mem_parallelepiped_iff, Set.mem_Icc, Module.Basis.ext_elem_iff, Finsupp.single_apply, smul_eq_mul, Pi.le_def, mul_one, Finsupp.smul_single, Module.Basis.repr_self, forall_and, map_smul
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
E : Type u_3
inst : Fintype ι
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
b : Basis ι ℝ E
x : E
⊢ (∃ (t : ι → ℝ),
      ∀ (x_1 : ι), (0 ≤ t x_1 ∧ t x_1 ≤ 1) ∧ (((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) x_1 = t x_1) ↔
    ∀ (i : ι),
      LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) ∧
        LE.le (α := ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) (1 : ℝ)

Tactic:
aesop
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
E : Type u_3
inst : Fintype ι
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
b : Basis ι ℝ E
h :
  ∀ (x : E),
    Membership.mem (γ := Set E) (parallelepiped.{u_1, u_3} (ι := ι) (⇑b : (a : ι) → E)) x ↔
      Membership.mem (γ := Set E)
        {x : E |
          ∀ (i : ι),
            Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
              ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ)}
        x
h₁ :
  ∀ (x : E),
    (∃ (t : ι → ℝ),
        ∀ (x_1 : ι), (0 ≤ t x_1 ∧ t x_1 ≤ 1) ∧ (((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) x_1 = t x_1) ↔
      ∀ (i : ι),
        LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) ∧
          LE.le (α := ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) (1 : ℝ)
⊢ Eq.{u_3 + 1} (α := Set E) (parallelepiped.{u_1, u_3} (ι := ι) (⇑b : (a : ι) → E))
    {x : E |
      ∀ (i : ι),
        Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ)}

Tactic:
classical
  ext x
  simp_rw [mem_parallelepiped_iff, mem_setOf_eq, b.ext_elem_iff, _root_.map_sum,
    map_smul, Finset.sum_apply', Basis.repr_self, Finsupp.smul_single, smul_eq_mul,
    mul_one, Finsupp.single_apply, Finset.sum_ite_eq', Finset.mem_univ, ite_true, mem_Icc,
    Pi.le_def, Pi.zero_apply, Pi.one_apply, ← forall_and]
  aesop

Premises used: Finset.mem_univ, Finset.sum_ite_eq', Pi.one_apply, Finset.sum_apply', Pi.zero_apply, Set.mem_setOf_eq, ite_true, map_sum, mem_parallelepiped_iff, Set.mem_Icc, Module.Basis.ext_elem_iff, Finsupp.single_apply, smul_eq_mul, Pi.le_def, mul_one, Finsupp.smul_single, Module.Basis.repr_self, forall_and, map_smul
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
E : Type u_3
F : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
inst_3 : AddCommGroup F
inst_4 : Module ℝ F
f : E →ₗ[ℝ] F
v : ι → E
simp :
  Eq.{u_4 + 1} (α := Set F)
    (image.{u_1, u_4} (α := ι → ℝ)
      (Function.comp.{u_1 + 1, u_3 + 1, u_4 + 1} (β := E) (⇑f : (a : E) → F) fun (t : ι → ℝ) ↦ ∑ i : ι, t i • v i)
      (Icc 0 1))
    ((fun (t : ι → ℝ) ↦ ∑ i : ι, HSMul.hSMul (β := F) (t i) (((⇑f : (a : E) → F) ∘ v) i)) '' Icc 0 1)
⊢ Eq.{u_4 + 1} (α := Set F) ((⇑f : (a : E) → F) '' parallelepiped v) (parallelepiped ((⇑f : (a : E) → F) ∘ v))

Tactic:
simp only [parallelepiped, ← image_comp]

Premises used: Set.image_comp, parallelepiped