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
v : E
L : ℝ →L[ℝ] E := ContinuousLinearMap.smulRight (S := ℝ) 1 v
⊢ ∀ᵐ (p : E) ∂μ, LineDifferentiableAt ℝ f p v
have suffices : ∀ (p : E), ∀ᵐ (t : ℝ), LineDifferentiableAt ℝ f (p + t • v) v
Tactic: suffices A : ∀ p, ∀ᵐ (t : ℝ) ∂volume, LineDifferentiableAt ℝ f (p + t • v) v from
    ae_mem_of_ae_add_linearMap_mem L.toLinearMap volume μ
      (measurableSet_lineDifferentiableAt hf.continuous) A
-- 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
v : E
L : ℝ →L[ℝ] E := ContinuousLinearMap.smulRight (S := ℝ) 1 v
p : E
⊢ ∀ᵐ (t : ℝ), LineDifferentiableAt ℝ f (p + t • v) v
have this : ∀ᵐ (s : ℝ), DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ f (p + t • v)) s
Tactic: have : ∀ᵐ (s : ℝ), DifferentiableAt ℝ (fun t ↦ f (p + t • v)) s :=
    (hf.comp ((LipschitzWith.const p).add L.lipschitz)).ae_differentiableAt_real
-- 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
v : E
L : ℝ →L[ℝ] E := ContinuousLinearMap.smulRight (S := ℝ) 1 v
p : E
this : ∀ᵐ (s : ℝ), DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ f (p + t • v)) s
⊢ ∀ᵐ (t : ℝ), LineDifferentiableAt ℝ f (p + t • v) v
have h : ∀ (s : ℝ) (hs : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ f (p + t • v)) s), LineDifferentiableAt ℝ f (p + s • v) v
Tactic: filter_upwards [this] with s hs
-- 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
v : E
L : ℝ →L[ℝ] E := ContinuousLinearMap.smulRight (S := ℝ) 1 v
p : E
this : ∀ᵐ (s : ℝ), DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ f (p + t • v)) s
s : ℝ
hs : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ f (p + t • v)) s
⊢ LineDifferentiableAt ℝ f (p + s • v) v
have h's : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ f (p + t • v)) (s + 0)
Tactic: have h's : DifferentiableAt ℝ (fun t ↦ f (p + t • v)) (s + 0) := by simpa using hs
-- 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
v : E
L : ℝ →L[ℝ] E := ContinuousLinearMap.smulRight (S := ℝ) 1 v
p : E
this : ∀ᵐ (s : ℝ), DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ f (p + t • v)) s
s : ℝ
hs : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ f (p + t • v)) s
h's : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ f (p + t • v)) (s + 0)
⊢ LineDifferentiableAt ℝ f (p + s • v) v
have this₁ : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ s + t) 0
Tactic: have : DifferentiableAt ℝ (fun t ↦ s + t) 0 := differentiableAt_id.const_add _
-- 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
v : E
L : ℝ →L[ℝ] E := ContinuousLinearMap.smulRight (S := ℝ) 1 v
p : E
this_1 : ∀ᵐ (s : ℝ), DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ f (p + t • v)) s
s : ℝ
hs : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ f (p + t • v)) s
h's : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ f (p + t • v)) (s + 0)
this : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ s + t) 0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ f (p + s • v + t • v)) 0
have h : ∀ (t : ℝ), f (p + s • v + t • v) = ((fun (t : ℝ) ↦ f (p + t • v)) ∘ HAdd.hAdd s) t
Tactic: convert! h's.comp 0 this with _ t
-- 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 g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
⊢ Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
have hF_meas : ∀ᶠ (n : ℝ) in 𝓝[>] 0, AEStronglyMeasurable (β := ℝ) (fun (a : E) ↦ n⁻¹ • (f (a + n • v) - f a) * g a) μ
Tactic: apply tendsto_integral_filter_of_dominated_convergence (fun x ↦ (C * ‖v‖) * ‖g 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 g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
hF_meas : ∀ᶠ (n : ℝ) in 𝓝[>] 0, AEStronglyMeasurable (β := ℝ) (fun (a : E) ↦ n⁻¹ • (f (a + n • v) - f a) * g a) μ
⊢ Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
have h_bound : ∀ᶠ (n : ℝ) in 𝓝[>] 0, ∀ᵐ (a : E) ∂μ, ‖n⁻¹ • (f (a + n • v) - f a) * g a‖ ≤ (↑C : ℝ) * ‖v‖ * ‖g a‖
Tactic: apply tendsto_integral_filter_of_dominated_convergence (fun x ↦ (C * ‖v‖) * ‖g 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 g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
hF_meas : ∀ᶠ (n : ℝ) in 𝓝[>] 0, AEStronglyMeasurable (β := ℝ) (fun (a : E) ↦ n⁻¹ • (f (a + n • v) - f a) * g a) μ
h_bound : ∀ᶠ (n : ℝ) in 𝓝[>] 0, ∀ᵐ (a : E) ∂μ, ‖n⁻¹ • (f (a + n • v) - f a) * g a‖ ≤ (↑C : ℝ) * ‖v‖ * ‖g a‖
⊢ Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
have bound_integrable : Integrable (ε := ℝ) (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) μ
Tactic: apply tendsto_integral_filter_of_dominated_convergence (fun x ↦ (C * ‖v‖) * ‖g 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 g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
hF_meas : ∀ᶠ (n : ℝ) in 𝓝[>] 0, AEStronglyMeasurable (β := ℝ) (fun (a : E) ↦ n⁻¹ • (f (a + n • v) - f a) * g a) μ
h_bound : ∀ᶠ (n : ℝ) in 𝓝[>] 0, ∀ᵐ (a : E) ∂μ, ‖n⁻¹ • (f (a + n • v) - f a) * g a‖ ≤ (↑C : ℝ) * ‖v‖ * ‖g a‖
bound_integrable : Integrable (ε := ℝ) (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) μ
⊢ Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
have h_lim : ∀ᵐ (a : E) ∂μ, Tendsto (fun (n : ℝ) ↦ n⁻¹ • (f (a + n • v) - f a) * g a) (𝓝[>] 0) (𝓝 (lineDeriv ℝ f a v * g a))
Tactic: apply tendsto_integral_filter_of_dominated_convergence (fun x ↦ (C * ‖v‖) * ‖g 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 g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 0, AEStronglyMeasurable (β := ℝ) (fun (a : E) ↦ n⁻¹ • (f (a + n • v) - f a) * g a) μ
have hF_meas : ∀ (t : ℝ), AEStronglyMeasurable (β := ℝ) (fun (a : E) ↦ t⁻¹ • (f (a + t • v) - f a) * g a) μ
Tactic: filter_upwards with t
-- 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 g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
t : ℝ
⊢ AEStronglyMeasurable (β := ℝ) (fun (a : E) ↦ t⁻¹ • (f (a + t • v) - f a) * g a) μ
have apply : AEStronglyMeasurable (β := ℝ) (fun (a : E) ↦ t⁻¹ • (f (a + t • v) - f a)) μ
Tactic: apply AEStronglyMeasurable.mul ?_ hg.aestronglyMeasurable
-- 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 g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
t : ℝ
⊢ AEStronglyMeasurable (β := ℝ) (fun (a : E) ↦ t⁻¹ • (f (a + t • v) - f a)) μ
have apply : AEStronglyMeasurable (β := ℝ) (fun (x : E) ↦ f (x + t • v) - f x) μ
Tactic: apply aestronglyMeasurable_const.smul
-- 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 g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
t : ℝ
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : E) ↦ f (x + t • v) - f x) μ
have apply : AEStronglyMeasurable (β := ℝ) (fun (x : E) ↦ f (x + t • v)) μ
Tactic: apply AEStronglyMeasurable.sub _ hf.continuous.measurable.aestronglyMeasurable
-- 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 g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
t : ℝ
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : E) ↦ f (x + t • v)) μ
have hf₁ : AEMeasurable (β := ℝ) (fun (x : E) ↦ f (x + t • v)) μ
Tactic: apply AEMeasurable.aestronglyMeasurable
-- 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 g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
t : ℝ
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) t → ∀ᵐ (a : E) ∂μ, ‖t⁻¹ • (f (a + t • v) - f a) * g a‖ ≤ (↑C : ℝ) * ‖v‖ * ‖g a‖
have h : ∀ (ht : 0 < t), ∀ᵐ (a : E) ∂μ, ‖t⁻¹ • (f (a + t • v) - f a) * g a‖ ≤ (↑C : ℝ) * ‖v‖ * ‖g a‖
Tactic: (ht : 0 < t)
-- 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 g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 0, ∀ᵐ (a : E) ∂μ, ‖n⁻¹ • (f (a + n • v) - f a) * g a‖ ≤ (↑C : ℝ) * ‖v‖ * ‖g a‖
have h : ∀ (t : ℝ) (ht : 0 < t), ∀ᵐ (a : E) ∂μ, ‖t⁻¹ • (f (a + t • v) - f a) * g a‖ ≤ (↑C : ℝ) * ‖v‖ * ‖g a‖
Tactic: filter_upwards [self_mem_nhdsWithin] with t (ht : 0 < t)
-- 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 g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
t : ℝ
ht : 0 < t
⊢ ∀ᵐ (a : E) ∂μ, ‖t⁻¹ • (f (a + t • v) - f a) * g a‖ ≤ (↑C : ℝ) * ‖v‖ * ‖g a‖
have h : ∀ (x : E), ‖t⁻¹ • (f (x + t • v) - f x) * g x‖ ≤ (↑C : ℝ) * ‖v‖ * ‖g x‖
Tactic: filter_upwards with 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 g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
t : ℝ
ht : 0 < t
x : E
⊢ t⁻¹ * ‖f (x + t • v) - f x‖ * ‖g x‖ ≤ t⁻¹ * ((↑C : ℝ) * ‖x + t • v - x‖) * ‖g x‖
have hbc : ‖f (x + t • v) - f x‖ ≤ (↑C : ℝ) * ‖x + t • v - x‖
Tactic: gcongr
-- 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 g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
t : ℝ
ht : 0 < t
x : E
⊢ ‖t⁻¹ • (f (x + t • v) - f x) * g x‖ ≤ (↑C : ℝ) * ‖v‖ * ‖g x‖
have calc : ‖t⁻¹ • (f (x + t • v) - f x) * g x‖ = t⁻¹ * ‖f (x + t • v) - f x‖ * ‖g x‖
Tactic: calc ‖t⁻¹ • (f (x + t • v) - f x) * g x‖
      = (t⁻¹ * ‖f (x + t • v) - f x‖) * ‖g x‖ := by simp [norm_mul, ht.le]
    _ ≤ (t⁻¹ * (C * ‖(x + t • v) - x‖)) * ‖g x‖ := by
      gcongr; exact LipschitzWith.norm_sub_le hf (x + t • v) x
    _ = (C * ‖v‖) * ‖g x‖ := by simp [field, norm_smul, abs_of_nonneg ht.le]
