awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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 : ℝ
⊢ Eq (α := ℝ) (∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ)
have suffices : Eq (α := ℝ) (∫ (x : E), (f (x + t • v) - f x) * g x ∂μ) (∫ (x : E), f x * (g (x + t • -v) - g x) ∂μ)
Tactic: suffices S2 : ∫ x, (f (x + t • v) - f x) * g x ∂μ = ∫ x, f x * (g (x + t • (-v)) - g x) ∂μ by
    simp only [smul_eq_mul, mul_assoc, integral_const_mul, S2, mul_comm (f _)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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 : ℝ
⊢ Eq (α := ℝ) (∫ (x : E), f (x + t • v) * g x ∂μ) (∫ (x : E), f x * g (x + t • -v) ∂μ)
have rw : Eq (α := ℝ) (∫ (x : E), f (x + t • -v + t • v) * g (x + t • -v) ∂μ) (∫ (x : E), f x * g (x + t • -v) ∂μ)
Tactic: rw [← integral_add_right_eq_self _ (t • (-v))]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (hypothesis)
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 : ℝ
⊢ Eq (α := ℝ) (∫ (x : E), (f (x + t • v) - f x) * g x ∂μ) (∫ (x : E), f x * (g (x + t • -v) - g x) ∂μ)
have S3 : Eq (α := ℝ) (∫ (x : E), f (x + t • v) * g x ∂μ) (∫ (x : E), f x * g (x + t • -v) ∂μ)
Tactic: have S3 : ∫ x, f (x + t • v) * g x ∂μ = ∫ x, f x * g (x + t • (-v)) ∂μ := by
    rw [← integral_add_right_eq_self _ (t • (-v))]; simp
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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) ∂μ)
⊢ Eq (α := ℝ) (∫ (x : E), (f (x + t • v) - f x) * g x ∂μ) (∫ (x : E), f x * (g (x + t • -v) - g x) ∂μ)
have simp_rw : 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: simp_rw [_root_.sub_mul, _root_.mul_sub]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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) ∂μ)
⊢ 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 ∂μ)
have hf₁ : Integrable (ε := ℝ) (fun (x : E) ↦ f x * g (x + t • -v)) μ
Tactic: rw [integral_sub, integral_sub, S3]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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)) μ
⊢ 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 ∂μ)
have hg₁ : Integrable (ε := ℝ) (fun (x : E) ↦ f x * g x) μ
Tactic: rw [integral_sub, integral_sub, S3]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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) μ
⊢ 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 ∂μ)
have hf₂ : Integrable (ε := ℝ) (fun (x : E) ↦ f (x + t • v) * g x) μ
Tactic: rw [integral_sub, integral_sub, S3]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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 + t • -v)) μ
have hf₁ : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : E) ↦ f x * g (x + t • -v)
Tactic: apply Continuous.integrable_of_hasCompactSupport
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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)
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ f x * g (x + t • -v)) μ
have hf₂ : HasCompactSupport (β := ℝ) fun (x : E) ↦ f x * g (x + t • -v)
Tactic: apply Continuous.integrable_of_hasCompactSupport
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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 + t • v) * g x) μ
have hf₁ : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : E) ↦ f (x + t • v) * g x
Tactic: apply Continuous.integrable_of_hasCompactSupport
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ f (x + t • v) * g x) μ
have hf₂ : HasCompactSupport (β := ℝ) fun (x : E) ↦ f (x + t • v) * g x
Tactic: apply Continuous.integrable_of_hasCompactSupport
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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
⊢ ∀ᵐ (x : E) ∂μ, lineDeriv ℝ f x (∑ i ∈ s, a i • v i) = ∑ i ∈ s, a i • lineDeriv ℝ f x (v i)
have 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) ∂μ)
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 ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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
⊢ 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) ∂μ)
have 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 ∂μ)
Tactic: simp_rw [Finset.smul_sum]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (hypothesis)
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
⊢ 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 ∂μ)
have A : ∀ 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))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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) μ
⊢ 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 ∂μ)
have 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 ∂μ)
Tactic: rw [integral_finsetSum _ A]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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 ∂μ)
⊢ 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)) ∂μ)
have 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) ∂μ)
Tactic: simp_rw [← mul_assoc, mul_comm _ (a _), mul_assoc, integral_const_mul, mul_comm (g _), S1]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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) ∂μ)
⊢ 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)) ∂μ)
have 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) ∂μ)
Tactic: simp_rw [← mul_assoc, mul_comm _ (a _), mul_assoc, integral_const_mul, mul_comm (g _), S1]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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) ∂μ)
⊢ 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)) ∂μ)
have 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)) ∂μ)
Tactic: simp_rw [← mul_assoc, mul_comm _ (a _), mul_assoc, integral_const_mul, mul_comm (g _), S1]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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)) ∂μ)
⊢ 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)) ∂μ)
have 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) ∂μ)
Tactic: simp_rw [← mul_assoc, mul_comm _ (a _), mul_assoc, integral_const_mul, mul_comm (g _), S1]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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) μ
⊢ 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 ∂μ)
have 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 ∂μ)
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]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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) ∂μ)
⊢ 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 ∂μ)
have 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 ∂μ)
Tactic: obtain ⟨D, g_lip⟩ : ∃ D, LipschitzWith D g :=
      ContDiff.lipschitzWith_of_hasCompactSupport g_comp g_smooth (by simp)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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
⊢ 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 ∂μ)
have 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 ∂μ)
Tactic: simp_rw [integral_lineDeriv_mul_eq hf g_lip g_comp]