awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
hx : x ∈ ball c f.rOut
rwa : ∀ (hx : x ∈ support (↑f : E → ℝ)), (↑f : E → ℝ) x ≠ 0
⊢ (↑f : E → ℝ) x ≠ 0
have rwa₁ : ∀ (hx : (↑f : E → ℝ) x ≠ 0), (↑f : E → ℝ) x ≠ 0
Tactic: rwa [← support_eq, mem_support] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
hx : f.rOut ≤ dist x c
⊢ (↑f : E → ℝ) x = 0
have rwa : x ∉ support (↑f : E → ℝ)
Tactic: rwa [← notMem_support, support_eq, mem_ball, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
hx : f.rOut ≤ dist x c
rwa : x ∉ support (↑f : E → ℝ)
⊢ (↑f : E → ℝ) x = 0
have rwa₁ : x ∉ ball c f.rOut
Tactic: rwa [← notMem_support, support_eq, mem_ball, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
hx : f.rOut ≤ dist x c
rwa : x ∉ support (↑f : E → ℝ)
rwa₁ : x ∉ ball c f.rOut
⊢ (↑f : E → ℝ) x = 0
have rwa₂ : ¬dist x c < f.rOut
Tactic: rwa [← notMem_support, support_eq, mem_ball, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
c : E
f : ContDiffBump c
inst_3 : FiniteDimensional ℝ E
⊢ HasCompactSupport (↑f : E → ℝ)
have simp_rw : IsCompact (tsupport (↑f : E → ℝ))
Tactic: simp_rw [HasCompactSupport, f.tsupport_eq, isCompact_closedBall]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
c : E
f : ContDiffBump c
inst_3 : FiniteDimensional ℝ E
simp_rw : IsCompact (tsupport (↑f : E → ℝ))
⊢ HasCompactSupport (↑f : E → ℝ)
have simp_rw₁ : IsCompact (closedBall c f.rOut)
Tactic: simp_rw [HasCompactSupport, f.tsupport_eq, isCompact_closedBall]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Basic (goal)
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 ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : X) ↦ (↑(f x) : E → ℝ) (g x)) s x
have change : ContDiffWithinAt ℝ (↑n : ℕ∞ω)
  (uncurry (ContDiffBumpBase.toFun (someContDiffBumpBase E)) ∘ fun (x : X) ↦
    ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x)))
  s x
Tactic: change ContDiffWithinAt ℝ n (uncurry (someContDiffBumpBase E).toFun ∘ fun x : X =>
    ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x))) s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Basic (goal)
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 ℝ (↑n : ℕ∞ω)
    (uncurry (ContDiffBumpBase.toFun (someContDiffBumpBase E)) ∘ fun (x : X) ↦
      ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x)))
    s x
have refine_1 : SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ ∈ 𝓝 ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x))
Tactic: refine (((someContDiffBumpBase E).smooth.contDiffAt ?_).of_le
    (mod_cast le_top)).comp_contDiffWithinAt x ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Basic (goal)
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
refine_1 : SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ ∈ 𝓝 ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x))
⊢ ContDiffWithinAt ℝ (↑n : ℕ∞ω)
    (uncurry (ContDiffBumpBase.toFun (someContDiffBumpBase E)) ∘ fun (x : X) ↦
      ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x)))
    s x
