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 : ℝ≥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 ℝ 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 ∂μ)
have 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) ∂μ)
Tactic: simp_rw [(g_smooth.differentiable (by simp)).differentiableAt.lineDeriv_eq_fderiv]
-- 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), 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) ∂μ)
have 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) ∂μ)
Tactic: simp only [map_neg, _root_.map_sum, map_smul, smul_eq_mul, neg_mul]
-- 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), 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 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) ∂μ)
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
-- 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) μ
B :
  ∀ 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) ∂μ)
have 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) ∂μ)
Tactic: simp_rw [Finset.sum_mul, mul_assoc, integral_finsetSum s B, integral_const_mul]
-- 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) μ
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) ∂μ)
⊢ 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) ∂μ)
have 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) ∂μ)
Tactic: simp_rw [Finset.sum_mul, mul_assoc, integral_finsetSum s B, integral_const_mul]
-- 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) μ
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) ∂μ)
⊢ 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) ∂μ)
have 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) ∂μ)
Tactic: simp_rw [Finset.sum_mul, mul_assoc, integral_finsetSum s B, integral_const_mul]
-- 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), (∑ 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) ∂μ)
have suffices : ∀ i ∈ s, Integrable (ε := ℝ) (fun (x : E) ↦ a i * 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]
-- 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) μ
i : ι
_hi : i ∈ s
L : StrongDual ℝ E → ℝ := fun (f : StrongDual ℝ E) ↦ (f : (a : E) → ℝ) (v i)
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ a i * HMul.hMul (α := ℝ) ((fderiv ℝ g x : (a : E) → ℝ) (v i) : ℝ) (f x)) μ
have change : Integrable (ε := ℝ) (fun (x : E) ↦ a i * ((L ∘ fderiv ℝ g) x * f x)) μ
Tactic: change Integrable (fun x ↦ a i * ((L ∘ (fderiv ℝ g)) x * f x)) μ
-- 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) μ
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)) μ
have refine_1 : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : E) ↦ (L ∘ fderiv ℝ g) x * f x
Tactic: refine (Continuous.integrable_of_hasCompactSupport ?_ ?_).const_mul _
-- 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) μ
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
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ a i * ((L ∘ fderiv ℝ g) x * f x)) μ
have refine_2 : HasCompactSupport (β := ℝ) fun (x : E) ↦ (L ∘ fderiv ℝ g) x * f x
Tactic: refine (Continuous.integrable_of_hasCompactSupport ?_ ?_).const_mul _
-- 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
s : Set E
hs : s.Countable
⊢ ∀ᵐ (x : E) ∂μ, ∃ (L : StrongDual ℝ E), ∀ v ∈ s, HasLineDerivAt ℝ f ((L : (a : E) → ℝ) v) x v
have 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
Tactic: have B := Basis.ofVectorSpace ℝ E
-- 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
s : Set E
hs : s.Countable
B : Basis (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) ℝ E
⊢ ∀ᵐ (x : E) ∂μ, ∃ (L : StrongDual ℝ E), ∀ v ∈ s, HasLineDerivAt ℝ f ((L : (a : E) → ℝ) v) x v
have 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))
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 _ _ _)
-- 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
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) ∂μ, ∃ (L : StrongDual ℝ E), ∀ v ∈ s, HasLineDerivAt ℝ f ((L : (a : E) → ℝ) v) x v
have I2 : ∀ᵐ (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)
-- 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
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
⊢ ∀ᵐ (x : E) ∂μ, ∃ (L : StrongDual ℝ E), ∀ v ∈ s, HasLineDerivAt ℝ f ((L : (a : E) → ℝ) v) x v
have 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
Tactic: filter_upwards [I1, I2] with x hx h'x
-- 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
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
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 :=
  ((LinearMap.toContinuousLinearMap : (E →ₗ[ℝ] ℝ) ≃ₗ[ℝ] E →L[ℝ] ℝ) : (a : E →ₗ[ℝ] ℝ) → E →L[ℝ] ℝ)
    ((B.constr ℝ : (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) → ℝ) → E →ₗ[ℝ] ℝ)
        fun (i : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) ↦
        lineDeriv ℝ f x ((B : (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → E) i) :
      E →ₗ[ℝ] ℝ)
⊢ ∃ (L : StrongDual ℝ E), ∀ v ∈ s, HasLineDerivAt ℝ f ((L : (a : E) → ℝ) v) x v
have h : ∀ (v : E) (hv : v ∈ s), HasLineDerivAt ℝ f ((L : (a : E) → ℝ) v) x v
Tactic: refine ⟨L, fun v hv ↦ ?_⟩