awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Basic
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup X
inst_3 : NormedSpace ℝ X
inst_4 : HasContDiffBump E
n : ℕ∞
c g : X → E
s : Set X
f : (x : X) → ContDiffBump (c x)
x : X
hc : ContDiffWithinAt ℝ (↑n : ℕ∞ω) c s x
hr : ContDiffWithinAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : X) ↦ (f x).rIn) s x
hR : ContDiffWithinAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : X) ↦ (f x).rOut) s x
hg : ContDiffWithinAt ℝ (↑n : ℕ∞ω) g s x
⊢ ContDiffWithinAt.{0, u_2, u_1} ℝ (F := ℝ × E) (↑n : ℕ∞ω)
    (fun (x : X) ↦ ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x))) s x

Tactic:
(hR.div hr (f x).rIn_pos.ne').prodMk ((hr.inv (f x).rIn_pos.ne').smul (hg.sub hc))

Premises used: ContDiffWithinAt.sub, ContDiffWithinAt.smul, ContDiffWithinAt.inv, LT.lt.ne', ContDiffWithinAt.div, ContDiffWithinAt.prodMk, ContDiffBump.rIn_pos
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Basic
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup X
inst_3 : NormedSpace ℝ X
inst_4 : HasContDiffBump E
n : ℕ∞
c g : X → E
s : Set X
f : (x : X) → ContDiffBump (c x)
x : X
hc : ContDiffWithinAt ℝ (↑n : ℕ∞ω) c s x
hr : ContDiffWithinAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : X) ↦ (f x).rIn) s x
hR : ContDiffWithinAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : X) ↦ (f x).rOut) s x
hg : ContDiffWithinAt ℝ (↑n : ℕ∞ω) g s x
⊢ ContDiffWithinAt.{0, u_2, u_1} ℝ (F := ℝ × E) (↑n : ℕ∞ω)
    (fun (x : X) ↦ ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x))) s x

Tactic:
exact (hR.div hr (f x).rIn_pos.ne').prodMk ((hr.inv (f x).rIn_pos.ne').smul (hg.sub hc))

Premises used: ContDiffWithinAt.sub, ContDiffWithinAt.smul, ContDiffWithinAt.inv, LT.lt.ne', ContDiffWithinAt.div, ContDiffWithinAt.prodMk, ContDiffBump.rIn_pos
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Basic
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup X
inst_3 : NormedSpace ℝ X
inst_4 : HasContDiffBump E
n : ℕ∞
c g : X → E
f : (x : X) → ContDiffBump (c x)
x : X
hc : ContDiffAt ℝ (↑n : ℕ∞ω) c x
hr : ContDiffAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : X) ↦ (f x).rIn) x
hR : ContDiffAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : X) ↦ (f x).rOut) x
hg : ContDiffAt ℝ (↑n : ℕ∞ω) g x
⊢ ContDiffAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : X) ↦ (↑(f x) : E → ℝ) (g x)) x

Tactic:
hc.contDiffBump hr hR hg

Premises used: ContDiffAt, ContDiffWithinAt.contDiffBump
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Basic
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup X
inst_3 : NormedSpace ℝ X
inst_4 : HasContDiffBump E
n : ℕ∞
c g : X → E
f : (x : X) → ContDiffBump (c x)
hc : ContDiff ℝ (↑n : ℕ∞ω) c
hr : ContDiff ℝ (F := ℝ) (↑n : ℕ∞ω) fun (x : X) ↦ (f x).rIn
hR : ContDiff ℝ (F := ℝ) (↑n : ℕ∞ω) fun (x : X) ↦ (f x).rOut
hg : ContDiff ℝ (↑n : ℕ∞ω) g
rw :
  ∀ (hc : ∀ (x : X), ContDiffAt ℝ (↑n : ℕ∞ω) c x)
    (hr : ∀ (x : X), ContDiffAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : X) ↦ (f x).rIn) x)
    (hR : ∀ (x : X), ContDiffAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : X) ↦ (f x).rOut) x)
    (hg : ∀ (x : X), ContDiffAt ℝ (↑n : ℕ∞ω) g x) (x : X),
    ContDiffAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : X) ↦ (↑(f x) : E → ℝ) (g x)) x
⊢ ContDiff ℝ (F := ℝ) (↑n : ℕ∞ω) fun (x : X) ↦ (↑(f x) : E → ℝ) (g x)

Tactic:
rw [contDiff_iff_contDiffAt] at *

