awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C D : ℝ≥0
f g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : LipschitzWith D g
h'g : HasCompactSupport g
v : E
A :
  Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
B :
  Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ))
t : ℝ
S3 : Eq (α := ℝ) (∫ (x : E), f (x + t • v) * g x ∂μ) (∫ (x : E), f x * g (x + t • -v) ∂μ)
hf₁ : Integrable (ε := ℝ) (fun (x : E) ↦ f x * g (x + t • -v)) μ
hg₁ : Integrable (ε := ℝ) (fun (x : E) ↦ f x * g x) μ
hf₂ : Integrable (ε := ℝ) (fun (x : E) ↦ f (x + t • v) * g x) μ
hg₂ : Integrable (ε := ℝ) (fun (x : E) ↦ f x * g x) μ
⊢ Eq (α := ℝ) (∫ (x : E), f (x + t • v) * g x - f x * g x ∂μ) (∫ (x : E), f x * g (x + t • -v) - f x * g x ∂μ)

Tactic:
rw [integral_sub, integral_sub, S3]

Premises used: MeasureTheory.integral_sub
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C D : ℝ≥0
f g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : LipschitzWith D g
h'g : HasCompactSupport g
v : E
A :
  Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
B :
  Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ))
t : ℝ
S3 : Eq (α := ℝ) (∫ (x : E), f (x + t • v) * g x ∂μ) (∫ (x : E), f x * g (x + t • -v) ∂μ)
hf₁ : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : E) ↦ f x * g (x + t • -v)
hf₂ : HasCompactSupport (β := ℝ) fun (x : E) ↦ f x * g (x + t • -v)
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ f x * g (x + t • -v)) μ

Tactic:
apply Continuous.integrable_of_hasCompactSupport

Premises used: Continuous.integrable_of_hasCompactSupport
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C D : ℝ≥0
f g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : LipschitzWith D g
h'g : HasCompactSupport g
v : E
A :
  Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
B :
  Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ))
t : ℝ
S3 : Eq (α := ℝ) (∫ (x : E), f (x + t • v) * g x ∂μ) (∫ (x : E), f x * g (x + t • -v) ∂μ)
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : E) ↦ f x * g (x + t • -v)

Tactic:
hf.continuous.mul (hg.continuous.comp (continuous_add_const _))

Premises used: Continuous.comp, continuous_add_const, Continuous.mul, LipschitzWith.continuous
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C D : ℝ≥0
f g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : LipschitzWith D g
h'g : HasCompactSupport g
v : E
A :
  Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
B :
  Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ))
t : ℝ
S3 : Eq (α := ℝ) (∫ (x : E), f (x + t • v) * g x ∂μ) (∫ (x : E), f x * g (x + t • -v) ∂μ)
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : E) ↦ f x * g (x + t • -v)

Tactic:
exact hf.continuous.mul (hg.continuous.comp (continuous_add_const _))

Premises used: Continuous.comp, continuous_add_const, Continuous.mul, LipschitzWith.continuous
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C D : ℝ≥0
f g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : LipschitzWith D g
h'g : HasCompactSupport g
v : E
A :
  Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
B :
  Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ))
t : ℝ
S3 : Eq (α := ℝ) (∫ (x : E), f (x + t • v) * g x ∂μ) (∫ (x : E), f x * g (x + t • -v) ∂μ)
⊢ HasCompactSupport (β := ℝ) fun (x : E) ↦ f x * g (x + t • -v)

Tactic:
(h'g.comp_homeomorph (Homeomorph.addRight (t • (-v)))).mul_left

Premises used: HasCompactSupport.comp_homeomorph, HasCompactSupport.mul_left, Homeomorph.addRight, HSMul.hSMul, Neg.neg
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C D : ℝ≥0
f g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : LipschitzWith D g
h'g : HasCompactSupport g
v : E
A :
  Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
B :
  Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ))
t : ℝ
S3 : Eq (α := ℝ) (∫ (x : E), f (x + t • v) * g x ∂μ) (∫ (x : E), f x * g (x + t • -v) ∂μ)
⊢ HasCompactSupport (β := ℝ) fun (x : E) ↦ f x * g (x + t • -v)

