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 : ℝ≥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), HMul.hMul (α := ℝ) ((fderiv ℝ g x : (a : E) → ℝ) (-∑ i ∈ s, a i • v i) : ℝ) (f x) ∂μ)
    (∑ x ∈ s, a x * ∫ (x_1 : E), HMul.hMul (α := ℝ) ((fderiv ℝ g x_1 : (a : E) → ℝ) (-v x) : ℝ) (f x_1) ∂μ)
⊢ 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 [(g_smooth.differentiable (by simp)).differentiableAt.lineDeriv_eq_fderiv]

Premises used: Differentiable.differentiableAt, ContDiff.differentiable, DifferentiableAt.lineDeriv_eq_fderiv
-- 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 :
  Eq (α := ℝ)
    (∫ (x : E), -((∑ x_1 ∈ s, HMul.hMul (β := ℝ) (a x_1) ((fderiv ℝ g x : (a : E) → ℝ) (v x_1) : ℝ)) * f x) ∂μ)
    (∑ x ∈ s, a x * ∫ (x_1 : E), -HMul.hMul (α := ℝ) ((fderiv ℝ g x_1 : (a : E) → ℝ) (v x) : ℝ) (f x_1) ∂μ)
⊢ Eq (α := ℝ) (∫ (x : E), HMul.hMul (α := ℝ) ((fderiv ℝ g x : (a : E) → ℝ) (-∑ i ∈ s, a i • v i) : ℝ) (f x) ∂μ)
    (∑ x ∈ s, a x * ∫ (x_1 : E), HMul.hMul (α := ℝ) ((fderiv ℝ g x_1 : (a : E) → ℝ) (-v x) : ℝ) (f x_1) ∂μ)

Tactic:
simp only [map_neg, _root_.map_sum, map_smul, smul_eq_mul, neg_mul]

Premises used: map_neg, map_sum, neg_mul, smul_eq_mul, map_smul
-- 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 :
  Eq (α := ℝ) (∫ (a_1 : E), (∑ x ∈ s, HMul.hMul (β := ℝ) (a x) ((fderiv ℝ g a_1 : (a : E) → ℝ) (v x) : ℝ)) * f a_1 ∂μ)
    (∑ x ∈ s, a x * ∫ (a : E), HMul.hMul (α := ℝ) ((fderiv ℝ g a : (a : E) → ℝ) (v x) : ℝ) (f a) ∂μ)
⊢ Eq (α := ℝ)
    (∫ (x : E), -((∑ x_1 ∈ s, HMul.hMul (β := ℝ) (a x_1) ((fderiv ℝ g x : (a : E) → ℝ) (v x_1) : ℝ)) * f x) ∂μ)
    (∑ x ∈ s, a x * ∫ (x_1 : E), -HMul.hMul (α := ℝ) ((fderiv ℝ g x_1 : (a : E) → ℝ) (v x) : ℝ) (f x_1) ∂μ)

Tactic:
simp only [integral_neg, mul_neg, Finset.sum_neg_distrib, neg_inj]

Premises used: MeasureTheory.integral_neg, neg_inj, Finset.sum_neg_distrib, mul_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 : ℝ≥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 (α := ℝ) (∫ (a_1 : E), (∑ x ∈ s, HMul.hMul (β := ℝ) (a x) ((fderiv ℝ g a_1 : (a : E) → ℝ) (v x) : ℝ)) * f a_1 ∂μ)
    (∑ x ∈ s, a x * ∫ (a : E), HMul.hMul (α := ℝ) ((fderiv ℝ g a : (a : E) → ℝ) (v x) : ℝ) (f a) ∂μ)

Tactic:
S2
-- 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
⊢ Eq (α := ℝ) (∫ (a_1 : E), (∑ x ∈ s, HMul.hMul (β := ℝ) (a x) ((fderiv ℝ g a_1 : (a : E) → ℝ) (v x) : ℝ)) * f a_1 ∂μ)
    (∑ x ∈ s, a x * ∫ (a : E), HMul.hMul (α := ℝ) ((fderiv ℝ g a : (a : E) → ℝ) (v x) : ℝ) (f a) ∂μ)