Premises used: contDiff_iff_contDiffAt
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Basic
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup X
inst_3 : NormedSpace ℝ X
inst_4 : HasContDiffBump E
n : ℕ∞
c g : X → E
f : (x : X) → ContDiffBump (c x)
hc : ∀ (x : X), ContDiffAt ℝ (↑n : ℕ∞ω) c x
hr : ∀ (x : X), ContDiffAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : X) ↦ (f x).rIn) x
hR : ∀ (x : X), ContDiffAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : X) ↦ (f x).rOut) x
hg : ∀ (x : X), ContDiffAt ℝ (↑n : ℕ∞ω) g x
⊢ ∀ (x : X), ContDiffAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : X) ↦ (↑(f x) : E → ℝ) (g x)) x

Tactic:
fun x => (hc x).contDiffBump (hr x) (hR x) (hg x)

Premises used: ContDiffAt.contDiffBump
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Basic
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup X
inst_3 : NormedSpace ℝ X
inst_4 : HasContDiffBump E
n : ℕ∞
c g : X → E
f : (x : X) → ContDiffBump (c x)
hc : ∀ (x : X), ContDiffAt ℝ (↑n : ℕ∞ω) c x
hr : ∀ (x : X), ContDiffAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : X) ↦ (f x).rIn) x
hR : ∀ (x : X), ContDiffAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : X) ↦ (f x).rOut) x
hg : ∀ (x : X), ContDiffAt ℝ (↑n : ℕ∞ω) g x
⊢ ∀ (x : X), ContDiffAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : X) ↦ (↑(f x) : E → ℝ) (g x)) x

Tactic:
exact fun x => (hc x).contDiffBump (hr x) (hR x) (hg x)

Premises used: ContDiffAt.contDiffBump
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
c : E
f : ContDiffBump c
n : ℕ∞
⊢ ContDiff ℝ (↑n : ℕ∞ω) (↑f : E → ℝ)

Tactic:
contDiff_const.contDiffBump contDiff_const contDiff_const contDiff_id

Premises used: contDiff_id, contDiff_const, ContDiff.contDiffBump
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
⊢ ContDiffAt ℝ (↑n : ℕ∞ω) (↑f : E → ℝ) x

Tactic:
f.contDiff.contDiffAt

Premises used: ContDiffBump.contDiff, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
s : Set E
⊢ ContDiffWithinAt ℝ (↑n : ℕ∞ω) (↑f : E → ℝ) s x

Tactic:
f.contDiffAt.contDiffWithinAt

Premises used: ContDiffBump.contDiffAt, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
c : E
f : ContDiffBump c
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (↑f : E → ℝ)

Tactic:
contDiff_zero.mp f.contDiff