Tactic:
exact (h'g.comp_homeomorph (Homeomorph.addRight (t • (-v)))).mul_left

Premises used: HasCompactSupport.comp_homeomorph, HasCompactSupport.mul_left, Homeomorph.addRight, HSMul.hSMul, Neg.neg
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C D : ℝ≥0
f g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : LipschitzWith D g
h'g : HasCompactSupport g
v : E
A :
  Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
B :
  Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ))
t : ℝ
S3 : Eq (α := ℝ) (∫ (x : E), f (x + t • v) * g x ∂μ) (∫ (x : E), f x * g (x + t • -v) ∂μ)
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ f x * g x) μ

Tactic:
(hf.continuous.mul hg.continuous).integrable_of_hasCompactSupport h'g.mul_left

Premises used: Continuous.integrable_of_hasCompactSupport, Continuous.mul, LipschitzWith.continuous, HasCompactSupport.mul_left
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C D : ℝ≥0
f g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : LipschitzWith D g
h'g : HasCompactSupport g
v : E
A :
  Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
B :
  Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ))
t : ℝ
S3 : Eq (α := ℝ) (∫ (x : E), f (x + t • v) * g x ∂μ) (∫ (x : E), f x * g (x + t • -v) ∂μ)
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ f x * g x) μ

Tactic:
exact (hf.continuous.mul hg.continuous).integrable_of_hasCompactSupport h'g.mul_left

Premises used: Continuous.integrable_of_hasCompactSupport, Continuous.mul, LipschitzWith.continuous, HasCompactSupport.mul_left
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C D : ℝ≥0
f g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : LipschitzWith D g
h'g : HasCompactSupport g
v : E
A :
  Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
B :
  Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ))
t : ℝ
S3 : Eq (α := ℝ) (∫ (x : E), f (x + t • v) * g x ∂μ) (∫ (x : E), f x * g (x + t • -v) ∂μ)
hf₁ : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : E) ↦ f (x + t • v) * g x
hf₂ : HasCompactSupport (β := ℝ) fun (x : E) ↦ f (x + t • v) * g x
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ f (x + t • v) * g x) μ

Tactic:
apply Continuous.integrable_of_hasCompactSupport

Premises used: Continuous.integrable_of_hasCompactSupport
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C D : ℝ≥0
f g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : LipschitzWith D g
h'g : HasCompactSupport g
v : E
A :
  Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
B :
  Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ))
t : ℝ
S3 : Eq (α := ℝ) (∫ (x : E), f (x + t • v) * g x ∂μ) (∫ (x : E), f x * g (x + t • -v) ∂μ)
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : E) ↦ f (x + t • v) * g x

Tactic:
(hf.continuous.comp (continuous_add_const _)).mul hg.continuous

Premises used: Continuous.comp, continuous_add_const, Continuous.mul, LipschitzWith.continuous
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C D : ℝ≥0
f g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : LipschitzWith D g
h'g : HasCompactSupport g
v : E
A :
  Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
B :
  Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ))
t : ℝ
S3 : Eq (α := ℝ) (∫ (x : E), f (x + t • v) * g x ∂μ) (∫ (x : E), f x * g (x + t • -v) ∂μ)
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : E) ↦ f (x + t • v) * g x

Tactic:
exact (hf.continuous.comp (continuous_add_const _)).mul hg.continuous

Premises used: Continuous.comp, continuous_add_const, Continuous.mul, LipschitzWith.continuous
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C D : ℝ≥0
f g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : LipschitzWith D g
h'g : HasCompactSupport g
v : E
A :
  Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
B :
  Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ))
t : ℝ
S3 : Eq (α := ℝ) (∫ (x : E), f (x + t • v) * g x ∂μ) (∫ (x : E), f x * g (x + t • -v) ∂μ)
⊢ HasCompactSupport (β := ℝ) fun (x : E) ↦ f (x + t • v) * g x

Tactic:
h'g.mul_left