Tactic:
exact S2
-- 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), (∑ 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 ∂μ)

Tactic:
suffices S2 : ∫ x, (∑ i ∈ s, a i * fderiv ℝ g x (v i)) * f x ∂μ =
                  ∑ i ∈ s, a i * ∫ x, fderiv ℝ g x (v i) * f x ∂μ by
    obtain ⟨D, g_lip⟩ : ∃ D, LipschitzWith D g :=
      ContDiff.lipschitzWith_of_hasCompactSupport g_comp g_smooth (by simp)
    simp_rw [integral_lineDeriv_mul_eq hf g_lip g_comp]
    simp_rw [(g_smooth.differentiable (by simp)).differentiableAt.lineDeriv_eq_fderiv]
    simp only [map_neg, _root_.map_sum, map_smul, smul_eq_mul, neg_mul]
    simp only [integral_neg, mul_neg, Finset.sum_neg_distrib, neg_inj]
    exact S2
-- 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) μ
B :
  ∀ i ∈ s, Integrable (ε := ℝ) (fun (x : E) ↦ a i * HMul.hMul (α := ℝ) ((fderiv ℝ g x : (a : E) → ℝ) (v i) : ℝ) (f x)) μ
simp_rw :
  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) ∂μ)
simp_rw₁ :
  Eq (α := ℝ) (∫ (x : E), ∑ x_1 ∈ s, a x_1 * HMul.hMul (α := ℝ) ((fderiv ℝ g x : (a : E) → ℝ) (v x_1) : ℝ) (f x) ∂μ)
    (∑ i ∈ s, a i * ∫ (x : E), HMul.hMul (α := ℝ) ((fderiv ℝ g x : (a : E) → ℝ) (v i) : ℝ) (f x) ∂μ)
simp_rw₂ :
  Eq (α := ℝ) (∑ i ∈ s, ∫ (a_1 : E), a i * HMul.hMul (α := ℝ) ((fderiv ℝ g a_1 : (a : E) → ℝ) (v i) : ℝ) (f a_1) ∂μ)
    (∑ i ∈ s, a i * ∫ (x : E), HMul.hMul (α := ℝ) ((fderiv ℝ g x : (a : E) → ℝ) (v i) : ℝ) (f x) ∂μ)
⊢ 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) ∂μ)

Tactic:
simp_rw [Finset.sum_mul, mul_assoc, integral_finsetSum s B, integral_const_mul]

Premises used: MeasureTheory.integral_const_mul, mul_assoc, MeasureTheory.integral_finsetSum, Finset.sum_mul
-- 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 :
  ∀ i ∈ s, Integrable (ε := ℝ) (fun (x : E) ↦ a i * HMul.hMul (α := ℝ) ((fderiv ℝ g x : (a : E) → ℝ) (v i) : ℝ) (f x)) μ
⊢ 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) ∂μ)

Tactic:
suffices B : ∀ i ∈ s, Integrable (fun x ↦ a i * (fderiv ℝ g x (v i) * f x)) μ by
    simp_rw [Finset.sum_mul, mul_assoc, integral_finsetSum s B, integral_const_mul]
-- 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) μ
i : ι
_hi : i ∈ s
L : StrongDual ℝ E → ℝ := fun (f : StrongDual ℝ E) ↦ (f : (a : E) → ℝ) (v i)
change : Integrable (ε := ℝ) (fun (x : E) ↦ a i * ((L ∘ fderiv ℝ g) x * f x)) μ
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ a i * HMul.hMul (α := ℝ) ((fderiv ℝ g x : (a : E) → ℝ) (v i) : ℝ) (f x)) μ

Tactic:
change Integrable (fun x ↦ a i * ((L ∘ (fderiv ℝ g)) x * f x)) μ

Premises used: Real, HMul.hMul, MeasureTheory.Integrable, Function.comp, fderiv
-- 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) μ
i : ι
_hi : i ∈ s
L : StrongDual ℝ E → ℝ := fun (f : StrongDual ℝ E) ↦ (f : (a : E) → ℝ) (v i)
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ a i * ((L ∘ fderiv ℝ g) x * f x)) μ