-- 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 g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
t : ℝ
ht : 0 < t
x : E
calc : ‖t⁻¹ • (f (x + t • v) - f x) * g x‖ = t⁻¹ * ‖f (x + t • v) - f x‖ * ‖g x‖
⊢ ‖t⁻¹ • (f (x + t • v) - f x) * g x‖ ≤ (↑C : ℝ) * ‖v‖ * ‖g x‖
have calc₁ : t⁻¹ * ‖f (x + t • v) - f x‖ * ‖g x‖ ≤ t⁻¹ * ((↑C : ℝ) * ‖x + t • v - x‖) * ‖g x‖
Tactic: calc ‖t⁻¹ • (f (x + t • v) - f x) * g x‖
      = (t⁻¹ * ‖f (x + t • v) - f x‖) * ‖g x‖ := by simp [norm_mul, ht.le]
    _ ≤ (t⁻¹ * (C * ‖(x + t • v) - x‖)) * ‖g x‖ := by
      gcongr; exact LipschitzWith.norm_sub_le hf (x + t • v) x
    _ = (C * ‖v‖) * ‖g x‖ := by simp [field, norm_smul, abs_of_nonneg ht.le]
-- 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 g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
t : ℝ
ht : 0 < t
x : E
calc : ‖t⁻¹ • (f (x + t • v) - f x) * g x‖ = t⁻¹ * ‖f (x + t • v) - f x‖ * ‖g x‖
calc₁ : t⁻¹ * ‖f (x + t • v) - f x‖ * ‖g x‖ ≤ t⁻¹ * ((↑C : ℝ) * ‖x + t • v - x‖) * ‖g x‖
⊢ ‖t⁻¹ • (f (x + t • v) - f x) * g x‖ ≤ (↑C : ℝ) * ‖v‖ * ‖g x‖
have calc₂ : t⁻¹ * ((↑C : ℝ) * ‖x + t • v - x‖) * ‖g x‖ = (↑C : ℝ) * ‖v‖ * ‖g x‖
Tactic: calc ‖t⁻¹ • (f (x + t • v) - f x) * g x‖
      = (t⁻¹ * ‖f (x + t • v) - f x‖) * ‖g x‖ := by simp [norm_mul, ht.le]
    _ ≤ (t⁻¹ * (C * ‖(x + t • v) - x‖)) * ‖g x‖ := by
      gcongr; exact LipschitzWith.norm_sub_le hf (x + t • v) x
    _ = (C * ‖v‖) * ‖g x‖ := by simp [field, norm_smul, abs_of_nonneg ht.le]