Premises used: HasCompactSupport.mul_left
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C D : ℝ≥0
f g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : LipschitzWith D g
h'g : HasCompactSupport g
v : E
A :
  Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
B :
  Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ))
t : ℝ
S3 : Eq (α := ℝ) (∫ (x : E), f (x + t • v) * g x ∂μ) (∫ (x : E), f x * g (x + t • -v) ∂μ)
⊢ HasCompactSupport (β := ℝ) fun (x : E) ↦ f (x + t • v) * g x

Tactic:
exact h'g.mul_left

Premises used: HasCompactSupport.mul_left
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
ι : Type u_3
s : Finset ι
a : ι → ℝ
v : ι → E
apply :
  ∀ (g : E → ℝ) (g_smooth : ContDiff ℝ (↑⊤ : WithTop ℕ∞) g) (g_comp : HasCompactSupport g),
    Eq (α := ℝ) (∫ (x : E), g x • lineDeriv ℝ f x (∑ i ∈ s, a i • v i) ∂μ)
      (∫ (x : E),
        HSMul.hSMul (β := ℝ) (g x) (∑ i ∈ s, HSMul.hSMul (β := E → ℝ) (a i) (fun (x : E) ↦ lineDeriv ℝ f x (v i)) x) ∂μ)
⊢ ∀ᵐ (x : E) ∂μ, lineDeriv ℝ f x (∑ i ∈ s, a i • v i) = ∑ i ∈ s, a i • lineDeriv ℝ f x (v i)

Tactic:
apply ae_eq_of_integral_contDiff_smul_eq (hf.locallyIntegrable_lineDeriv _)
    (locallyIntegrable_finsetSum _ (fun i hi ↦ (hf.locallyIntegrable_lineDeriv (v i)).smul (a i)))
    (fun g g_smooth g_comp ↦ ?_)

Premises used: MeasureTheory.locallyIntegrable_finsetSum, LipschitzWith.locallyIntegrable_lineDeriv, MeasureTheory.LocallyIntegrable.smul, ae_eq_of_integral_contDiff_smul_eq
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
ι : Type u_3
s : Finset ι
a : ι → ℝ
v : ι → E
g : E → ℝ
g_smooth : ContDiff ℝ (↑⊤ : WithTop ℕ∞) g
g_comp : HasCompactSupport g
simp_rw :
  Eq (α := ℝ) (∫ (x : E), g x • lineDeriv ℝ f x (∑ i ∈ s, a i • v i) ∂μ)
    (∫ (x : E), ∑ x_1 ∈ s, g x • HSMul.hSMul (β := E → ℝ) (a x_1) (fun (x : E) ↦ lineDeriv ℝ f x (v x_1)) x ∂μ)
⊢ Eq (α := ℝ) (∫ (x : E), g x • lineDeriv ℝ f x (∑ i ∈ s, a i • v i) ∂μ)
    (∫ (x : E),
      HSMul.hSMul (β := ℝ) (g x) (∑ i ∈ s, HSMul.hSMul (β := E → ℝ) (a i) (fun (x : E) ↦ lineDeriv ℝ f x (v i)) x) ∂μ)

Tactic:
simp_rw [Finset.smul_sum]

Premises used: Finset.smul_sum
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
ι : Type u_3
s : Finset ι
a : ι → ℝ
v : ι → E
g : E → ℝ
g_smooth : ContDiff ℝ (↑⊤ : WithTop ℕ∞) g
g_comp : HasCompactSupport g
⊢ ∀ i ∈ s,
    Integrable (ε := ℝ)
      (fun (x : E) ↦ g x • HSMul.hSMul (β := (x : E) → ℝ) (a i) (fun (x : E) ↦ lineDeriv ℝ f x (v i)) x) μ