have refine_2 : 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: refine (((someContDiffBumpBase E).smooth.contDiffAt ?_).of_le
    (mod_cast le_top)).comp_contDiffWithinAt x ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Basic (goal)
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
⊢ ContDiff ℝ (F := ℝ) (↑n : ℕ∞ω) fun (x : X) ↦ (↑(f x) : E → ℝ) (g x)
have 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
Tactic: rw [contDiff_iff_contDiffAt] at *
Cleared hypotheses: hc, hr, hR, hg
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Convolution (goal)
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₀
⊢ ((↑φ : G → ℝ) ⋆[lsmul ℝ ℝ, μ] g) x₀ = integral μ (↑φ : G → ℝ) • g x₀
have simp_rw : ∫ (t : G), (((lsmul ℝ ℝ : (a : ℝ) → E' →L[ℝ] E') ((↑φ : G → ℝ) t) : E' →L[ℝ] E') : (a : E') → E') (g x₀) ∂μ =
  integral μ (↑φ : G → ℝ) • g x₀
Tactic: simp_rw [convolution_eq_right' _ φ.support_eq.subset hg, lsmul_apply, integral_smul_const]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Convolution (goal)
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₀
⊢ ((↑φ : G → ℝ) ⋆[lsmul ℝ ℝ, μ] g) x₀ = integral μ (↑φ : G → ℝ) • g x₀
have simp_rw₁ : ∫ (t : G), (↑φ : G → ℝ) t • g x₀ ∂μ = integral μ (↑φ : G → ℝ) • g x₀
Tactic: simp_rw [convolution_eq_right' _ φ.support_eq.subset hg, lsmul_apply, integral_smul_const]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Convolution (goal)
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₀
⊢ (φ.normed μ ⋆[lsmul ℝ ℝ, μ] g) x₀ = g x₀
have rw : ∫ (t : G), (((lsmul ℝ ℝ : (a : ℝ) → E' →L[ℝ] E') (φ.normed μ t) : E' →L[ℝ] E') : (a : E') → E') (g x₀) ∂μ = g x₀
Tactic: rw [convolution_eq_right' _ φ.support_normed_eq.subset hg]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Convolution (goal)
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₀) ≤ ε
⊢ 0 ≤ ε
have simp_rw : dist (g x₀) (g x₀) ≤ ε
Tactic: simp_rw [← dist_self (g x₀), hg x₀ (mem_ball_self φ.rOut_pos)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Convolution (goal)
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) ∂μ, Tendsto (fun (i : ι) ↦ ((φ i).normed μ ⋆[lsmul ℝ ℝ, μ] g) x₀) l (𝓝 (g x₀))
have 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₀))
Tactic: filter_upwards [(Besicovitch.vitaliFamily μ).ae_tendsto_average_norm_sub hg] with x₀ h₀
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Convolution (goal)
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).normed μ ⋆[lsmul ℝ ℝ, μ] g) x₀) l (𝓝 (g x₀))
have h : Tendsto (fun (i : ι) ↦ ∫ (t : G), (φ i).normed μ (x₀ - t) • g t ∂μ) l (𝓝 (g x₀))
Tactic: simp only [convolution_eq_swap, lsmul_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Convolution (hypothesis)
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 : ι) ↦ ∫ (t : G), (φ i).normed μ (x₀ - t) • g t ∂μ) l (𝓝 (g x₀))
have hφ' : 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)⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Convolution (hypothesis)
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 (fun (i : ι) ↦ ∫ (t : G), (φ i).normed μ (x₀ - t) • g t ∂μ) l (𝓝 (g x₀))
have 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)
Tactic: have := (h₀.comp (Besicovitch.tendsto_filterAt μ x₀)).comp hφ'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Convolution (goal)
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)
⊢ Tendsto (fun (i : ι) ↦ ∫ (t : G), (φ i).normed μ (x₀ - t) • g t ∂μ) l (𝓝 (g x₀))
have h : ∀ᶠ (i : ι) in l, IntegrableOn g ((fun (r : ℝ) ↦ closedBall x₀ r) ((fun (i : ι) ↦ (φ i).rOut) i)) μ
Tactic: apply tendsto_integral_smul_of_tendsto_average_norm_sub (K ^ (Module.finrank ℝ G)) this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Convolution (goal)
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)) μ
⊢ Tendsto (fun (i : ι) ↦ ∫ (t : G), (φ i).normed μ (x₀ - t) • g t ∂μ) l (𝓝 (g x₀))
have h₁ : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : G), (φ i).normed μ (x₀ - y) ∂μ) l (𝓝 1)
Tactic: apply tendsto_integral_smul_of_tendsto_average_norm_sub (K ^ (Module.finrank ℝ G)) this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Convolution (goal)
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)
⊢ Tendsto (fun (i : ι) ↦ ∫ (t : G), (φ i).normed μ (x₀ - t) • g t ∂μ) l (𝓝 (g x₀))
have 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))
Tactic: apply tendsto_integral_smul_of_tendsto_average_norm_sub (K ^ (Module.finrank ℝ G)) this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Convolution (goal)
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))
⊢ Tendsto (fun (i : ι) ↦ ∫ (t : G), (φ i).normed μ (x₀ - t) • g t ∂μ) l (𝓝 (g x₀))
have 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))
Tactic: apply tendsto_integral_smul_of_tendsto_average_norm_sub (K ^ (Module.finrank ℝ G)) this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Convolution (goal)
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 : ι) in l, IntegrableOn g ((fun (r : ℝ) ↦ closedBall x₀ r) ((fun (i : ι) ↦ (φ i).rOut) i)) μ
have h : ∀ (a : ι),
  Membership.mem (γ := Set ι)
    {x : ι | (fun (i : ι) ↦ IntegrableOn g ((fun (r : ℝ) ↦ closedBall x₀ r) ((fun (i : ι) ↦ (φ i).rOut) i)) μ) x} a
Tactic: filter_upwards with i using
      hg.integrableOn_isCompact (isCompact_closedBall _ _)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Convolution (goal)
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
⊢ ∀ᶠ (i : ι) in l, IntegrableOn g ((fun (r : ℝ) ↦ closedBall x₀ r) ((fun (i : ι) ↦ (φ i).rOut) i)) μ
have h₁ : ∀ (a : ι), IntegrableOn g (closedBall x₀ (φ a).rOut) μ
Tactic: filter_upwards with i using
      hg.integrableOn_isCompact (isCompact_closedBall _ _)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Convolution (goal)
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)
⊢ Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : G), (φ i).normed μ (x₀ - y) ∂μ) l (𝓝 1)
have apply : ∀ (i : ι), Eq (α := ℝ) 1 (∫ (y : G), (φ i).normed μ (x₀ - y) ∂μ)
Tactic: apply tendsto_const_nhds.congr (fun i ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Convolution (goal)
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 (∫ (y : G), (φ i).normed μ (x₀ - y) ∂μ)
have rw : Eq (α := ℝ) 1 (∫ (x : G), (φ i).normed μ (x₀ - -x) ∂μ)
Tactic: rw [← integral_neg_eq_self]