-- 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 g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
⊢ ∀ᵐ (a : E) ∂μ, Tendsto (fun (n : ℝ) ↦ n⁻¹ • (f (a + n • v) - f a) * g a) (𝓝[>] 0) (𝓝 (lineDeriv ℝ f a v * g a))
have h : ∀ (x : E) (hx : LineDifferentiableAt ℝ f x v),
  Tendsto (fun (n : ℝ) ↦ n⁻¹ • (f (x + n • v) - f x) * g x) (𝓝[>] 0) (𝓝 (lineDeriv ℝ f x v * g x))
Tactic: filter_upwards [hf.ae_lineDifferentiableAt v] with x hx
-- 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 g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
⊢ Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
have K_compact : IsCompact K
Tactic: have K_compact : IsCompact K := IsCompact.cthickening h'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 : ℝ≥0
f g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
⊢ Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
have hF_meas : ∀ᶠ (n : ℝ) in 𝓝[>] 0, AEStronglyMeasurable (β := ℝ) (fun (a : E) ↦ n⁻¹ • (f (a + n • v) - f a) * g a) μ
Tactic: apply tendsto_integral_filter_of_dominated_convergence
      (K.indicator (fun x ↦ (C * ‖v‖) * ‖g 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 g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
hF_meas : ∀ᶠ (n : ℝ) in 𝓝[>] 0, AEStronglyMeasurable (β := ℝ) (fun (a : E) ↦ n⁻¹ • (f (a + n • v) - f a) * g a) μ
⊢ Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
have h_bound : ∀ᶠ (n : ℝ) in 𝓝[>] 0,
  ∀ᵐ (a : E) ∂μ, ‖n⁻¹ • (f (a + n • v) - f a) * g a‖ ≤ K.indicator (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) a
Tactic: apply tendsto_integral_filter_of_dominated_convergence
      (K.indicator (fun x ↦ (C * ‖v‖) * ‖g 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 g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
hF_meas : ∀ᶠ (n : ℝ) in 𝓝[>] 0, AEStronglyMeasurable (β := ℝ) (fun (a : E) ↦ n⁻¹ • (f (a + n • v) - f a) * g a) μ
h_bound :
  ∀ᶠ (n : ℝ) in 𝓝[>] 0,
    ∀ᵐ (a : E) ∂μ, ‖n⁻¹ • (f (a + n • v) - f a) * g a‖ ≤ K.indicator (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) a
⊢ Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
have bound_integrable : Integrable (ε := ℝ) (K.indicator fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) μ
Tactic: apply tendsto_integral_filter_of_dominated_convergence
      (K.indicator (fun x ↦ (C * ‖v‖) * ‖g 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 g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
hF_meas : ∀ᶠ (n : ℝ) in 𝓝[>] 0, AEStronglyMeasurable (β := ℝ) (fun (a : E) ↦ n⁻¹ • (f (a + n • v) - f a) * g a) μ
h_bound :
  ∀ᶠ (n : ℝ) in 𝓝[>] 0,
    ∀ᵐ (a : E) ∂μ, ‖n⁻¹ • (f (a + n • v) - f a) * g a‖ ≤ K.indicator (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) a
bound_integrable : Integrable (ε := ℝ) (K.indicator fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) μ
⊢ Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
have h_lim : ∀ᵐ (a : E) ∂μ, Tendsto (fun (n : ℝ) ↦ n⁻¹ • (f (a + n • v) - f a) * g a) (𝓝[>] 0) (𝓝 (lineDeriv ℝ f a v * g a))
Tactic: apply tendsto_integral_filter_of_dominated_convergence
      (K.indicator (fun x ↦ (C * ‖v‖) * ‖g 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 g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 0, AEStronglyMeasurable (β := ℝ) (fun (a : E) ↦ n⁻¹ • (f (a + n • v) - f a) * g a) μ
have hF_meas : ∀ (t : ℝ), AEStronglyMeasurable (β := ℝ) (fun (a : E) ↦ t⁻¹ • (f (a + t • v) - f a) * g a) μ
Tactic: filter_upwards with t
-- 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 g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
t : ℝ
⊢ AEStronglyMeasurable (β := ℝ) (fun (a : E) ↦ t⁻¹ • (f (a + t • v) - f a) * g a) μ
have apply : AEStronglyMeasurable (β := ℝ) (fun (a : E) ↦ t⁻¹ • (f (a + t • v) - f a)) μ
Tactic: apply AEStronglyMeasurable.mul ?_ hg.aestronglyMeasurable
-- 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 g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
t : ℝ
⊢ AEStronglyMeasurable (β := ℝ) (fun (a : E) ↦ t⁻¹ • (f (a + t • v) - f a)) μ
have apply : AEStronglyMeasurable (β := ℝ) (fun (x : E) ↦ f (x + t • v) - f x) μ
Tactic: apply aestronglyMeasurable_const.smul
-- 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 g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
t : ℝ
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : E) ↦ f (x + t • v) - f x) μ
have apply : AEStronglyMeasurable (β := ℝ) (fun (x : E) ↦ f (x + t • v)) μ
Tactic: apply AEStronglyMeasurable.sub _ hf.continuous.measurable.aestronglyMeasurable