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 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 : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioc 0 1) t
t_pos : 0 < t
x : E
hx : x ∉ K
A : f x = 0
rw : x + t • v ∉ Function.support f
⊢ f (x + t • v) = 0

Tactic:
rw [← Function.notMem_support]

Premises used: Function.notMem_support
-- 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 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 : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioc 0 1) t
t_pos : 0 < t
x : E
hx : x ∉ K
A : f x = 0
contrapose : ∀ (hx : x + t • v ∈ Function.support f), x ∈ K
⊢ x + t • v ∉ Function.support f

Tactic:
contrapose hx
-- 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 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 : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioc 0 1) t
t_pos : 0 < t
x : E
A : f x = 0
hx : x + t • v ∈ Function.support f
apply : dist x (x + t • v) ≤ ‖v‖
⊢ x ∈ K

Tactic:
apply mem_cthickening_of_dist_le _ _ (‖v‖) (tsupport f) (subset_tsupport _ hx)

Premises used: Norm.norm, subset_tsupport, Metric.mem_cthickening_of_dist_le, tsupport
-- 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 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 : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioc 0 1) t
t_pos : 0 < t
x : E
A : f x = 0
hx : x + t • v ∈ Function.support f
simp : t * ‖v‖ ≤ ‖v‖
⊢ dist x (x + t • v) ≤ ‖v‖

Tactic:
simp only [dist_eq_norm, sub_add_cancel_left, norm_neg, norm_smul, Real.norm_eq_abs,
          abs_of_nonneg t_pos.le]

Premises used: dist_eq_norm, norm_smul, sub_add_cancel_left, LT.lt.le, norm_neg, abs_of_nonneg, Real.norm_eq_abs
-- 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 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 : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioc 0 1) t
t_pos : 0 < t
x : E
A : f x = 0
hx : x + t • v ∈ Function.support f
⊢ t * ‖v‖ ≤ ‖v‖

Tactic:
mul_le_of_le_one_left (norm_nonneg v) ht.2

Premises used: mul_le_of_le_one_left, And.right, norm_nonneg
-- 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 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 : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioc 0 1) t
t_pos : 0 < t
x : E
A : f x = 0
hx : x + t • v ∈ Function.support f
⊢ t * ‖v‖ ≤ ‖v‖

Tactic:
exact mul_le_of_le_one_left (norm_nonneg v) ht.2

Premises used: mul_le_of_le_one_left, And.right, norm_nonneg
-- 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 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 : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioc 0 1) t
t_pos : 0 < t
x : E
hx : x ∉ K
A : f x = 0
⊢ f (x + t • v) = 0

Tactic:
have B : f (x + t • v) = 0 := by
        rw [← Function.notMem_support]
        contrapose hx
        apply mem_cthickening_of_dist_le _ _ (‖v‖) (tsupport f) (subset_tsupport _ hx)
        simp only [dist_eq_norm, sub_add_cancel_left, norm_neg, norm_smul, Real.norm_eq_abs,
          abs_of_nonneg t_pos.le]
        exact mul_le_of_le_one_left (norm_nonneg v) ht.2
-- 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 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 : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioc 0 1) t
t_pos : 0 < t
x : E
hx : x ∉ K
A : f x = 0
B : f (x + t • v) = 0
neg : LE.le (α := ℝ) 0 (K.indicator (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) x)
⊢ ‖t⁻¹ • (f (x + t • v) - f x) * g x‖ ≤ K.indicator (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) x

Tactic:
simp only [B, A, _root_.sub_self, smul_eq_mul, mul_zero, zero_mul, norm_zero]

Premises used: sub_self, MulZeroClass.zero_mul, norm_zero, MulZeroClass.mul_zero, smul_eq_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 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 : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioc 0 1) t
t_pos : 0 < t
x : E
hx : x ∉ K
A : f x = 0
B : f (x + t • v) = 0
y : E
_hy : y ∈ K
⊢ 0 ≤ (↑C : ℝ) * ‖v‖ * ‖g y‖

Tactic:
positivity
-- 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 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 : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioc 0 1) t
t_pos : 0 < t
x : E
hx : x ∉ K
A : f x = 0
B : f (x + t • v) = 0
⊢ LE.le (α := ℝ) 0 (K.indicator (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) x)

Tactic:
exact indicator_nonneg (fun y _hy ↦ by positivity) _

Premises used: Set.indicator_nonneg
-- 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 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
bound_integrable : IntegrableOn (ε := ℝ) (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) K μ
⊢ Integrable (ε := ℝ) (K.indicator fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) μ

Tactic:
rw [integrable_indicator_iff K_compact.measurableSet]

Premises used: MeasureTheory.integrable_indicator_iff, IsCompact.measurableSet
-- 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 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
⊢ ContinuousOn (Y := ℝ) (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) K

Tactic:
fun_prop
-- 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 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
⊢ IntegrableOn (ε := ℝ) (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) K μ

Tactic:
exact ContinuousOn.integrableOn_compact K_compact (by fun_prop)

Premises used: ContinuousOn.integrableOn_compact
-- 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 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
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))
⊢ ∀ᵐ (a : E) ∂μ, Tendsto (fun (n : ℝ) ↦ n⁻¹ • (f (a + n • v) - f a) * g a) (𝓝[>] 0) (𝓝 (lineDeriv ℝ f a v * g a))

Tactic:
filter_upwards [hf.ae_lineDifferentiableAt v] with x hx

Premises used: LipschitzWith.ae_lineDifferentiableAt
-- 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 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
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:
hx.hasLineDerivAt.tendsto_slope_zero_right.mul tendsto_const_nhds

Premises used: tendsto_const_nhds, HasLineDerivAt.tendsto_slope_zero_right, Filter.Tendsto.mul, LineDifferentiableAt.hasLineDerivAt
-- 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 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
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:
exact hx.hasLineDerivAt.tendsto_slope_zero_right.mul tendsto_const_nhds

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

Tactic:
have A : Tendsto (fun (t : ℝ) ↦ ∫ x, (t⁻¹ • (f (x + t • v) - f x)) * g x ∂μ) (𝓝[>] 0)
              (𝓝 (∫ x, lineDeriv ℝ f x v * g x ∂μ)) :=
    integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul
      hf (hg.continuous.integrable_of_hasCompactSupport h'g) 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 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 ∂μ))
⊢ Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ))

Tactic:
have B : Tendsto (fun (t : ℝ) ↦ ∫ x, (t⁻¹ • (g (x + t • (-v)) - g x)) * f x ∂μ) (𝓝[>] 0)
              (𝓝 (∫ x, lineDeriv ℝ g x (-v) * f x ∂μ)) :=
    integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul' hg h'g hf.continuous (-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 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 ∂μ))
S1 :
  ∀ (t : ℝ),
    Eq (α := ℝ) (∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ)
⊢ Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))

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

Tactic:
tendsto_nhds_unique A B

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

Tactic:
exact tendsto_nhds_unique A B

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

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

Tactic:
simp only [smul_eq_mul, mul_assoc, integral_const_mul, S2, mul_comm (f _)]

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

Tactic:
rw [← integral_add_right_eq_self _ (t • (-v))]

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

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 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) ∂μ)

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

Tactic:
simp_rw [_root_.sub_mul, _root_.mul_sub]

Premises used: mul_sub, sub_mul