Tactic:
(Continuous.integrable_of_hasCompactSupport ?_ ?_).const_mul _

Premises used: MeasureTheory.Integrable.const_mul
-- 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) μ
i : ι
_hi : i ∈ s
L : StrongDual ℝ E → ℝ := fun (f : StrongDual ℝ E) ↦ (f : (a : E) → ℝ) (v i)
refine_1 : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : E) ↦ (L ∘ fderiv ℝ g) x * f x
refine_2 : HasCompactSupport (β := ℝ) fun (x : E) ↦ (L ∘ fderiv ℝ g) x * f x
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ a i * ((L ∘ fderiv ℝ g) x * f x)) μ

Tactic:
refine (Continuous.integrable_of_hasCompactSupport ?_ ?_).const_mul _

Premises used: MeasureTheory.Integrable.const_mul
-- 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) μ
i : ι
_hi : i ∈ s
L : StrongDual ℝ E → ℝ := fun (f : StrongDual ℝ E) ↦ (f : (a : E) → ℝ) (v i)
⊢ 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) μ
i : ι
_hi : i ∈ s
L : StrongDual ℝ E → ℝ := fun (f : StrongDual ℝ E) ↦ (f : (a : E) → ℝ) (v i)
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : E) ↦ (L ∘ fderiv ℝ g) x * f x

Tactic:
exact ((g_smooth.continuous_fderiv (by simp)).clm_apply continuous_const).mul
      hf.continuous

Premises used: continuous_const, ContDiff.continuous_fderiv, Continuous.clm_apply, 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 : ℝ≥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) μ
i : ι
_hi : i ∈ s
L : StrongDual ℝ E → ℝ := fun (f : StrongDual ℝ E) ↦ (f : (a : E) → ℝ) (v i)
⊢ HasCompactSupport (β := ℝ) fun (x : E) ↦ (L ∘ fderiv ℝ g) x * f x

Tactic:
((g_comp.fderiv ℝ).comp_left rfl).mul_right

Premises used: Real, HasCompactSupport.fderiv, HasCompactSupport.mul_right, HasCompactSupport.comp_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
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) μ
i : ι
_hi : i ∈ s
L : StrongDual ℝ E → ℝ := fun (f : StrongDual ℝ E) ↦ (f : (a : E) → ℝ) (v i)
⊢ HasCompactSupport (β := ℝ) fun (x : E) ↦ (L ∘ fderiv ℝ g) x * f x

Tactic:
exact ((g_comp.fderiv ℝ).comp_left rfl).mul_right

Premises used: Real, HasCompactSupport.fderiv, HasCompactSupport.mul_right, HasCompactSupport.comp_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
s : Set E
hs : s.Countable
have :
  ∀ (B : Basis (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) ℝ E),
    ∀ᵐ (x : E) ∂μ, ∃ (L : StrongDual ℝ E), ∀ v ∈ s, HasLineDerivAt ℝ f ((L : (a : E) → ℝ) v) x v
⊢ ∀ᵐ (x : E) ∂μ, ∃ (L : StrongDual ℝ E), ∀ v ∈ s, HasLineDerivAt ℝ f ((L : (a : E) → ℝ) v) x v