Premises used: contDiff_zero, ContDiffBump.contDiff, Iff.mp
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : NormedSpace ℝ E'
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace ℝ G
inst_5 : CompleteSpace E'
φ : ContDiffBump.{uG} (E := G) 0
inst_6 : HasContDiffBump G
x₀ : G
hg : ∀ x ∈ ball x₀ φ.rOut, g x = g x₀
simp_rw :
  ∫ (t : G), (((lsmul ℝ ℝ : (a : ℝ) → E' →L[ℝ] E') ((↑φ : G → ℝ) t) : E' →L[ℝ] E') : (a : E') → E') (g x₀) ∂μ =
    integral μ (↑φ : G → ℝ) • g x₀
simp_rw₁ : ∫ (t : G), (↑φ : G → ℝ) t • g x₀ ∂μ = integral μ (↑φ : G → ℝ) • g x₀
⊢ ((↑φ : G → ℝ) ⋆[lsmul ℝ ℝ, μ] g) x₀ = integral μ (↑φ : G → ℝ) • g x₀

Tactic:
simp_rw [convolution_eq_right' _ φ.support_eq.subset hg, lsmul_apply, integral_smul_const]

Premises used: MeasureTheory.convolution_eq_right', integral_smul_const, ContinuousLinearMap.lsmul_apply, ContDiffBump.support_eq, Eq.subset
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : NormedSpace ℝ E'
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace ℝ G
inst_5 : CompleteSpace E'
φ : ContDiffBump.{uG} (E := G) 0
inst_6 : BorelSpace G
inst_7 : FiniteDimensional ℝ G
inst_8 : IsLocallyFiniteMeasure μ
inst_9 : μ.IsOpenPosMeasure
x₀ : G
hg : ∀ x ∈ ball x₀ φ.rOut, g x = g x₀
rw : ∫ (t : G), (((lsmul ℝ ℝ : (a : ℝ) → E' →L[ℝ] E') (φ.normed μ t) : E' →L[ℝ] E') : (a : E') → E') (g x₀) ∂μ = g x₀
⊢ (φ.normed μ ⋆[lsmul ℝ ℝ, μ] g) x₀ = g x₀

Tactic:
rw [convolution_eq_right' _ φ.support_normed_eq.subset hg]

Premises used: MeasureTheory.convolution_eq_right', ContDiffBump.support_normed_eq, Eq.subset
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : NormedSpace ℝ E'
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace ℝ G
inst_5 : CompleteSpace E'
φ : ContDiffBump.{uG} (E := G) 0
inst_6 : BorelSpace G
inst_7 : FiniteDimensional ℝ G
inst_8 : IsLocallyFiniteMeasure μ
inst_9 : μ.IsOpenPosMeasure
x₀ : G
hg : ∀ x ∈ ball x₀ φ.rOut, g x = g x₀
⊢ ∫ (t : G), (((lsmul ℝ ℝ : (a : ℝ) → E' →L[ℝ] E') (φ.normed μ t) : E' →L[ℝ] E') : (a : E') → E') (g x₀) ∂μ = g x₀

Tactic:
integral_normed_smul φ μ (g x₀)

Premises used: ContDiffBump.integral_normed_smul
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : NormedSpace ℝ E'
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace ℝ G
inst_5 : CompleteSpace E'
φ : ContDiffBump.{uG} (E := G) 0
inst_6 : BorelSpace G
inst_7 : FiniteDimensional ℝ G
inst_8 : IsLocallyFiniteMeasure μ
inst_9 : μ.IsOpenPosMeasure
x₀ : G
hg : ∀ x ∈ ball x₀ φ.rOut, g x = g x₀
⊢ ∫ (t : G), (((lsmul ℝ ℝ : (a : ℝ) → E' →L[ℝ] E') (φ.normed μ t) : E' →L[ℝ] E') : (a : E') → E') (g x₀) ∂μ = g x₀

Tactic:
exact integral_normed_smul φ μ (g x₀)

Premises used: ContDiffBump.integral_normed_smul
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : NormedSpace ℝ E'
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace ℝ G
inst_5 : CompleteSpace E'
φ : ContDiffBump.{uG} (E := G) 0
inst_6 : BorelSpace G
inst_7 : FiniteDimensional ℝ G
inst_8 : μ.IsAddHaarMeasure
x₀ : G
ε : ℝ
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ φ.rOut, dist (g x) (g x₀) ≤ ε
simp_rw : dist (g x₀) (g x₀) ≤ ε
⊢ 0 ≤ ε

Tactic:
simp_rw [← dist_self (g x₀), hg x₀ (mem_ball_self φ.rOut_pos)]

Premises used: Metric.mem_ball_self, dist_self, ContDiffBump.rOut_pos
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : NormedSpace ℝ E'
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace ℝ G
inst_5 : CompleteSpace E'
inst_6 : BorelSpace G
inst_7 : FiniteDimensional ℝ G
inst_8 : μ.IsAddHaarMeasure
ι : Type u_1
φ : ι → ContDiffBump.{uG} (E := G) 0
g : ι → G → E'
k : ι → G
x₀ : G
z₀ : E'
l : Filter ι
hφ : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝 0)
hig : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (g i) μ
hcg : Tendsto (uncurry g) (l ×ˢ 𝓝 x₀) (𝓝 z₀)
hk : Tendsto k l (𝓝 x₀)
⊢ Tendsto (fun (i : ι) ↦ ((φ i).normed μ ⋆[lsmul ℝ ℝ, μ] g i) (k i)) l (𝓝 z₀)

Tactic:
convolution_tendsto_right (Eventually.of_forall fun i => (φ i).nonneg_normed)
    (Eventually.of_forall fun i => (φ i).integral_normed) (tendsto_support_normed_smallSets hφ) hig
    hcg hk

Premises used: ContDiffBump.nonneg_normed, ContDiffBump.integral_normed, MeasureTheory.convolution_tendsto_right, Filter.Eventually.of_forall, ContDiffBump.tendsto_support_normed_smallSets
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : NormedSpace ℝ E'
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace ℝ G
inst_5 : CompleteSpace E'
inst_6 : BorelSpace G
inst_7 : FiniteDimensional ℝ G
inst_8 : μ.IsAddHaarMeasure
ι : Type u_1
φ : ι → ContDiffBump.{uG} (E := G) 0
l : Filter ι
hφ : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝 0)
hg :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
x₀ : G
⊢ Tendsto (fun (i : ι) ↦ ((φ i).normed μ ⋆[lsmul ℝ ℝ, μ] g) x₀) l (𝓝 (g x₀))

Tactic:
convolution_tendsto_right hφ (Eventually.of_forall fun _ => hg.aestronglyMeasurable)
    ((hg.tendsto x₀).comp tendsto_snd) tendsto_const_nhds

Premises used: tendsto_const_nhds, ContDiffBump.convolution_tendsto_right, Filter.Eventually.of_forall, Continuous.tendsto, Filter.Tendsto.comp, Continuous.aestronglyMeasurable, Filter.tendsto_snd
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : NormedSpace ℝ E'
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace ℝ G
inst_5 : CompleteSpace E'
inst_6 : BorelSpace G
inst_7 : FiniteDimensional ℝ G
inst_8 : μ.IsAddHaarMeasure
ι : Type u_1
φ : ι → ContDiffBump.{uG} (E := G) 0
l : Filter ι
K : ℝ
hφ : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g μ
h :
  ∀ (x₀ : G)
    (h₀ :
      Tendsto (β := ℝ) (fun (a : Set G) ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ)
        (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)),
    Tendsto (fun (i : ι) ↦ ((φ i).normed μ ⋆[lsmul ℝ ℝ, μ] g) x₀) l (𝓝 (g x₀))
⊢ ∀ᵐ (x₀ : G) ∂μ, Tendsto (fun (i : ι) ↦ ((φ i).normed μ ⋆[lsmul ℝ ℝ, μ] g) x₀) l (𝓝 (g x₀))

Tactic:
filter_upwards [(Besicovitch.vitaliFamily μ).ae_tendsto_average_norm_sub hg] with x₀ h₀

Premises used: Besicovitch.vitaliFamily, VitaliFamily.ae_tendsto_average_norm_sub
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : NormedSpace ℝ E'
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace ℝ G
inst_5 : CompleteSpace E'
inst_6 : BorelSpace G
inst_7 : FiniteDimensional ℝ G
inst_8 : μ.IsAddHaarMeasure
ι : Type u_1
φ : ι → ContDiffBump.{uG} (E := G) 0
l : Filter ι
K : ℝ
hφ : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g μ
x₀ : G
h₀ :
  Tendsto (β := ℝ) (fun (a : Set G) ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ)
    (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
h : Tendsto (fun (i : ι) ↦ ∫ (t : G), (φ i).normed μ (x₀ - t) • g t ∂μ) l (𝓝 (g x₀))
⊢ Tendsto (fun (i : ι) ↦ ((φ i).normed μ ⋆[lsmul ℝ ℝ, μ] g) x₀) l (𝓝 (g x₀))

Tactic:
simp only [convolution_eq_swap, lsmul_apply]

Premises used: ContinuousLinearMap.lsmul_apply, MeasureTheory.convolution_eq_swap
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : NormedSpace ℝ E'
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace ℝ G
inst_5 : CompleteSpace E'
inst_6 : BorelSpace G
inst_7 : FiniteDimensional ℝ G
inst_8 : μ.IsAddHaarMeasure
ι : Type u_1
φ : ι → ContDiffBump.{uG} (E := G) 0
l : Filter ι
K : ℝ
hφ : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g μ
x₀ : G
h₀ :
  Tendsto (β := ℝ) (fun (a : Set G) ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ)
    (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝[>] 0)

Tactic:
have hφ' : Tendsto (fun i ↦ (φ i).rOut) l (𝓝[>] 0) :=
    tendsto_nhdsWithin_iff.2 ⟨hφ, Eventually.of_forall (fun i ↦ (φ i).rOut_pos)⟩
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : NormedSpace ℝ E'
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace ℝ G
inst_5 : CompleteSpace E'
inst_6 : BorelSpace G
inst_7 : FiniteDimensional ℝ G
inst_8 : μ.IsAddHaarMeasure
ι : Type u_1
φ : ι → ContDiffBump.{uG} (E := G) 0
l : Filter ι
K : ℝ
hφ : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g μ
x₀ : G
h₀ :
  Tendsto (β := ℝ) (fun (a : Set G) ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ)
    (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
hφ' : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝[>] 0)
⊢ Tendsto (β := ℝ)
    (Function.comp (β := ℝ) ((fun (a : Set G) ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ∘ fun (r : ℝ) ↦ closedBall x₀ r)
      fun (i : ι) ↦ (φ i).rOut)
    l (𝓝 0)

Tactic:
have := (h₀.comp (Besicovitch.tendsto_filterAt μ x₀)).comp hφ'
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : NormedSpace ℝ E'
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace ℝ G
inst_5 : CompleteSpace E'
inst_6 : BorelSpace G
inst_7 : FiniteDimensional ℝ G
inst_8 : μ.IsAddHaarMeasure
ι : Type u_1
φ : ι → ContDiffBump.{uG} (E := G) 0
l : Filter ι
K : ℝ
hφ : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g μ
x₀ : G
h₀ :
  Tendsto (β := ℝ) (fun (a : Set G) ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ)
    (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
hφ' : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝[>] 0)
this :
  Tendsto (β := ℝ)
    (Function.comp (β := ℝ) ((fun (a : Set G) ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ∘ fun (r : ℝ) ↦ closedBall x₀ r)
      fun (i : ι) ↦ (φ i).rOut)
    l (𝓝 0)
h : ∀ᶠ (i : ι) in l, IntegrableOn g ((fun (r : ℝ) ↦ closedBall x₀ r) ((fun (i : ι) ↦ (φ i).rOut) i)) μ
h₁ : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : G), (φ i).normed μ (x₀ - y) ∂μ) l (𝓝 1)
h₂ :
  ∀ᶠ (i : ι) in l,
    Subset.{uG} (α := Set G) (support (M := ℝ) fun (y : G) ↦ (φ i).normed μ (x₀ - y))
      ((fun (r : ℝ) ↦ closedBall x₀ r) ((fun (i : ι) ↦ (φ i).rOut) i))
h₃ :
  ∀ᶠ (i : ι) in l,
    ∀ (x : G),
      |(φ i).normed μ (x₀ - x)| ≤
        K ^ Module.finrank ℝ G / μ.real ((fun (r : ℝ) ↦ closedBall x₀ r) ((fun (i : ι) ↦ (φ i).rOut) i))
⊢ Tendsto (fun (i : ι) ↦ ∫ (t : G), (φ i).normed μ (x₀ - t) • g t ∂μ) l (𝓝 (g x₀))

Tactic:
apply tendsto_integral_smul_of_tendsto_average_norm_sub (K ^ (Module.finrank ℝ G)) this

Premises used: Real, MeasureTheory.tendsto_integral_smul_of_tendsto_average_norm_sub, HPow.hPow, Module.finrank
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : NormedSpace ℝ E'
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace ℝ G
inst_5 : CompleteSpace E'
inst_6 : BorelSpace G
inst_7 : FiniteDimensional ℝ G
inst_8 : μ.IsAddHaarMeasure
ι : Type u_1
φ : ι → ContDiffBump.{uG} (E := G) 0
l : Filter ι
K : ℝ
hφ : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g μ
x₀ : G
h₀ :
  Tendsto (β := ℝ) (fun (a : Set G) ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ)
    (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
hφ' : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝[>] 0)
this :
  Tendsto (β := ℝ)
    (Function.comp (β := ℝ) ((fun (a : Set G) ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ∘ fun (r : ℝ) ↦ closedBall x₀ r)
      fun (i : ι) ↦ (φ i).rOut)
    l (𝓝 0)
i : ι
⊢ IntegrableOn g (closedBall x₀ (φ i).rOut) μ

Tactic:
hg.integrableOn_isCompact (isCompact_closedBall _ _)

Premises used: MeasureTheory.LocallyIntegrable.integrableOn_isCompact, ProperSpace.isCompact_closedBall
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : NormedSpace ℝ E'
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace ℝ G
inst_5 : CompleteSpace E'
inst_6 : BorelSpace G
inst_7 : FiniteDimensional ℝ G
inst_8 : μ.IsAddHaarMeasure
ι : Type u_1
φ : ι → ContDiffBump.{uG} (E := G) 0
l : Filter ι
K : ℝ
hφ : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g μ
x₀ : G
h₀ :
  Tendsto (β := ℝ) (fun (a : Set G) ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ)
    (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
hφ' : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝[>] 0)
this :
  Tendsto (β := ℝ)
    (Function.comp (β := ℝ) ((fun (a : Set G) ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ∘ fun (r : ℝ) ↦ closedBall x₀ r)
      fun (i : ι) ↦ (φ i).rOut)
    l (𝓝 0)
h :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x : ι | (fun (i : ι) ↦ IntegrableOn g ((fun (r : ℝ) ↦ closedBall x₀ r) ((fun (i : ι) ↦ (φ i).rOut) i)) μ) x} a
h₁ h₂ : ∀ (i : ι), IntegrableOn g (closedBall x₀ (φ i).rOut) μ
⊢ ∀ᶠ (i : ι) in l, IntegrableOn g ((fun (r : ℝ) ↦ closedBall x₀ r) ((fun (i : ι) ↦ (φ i).rOut) i)) μ

Tactic:
filter_upwards with i using
      hg.integrableOn_isCompact (isCompact_closedBall _ _)

Premises used: MeasureTheory.LocallyIntegrable.integrableOn_isCompact, ProperSpace.isCompact_closedBall
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : NormedSpace ℝ E'
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace ℝ G
inst_5 : CompleteSpace E'
inst_6 : BorelSpace G
inst_7 : FiniteDimensional ℝ G
inst_8 : μ.IsAddHaarMeasure
ι : Type u_1
φ : ι → ContDiffBump.{uG} (E := G) 0
l : Filter ι
K : ℝ
hφ : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g μ
x₀ : G
h₀ :
  Tendsto (β := ℝ) (fun (a : Set G) ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ)
    (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
hφ' : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝[>] 0)
this :
  Tendsto (β := ℝ)
    (Function.comp (β := ℝ) ((fun (a : Set G) ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ∘ fun (r : ℝ) ↦ closedBall x₀ r)
      fun (i : ι) ↦ (φ i).rOut)
    l (𝓝 0)
apply : ∀ (i : ι), Eq (α := ℝ) 1 (∫ (y : G), (φ i).normed μ (x₀ - y) ∂μ)
⊢ Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : G), (φ i).normed μ (x₀ - y) ∂μ) l (𝓝 1)

Tactic:
apply tendsto_const_nhds.congr (fun i ↦ ?_)

Premises used: tendsto_const_nhds, Filter.Tendsto.congr
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : NormedSpace ℝ E'
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace ℝ G
inst_5 : CompleteSpace E'
inst_6 : BorelSpace G
inst_7 : FiniteDimensional ℝ G
inst_8 : μ.IsAddHaarMeasure
ι : Type u_1
φ : ι → ContDiffBump.{uG} (E := G) 0
l : Filter ι
K : ℝ
hφ : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g μ
x₀ : G
h₀ :
  Tendsto (β := ℝ) (fun (a : Set G) ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ)
    (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
hφ' : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝[>] 0)
this :
  Tendsto (β := ℝ)
    (Function.comp (β := ℝ) ((fun (a : Set G) ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ∘ fun (r : ℝ) ↦ closedBall x₀ r)
      fun (i : ι) ↦ (φ i).rOut)
    l (𝓝 0)
i : ι
rw : Eq (α := ℝ) 1 (∫ (x : G), (φ i).normed μ (x₀ - -x) ∂μ)
⊢ Eq (α := ℝ) 1 (∫ (y : G), (φ i).normed μ (x₀ - y) ∂μ)

Tactic:
rw [← integral_neg_eq_self]

Premises used: MeasureTheory.integral_neg_eq_self
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : NormedSpace ℝ E'
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace ℝ G
inst_5 : CompleteSpace E'
inst_6 : BorelSpace G
inst_7 : FiniteDimensional ℝ G
inst_8 : μ.IsAddHaarMeasure
ι : Type u_1
φ : ι → ContDiffBump.{uG} (E := G) 0
l : Filter ι
K : ℝ
hφ : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g μ
x₀ : G
h₀ :
  Tendsto (β := ℝ) (fun (a : Set G) ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ)
    (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
hφ' : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝[>] 0)
this :
  Tendsto (β := ℝ)
    (Function.comp (β := ℝ) ((fun (a : Set G) ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ∘ fun (r : ℝ) ↦ closedBall x₀ r)
      fun (i : ι) ↦ (φ i).rOut)
    l (𝓝 0)
i : ι
⊢ Eq (α := ℝ) 1 (∫ (x : G), (φ i).normed μ (x₀ - -x) ∂μ)

Tactic:
simp only [sub_neg_eq_add, integral_add_left_eq_self, integral_normed]

Premises used: ContDiffBump.integral_normed, MeasureTheory.integral_add_left_eq_self, sub_neg_eq_add