Tactic:
have A : ∀ i ∈ s, Integrable (fun x ↦ g x • (a i • fun x ↦ lineDeriv ℝ f x (v i)) x) μ :=
    fun i hi ↦ (g_smooth.continuous.integrable_of_hasCompactSupport g_comp).smul_of_top_left
      ((hf.memLp_lineDeriv (v i)).const_smul (a i))
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
ι : Type u_3
s : Finset ι
a : ι → ℝ
v : ι → E
g : E → ℝ
g_smooth : ContDiff ℝ (↑⊤ : WithTop ℕ∞) g
g_comp : HasCompactSupport g
A :
  ∀ i ∈ s,
    Integrable (ε := ℝ)
      (fun (x : E) ↦ g x • HSMul.hSMul (β := (x : E) → ℝ) (a i) (fun (x : E) ↦ lineDeriv ℝ f x (v i)) x) μ
rw :
  Eq (α := ℝ) (∫ (x : E), g x • lineDeriv ℝ f x (∑ i ∈ s, a i • v i) ∂μ)
    (∑ i ∈ s, ∫ (a_1 : E), g a_1 • HSMul.hSMul (β := (x : E) → ℝ) (a i) (fun (x : E) ↦ lineDeriv ℝ f x (v i)) a_1 ∂μ)
⊢ Eq (α := ℝ) (∫ (x : E), g x • lineDeriv ℝ f x (∑ i ∈ s, a i • v i) ∂μ)
    (∫ (x : E), ∑ x_1 ∈ s, g x • HSMul.hSMul (β := E → ℝ) (a x_1) (fun (x : E) ↦ lineDeriv ℝ f x (v x_1)) x ∂μ)

Tactic:
rw [integral_finsetSum _ A]

Premises used: MeasureTheory.integral_finsetSum
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
ι : Type u_3
s : Finset ι
a : ι → ℝ
v : ι → E
g : E → ℝ
g_smooth : ContDiff ℝ (↑⊤ : WithTop ℕ∞) g
g_comp : HasCompactSupport g
A :
  ∀ i ∈ s,
    Integrable (ε := ℝ)
      (fun (x : E) ↦ g x • HSMul.hSMul (β := (x : E) → ℝ) (a i) (fun (x : E) ↦ lineDeriv ℝ f x (v i)) x) μ
S1 :
  Eq (α := ℝ) (∫ (x : E), lineDeriv ℝ f x (∑ i ∈ s, a i • v i) * g x ∂μ)
    (∑ i ∈ s, a i * ∫ (x : E), lineDeriv ℝ f x (v i) * g x ∂μ)
simp_rw :
  Eq (α := ℝ) (∫ (x : E), g x * lineDeriv ℝ f x (∑ i ∈ s, a i • v i) ∂μ)
    (∑ x ∈ s, ∫ (a_1 : E), g a_1 * a x * lineDeriv ℝ f a_1 (v x) ∂μ)
simp_rw₁ :
  Eq (α := ℝ) (∫ (x : E), g x * lineDeriv ℝ f x (∑ i ∈ s, a i • v i) ∂μ)
    (∑ x ∈ s, ∫ (a_1 : E), a x * g a_1 * lineDeriv ℝ f a_1 (v x) ∂μ)
simp_rw₂ :
  Eq (α := ℝ) (∫ (x : E), g x * lineDeriv ℝ f x (∑ i ∈ s, a i • v i) ∂μ)
    (∑ x ∈ s, ∫ (a_1 : E), a x * (g a_1 * lineDeriv ℝ f a_1 (v x)) ∂μ)
simp_rw₃ :
  Eq (α := ℝ) (∫ (x : E), g x * lineDeriv ℝ f x (∑ i ∈ s, a i • v i) ∂μ)
    (∑ x ∈ s, a x * ∫ (a : E), g a * lineDeriv ℝ f a (v x) ∂μ)
simp_rw₄ :
  Eq (α := ℝ) (∫ (x : E), lineDeriv ℝ f x (∑ i ∈ s, a i • v i) * g x ∂μ)
    (∑ x ∈ s, a x * ∫ (a : E), lineDeriv ℝ f a (v x) * g a ∂μ)
⊢ Eq (α := ℝ) (∫ (x : E), g x * lineDeriv ℝ f x (∑ i ∈ s, a i • v i) ∂μ)
    (∑ i ∈ s, ∫ (a_1 : E), g a_1 * (a i * lineDeriv ℝ f a_1 (v i)) ∂μ)