Tactic:
have B := Basis.ofVectorSpace ℝ E
-- 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
s : Set E
hs : s.Countable
B : Basis (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) ℝ E
⊢ ∀ᵐ (x : E) ∂μ,
    ∀ v ∈ s,
      lineDeriv ℝ f x
          (∑ i : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1),
            HSMul.hSMul (α := ℝ) (β := E)
              ((((B.repr : (a : E) → (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) →₀ ℝ) v :
                      (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) →₀ ℝ) :
                    (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → ℝ)
                  i :
                ℝ)
              ((B : (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → E) i : E)) =
        ∑ i : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1),
          HSMul.hSMul (α := ℝ)
            ((((B.repr : (a : E) → (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) →₀ ℝ) v :
                    (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) →₀ ℝ) :
                  (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → ℝ)
                i :
              ℝ)
            (lineDeriv ℝ f x ((B : (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → E) i))

Tactic:
have I1 : ∀ᵐ (x : E) ∂μ, ∀ v ∈ s, lineDeriv ℝ f x (∑ i, (B.repr v i) • B i) =
                                  ∑ i, B.repr v i • lineDeriv ℝ f x (B i) :=
    (ae_ball_iff hs).2 (fun v _ ↦ hf.ae_lineDeriv_sum_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
s : Set E
hs : s.Countable
B : Basis (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) ℝ E
I1 :
  ∀ᵐ (x : E) ∂μ,
    ∀ v ∈ s,
      lineDeriv ℝ f x
          (∑ i : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1),
            HSMul.hSMul (α := ℝ) (β := E)
              ((((B.repr : (a : E) → (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) →₀ ℝ) v :
                      (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) →₀ ℝ) :
                    (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → ℝ)
                  i :
                ℝ)
              ((B : (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → E) i : E)) =
        ∑ i : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1),
          HSMul.hSMul (α := ℝ)
            ((((B.repr : (a : E) → (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) →₀ ℝ) v :
                    (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) →₀ ℝ) :
                  (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → ℝ)
                i :
              ℝ)
            (lineDeriv ℝ f x ((B : (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → E) i))
⊢ ∀ᵐ (x : E) ∂μ, ∀ v ∈ s, LineDifferentiableAt ℝ f x v

Tactic:
have I2 : ∀ᵐ (x : E) ∂μ, ∀ v ∈ s, LineDifferentiableAt ℝ f x v :=
    (ae_ball_iff hs).2 (fun v _ ↦ hf.ae_lineDifferentiableAt v)
-- 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
s : Set E
hs : s.Countable
B : Basis (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) ℝ E
I1 :
  ∀ᵐ (x : E) ∂μ,
    ∀ v ∈ s,
      lineDeriv ℝ f x
          (∑ i : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1),
            HSMul.hSMul (α := ℝ) (β := E)
              ((((B.repr : (a : E) → (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) →₀ ℝ) v :
                      (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) →₀ ℝ) :
                    (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → ℝ)
                  i :
                ℝ)
              ((B : (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → E) i : E)) =
        ∑ i : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1),
          HSMul.hSMul (α := ℝ)
            ((((B.repr : (a : E) → (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) →₀ ℝ) v :
                    (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) →₀ ℝ) :
                  (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → ℝ)
                i :
              ℝ)
            (lineDeriv ℝ f x ((B : (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → E) i))
I2 : ∀ᵐ (x : E) ∂μ, ∀ v ∈ s, LineDifferentiableAt ℝ f x v
h :
  ∀ (x : E)
    (hx :
      ∀ v ∈ s,
        lineDeriv ℝ f x
            (∑ i : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1),
              HSMul.hSMul (α := ℝ) (β := E)
                ((((B.repr : (a : E) → (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) →₀ ℝ) v :
                        (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) →₀ ℝ) :
                      (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → ℝ)
                    i :
                  ℝ)
                ((B : (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → E) i : E)) =
          ∑ i : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1),
            HSMul.hSMul (α := ℝ)
              ((((B.repr : (a : E) → (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) →₀ ℝ) v :
                      (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) →₀ ℝ) :
                    (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → ℝ)
                  i :
                ℝ)
              (lineDeriv ℝ f x ((B : (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → E) i)))
    (h'x : ∀ v ∈ s, LineDifferentiableAt ℝ f x v),
    ∃ (L : StrongDual ℝ E), ∀ v ∈ s, HasLineDerivAt ℝ f ((L : (a : E) → ℝ) v) x v
⊢ ∀ᵐ (x : E) ∂μ, ∃ (L : StrongDual ℝ E), ∀ v ∈ s, HasLineDerivAt ℝ f ((L : (a : E) → ℝ) v) x v

Tactic:
filter_upwards [I1, I2] with x hx h'x