Tactic:
simp_rw [← mul_assoc, mul_comm _ (a _), mul_assoc, integral_const_mul, mul_comm (g _), S1]

Premises used: MeasureTheory.integral_const_mul, mul_assoc, mul_comm
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
ι : Type u_3
s : Finset ι
a : ι → ℝ
v : ι → E
g : E → ℝ
g_smooth : ContDiff ℝ (↑⊤ : WithTop ℕ∞) g
g_comp : HasCompactSupport g
A :
  ∀ i ∈ s,
    Integrable (ε := ℝ)
      (fun (x : E) ↦ g x • HSMul.hSMul (β := (x : E) → ℝ) (a i) (fun (x : E) ↦ lineDeriv ℝ f x (v i)) x) μ
suffices :
  Eq (α := ℝ) (∫ (x : E), lineDeriv ℝ f x (∑ i ∈ s, a i • v i) * g x ∂μ)
    (∑ i ∈ s, a i * ∫ (x : E), lineDeriv ℝ f x (v i) * g x ∂μ)
⊢ Eq (α := ℝ) (∫ (x : E), g x • lineDeriv ℝ f x (∑ i ∈ s, a i • v i) ∂μ)
    (∑ i ∈ s, ∫ (a_1 : E), g a_1 • HSMul.hSMul (β := (x : E) → ℝ) (a i) (fun (x : E) ↦ lineDeriv ℝ f x (v i)) a_1 ∂μ)

Tactic:
suffices S1 : ∫ x, lineDeriv ℝ f x (∑ i ∈ s, a i • v i) * g x ∂μ
      = ∑ i ∈ s, a i * ∫ x, lineDeriv ℝ f x (v i) * g x ∂μ by
    dsimp only [smul_eq_mul, Pi.smul_apply]
    simp_rw [← mul_assoc, mul_comm _ (a _), mul_assoc, integral_const_mul, mul_comm (g _), S1]
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
ι : Type u_3
s : Finset ι
a : ι → ℝ
v : ι → E
g : E → ℝ
g_smooth : ContDiff ℝ (↑⊤ : WithTop ℕ∞) g
g_comp : HasCompactSupport g
A :
  ∀ i ∈ s,
    Integrable (ε := ℝ)
      (fun (x : E) ↦ g x • HSMul.hSMul (β := (x : E) → ℝ) (a i) (fun (x : E) ↦ lineDeriv ℝ f x (v i)) x) μ
S2 :
  Eq (α := ℝ) (∫ (x : E), (∑ i ∈ s, HMul.hMul (β := ℝ) (a i) ((fderiv ℝ g x : (a : E) → ℝ) (v i) : ℝ)) * f x ∂μ)
    (∑ i ∈ s, a i * ∫ (x : E), HMul.hMul (α := ℝ) ((fderiv ℝ g x : (a : E) → ℝ) (v i) : ℝ) (f x) ∂μ)
⊢ Ne (α := WithTop ℕ∞) (↑⊤ : WithTop ℕ∞) 0

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
ι : Type u_3
s : Finset ι
a : ι → ℝ
v : ι → E
g : E → ℝ
g_smooth : ContDiff ℝ (↑⊤ : WithTop ℕ∞) g
g_comp : HasCompactSupport g
A :
  ∀ i ∈ s,
    Integrable (ε := ℝ)
      (fun (x : E) ↦ g x • HSMul.hSMul (β := (x : E) → ℝ) (a i) (fun (x : E) ↦ lineDeriv ℝ f x (v i)) x) μ
S2 :
  Eq (α := ℝ) (∫ (x : E), (∑ i ∈ s, HMul.hMul (β := ℝ) (a i) ((fderiv ℝ g x : (a : E) → ℝ) (v i) : ℝ)) * f x ∂μ)
    (∑ i ∈ s, a i * ∫ (x : E), HMul.hMul (α := ℝ) ((fderiv ℝ g x : (a : E) → ℝ) (v i) : ℝ) (f x) ∂μ)
obtain :
  ∀ (D : ℝ≥0) (g_lip : LipschitzWith D g),
    Eq (α := ℝ) (∫ (x : E), lineDeriv ℝ f x (∑ i ∈ s, a i • v i) * g x ∂μ)
      (∑ i ∈ s, a i * ∫ (x : E), lineDeriv ℝ f x (v i) * g x ∂μ)
⊢ Eq (α := ℝ) (∫ (x : E), lineDeriv ℝ f x (∑ i ∈ s, a i • v i) * g x ∂μ)
    (∑ i ∈ s, a i * ∫ (x : E), lineDeriv ℝ f x (v i) * g x ∂μ)

Tactic:
obtain ⟨D, g_lip⟩ : ∃ D, LipschitzWith D g :=
      ContDiff.lipschitzWith_of_hasCompactSupport g_comp g_smooth (by simp)

Premises used: ContDiff.lipschitzWith_of_hasCompactSupport
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
ι : Type u_3
s : Finset ι
a : ι → ℝ
v : ι → E
g : E → ℝ
g_smooth : ContDiff ℝ (↑⊤ : WithTop ℕ∞) g
g_comp : HasCompactSupport g
A :
  ∀ i ∈ s,
    Integrable (ε := ℝ)
      (fun (x : E) ↦ g x • HSMul.hSMul (β := (x : E) → ℝ) (a i) (fun (x : E) ↦ lineDeriv ℝ f x (v i)) x) μ
S2 :
  Eq (α := ℝ) (∫ (x : E), (∑ i ∈ s, HMul.hMul (β := ℝ) (a i) ((fderiv ℝ g x : (a : E) → ℝ) (v i) : ℝ)) * f x ∂μ)
    (∑ i ∈ s, a i * ∫ (x : E), HMul.hMul (α := ℝ) ((fderiv ℝ g x : (a : E) → ℝ) (v i) : ℝ) (f x) ∂μ)
D : ℝ≥0
g_lip : LipschitzWith D g
simp_rw :
  Eq (α := ℝ) (∫ (x : E), lineDeriv ℝ g x (-∑ i ∈ s, a i • v i) * f x ∂μ)
    (∑ x ∈ s, a x * ∫ (x_1 : E), lineDeriv ℝ g x_1 (-v x) * f x_1 ∂μ)
⊢ Eq (α := ℝ) (∫ (x : E), lineDeriv ℝ f x (∑ i ∈ s, a i • v i) * g x ∂μ)
    (∑ i ∈ s, a i * ∫ (x : E), lineDeriv ℝ f x (v i) * g x ∂μ)

Tactic:
simp_rw [integral_lineDeriv_mul_eq hf g_lip g_comp]

Premises used: LipschitzWith.integral_lineDeriv_mul_eq
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
ι : Type u_3
s : Finset ι
a : ι → ℝ
v : ι → E
g : E → ℝ
g_smooth : ContDiff ℝ (↑⊤ : WithTop ℕ∞) g
g_comp : HasCompactSupport g
A :
  ∀ i ∈ s,
    Integrable (ε := ℝ)
      (fun (x : E) ↦ g x • HSMul.hSMul (β := (x : E) → ℝ) (a i) (fun (x : E) ↦ lineDeriv ℝ f x (v i)) x) μ
S2 :
  Eq (α := ℝ) (∫ (x : E), (∑ i ∈ s, HMul.hMul (β := ℝ) (a i) ((fderiv ℝ g x : (a : E) → ℝ) (v i) : ℝ)) * f x ∂μ)
    (∑ i ∈ s, a i * ∫ (x : E), HMul.hMul (α := ℝ) ((fderiv ℝ g x : (a : E) → ℝ) (v i) : ℝ) (f x) ∂μ)
D : ℝ≥0
g_lip : LipschitzWith D g
⊢ Ne (α := WithTop ℕ∞) (↑⊤ : WithTop ℕ∞) 0

Tactic:
simp