-- Mathlib/Analysis/Calculus/BumpFunction/Convolution.lean
theorem ae_convolution_tendsto_right_of_locallyIntegrable
    {ι} {φ : ι → ContDiffBump (0 : G)} {l : Filter ι} {K : ℝ}
    (hφ : Tendsto (fun i ↦ (φ i).rOut) l (𝓝 0))
    (h'φ : ∀ᶠ i in l, (φ i).rOut ≤ K * (φ i).rIn) (hg : LocallyIntegrable g μ) : ∀ᵐ x₀ ∂μ,
    Tendsto (fun i ↦ ((φ i).normed μ ⋆[lsmul ℝ ℝ, μ] g) x₀) l (𝓝 (g x₀))

Proof state:
case h
G : Type uG
E' : Type uE'
inst✝¹¹ : NormedAddCommGroup E'
g : G → E'
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedSpace ℝ E'
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : HasContDiffBump G
inst✝⁵ : CompleteSpace E'
inst✝⁴ : BorelSpace G
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : μ.IsOpenPosMeasure
inst✝¹ : FiniteDimensional ℝ G
inst✝ : μ.IsAddLeftInvariant
ι : Type u_1
φ : ι → ContDiffBump 0
l : Filter ι
K : ℝ
hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g μ
this : μ.IsAddHaarMeasure
x₀ : G
h₀ : Tendsto (fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ((Besicovitch.vitaliFamily μ).filterAt x₀) (𝓝 0)
⊢ Tendsto (fun i => ∫ (t : G), (φ i).normed μ (x₀ - t) • g t ∂μ) l (𝓝 (g x₀))

Tactic:
have hφ' : Tendsto (fun i ↦ (φ i).rOut) l (𝓝[>] 0) :=
  tendsto_nhdsWithin_iff.2 ⟨hφ, Eventually.of_forall (fun i ↦ (φ i).rOut_pos)⟩

Result:
case h
G : Type uG
E' : Type uE'
inst✝¹¹ : NormedAddCommGroup E'
g : G → E'
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedSpace ℝ E'
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : HasContDiffBump G
inst✝⁵ : CompleteSpace E'
inst✝⁴ : BorelSpace G
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : μ.IsOpenPosMeasure
inst✝¹ : FiniteDimensional ℝ G
inst✝ : μ.IsAddLeftInvariant
ι : Type u_1
φ : ι → ContDiffBump 0
l : Filter ι
K : ℝ
hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g μ
this : μ.IsAddHaarMeasure
x₀ : G
h₀ : Tendsto (fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ((Besicovitch.vitaliFamily μ).filterAt x₀) (𝓝 0)
hφ' : Tendsto (fun i => (φ i).rOut) l (𝓝[>] 0)
⊢ Tendsto (fun i => ∫ (t : G), (φ i).normed μ (x₀ - t) • g t ∂μ) l (𝓝 (g x₀))

Proof state:
case h.f_int
G : Type uG
E' : Type uE'
inst✝¹¹ : NormedAddCommGroup E'
g : G → E'
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedSpace ℝ E'
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : HasContDiffBump G
inst✝⁵ : CompleteSpace E'
inst✝⁴ : BorelSpace G
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : μ.IsOpenPosMeasure
inst✝¹ : FiniteDimensional ℝ G
inst✝ : μ.IsAddLeftInvariant
ι : Type u_1
φ : ι → ContDiffBump 0
l : Filter ι
K : ℝ
hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g μ
this✝ : μ.IsAddHaarMeasure
x₀ : G
h₀ : Tendsto (fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ((Besicovitch.vitaliFamily μ).filterAt x₀) (𝓝 0)
hφ' : Tendsto (fun i => (φ i).rOut) l (𝓝[>] 0)
this : Tendsto (((fun a => ⨍ (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)) μ

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

Result:
no goals

Proof state:
case h.g_supp.h
G : Type uG
E' : Type uE'
inst✝¹¹ : NormedAddCommGroup E'
g : G → E'
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedSpace ℝ E'
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : HasContDiffBump G
inst✝⁵ : CompleteSpace E'
inst✝⁴ : BorelSpace G
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : μ.IsOpenPosMeasure
inst✝¹ : FiniteDimensional ℝ G
inst✝ : μ.IsAddLeftInvariant
ι : Type u_1
φ : ι → ContDiffBump 0
l : Filter ι
K : ℝ
hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g μ
this✝ : μ.IsAddHaarMeasure
x₀ : G
h₀ : Tendsto (fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ((Besicovitch.vitaliFamily μ).filterAt x₀) (𝓝 0)
hφ' : Tendsto (fun i => (φ i).rOut) l (𝓝[>] 0)
this : Tendsto (((fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ∘ fun r => closedBall x₀ r) ∘ fun i => (φ i).rOut) l (𝓝 0)
i : ι
x : G
hx : ‖x₀ - x‖ < (φ i).rOut
⊢ x ∈ closedBall x₀ (φ i).rOut

Tactic:
simpa [dist_eq_norm_sub'] using hx.le

Result:
no goals

Proof state:
case h.g_supp.h
G : Type uG
E' : Type uE'
inst✝¹¹ : NormedAddCommGroup E'
g : G → E'
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedSpace ℝ E'
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : HasContDiffBump G
inst✝⁵ : CompleteSpace E'
inst✝⁴ : BorelSpace G
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : μ.IsOpenPosMeasure
inst✝¹ : FiniteDimensional ℝ G
inst✝ : μ.IsAddLeftInvariant
ι : Type u_1
φ : ι → ContDiffBump 0
l : Filter ι
K : ℝ
hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g μ
this✝ : μ.IsAddHaarMeasure
x₀ : G
h₀ : Tendsto (fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ((Besicovitch.vitaliFamily μ).filterAt x₀) (𝓝 0)
hφ' : Tendsto (fun i => (φ i).rOut) l (𝓝[>] 0)
this : Tendsto (((fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ∘ fun r => closedBall x₀ r) ∘ fun i => (φ i).rOut) l (𝓝 0)
i : ι
x : G
hx : x ∈ (fun y => x₀ - y) ⁻¹' ball 0 (φ i).rOut
⊢ x ∈ closedBall x₀ (φ i).rOut

Tactic:
simp only [mem_preimage, mem_ball, dist_zero_right] at hx

Result:
case h.g_supp.h
G : Type uG
E' : Type uE'
inst✝¹¹ : NormedAddCommGroup E'
g : G → E'
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedSpace ℝ E'
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : HasContDiffBump G
inst✝⁵ : CompleteSpace E'
inst✝⁴ : BorelSpace G
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : μ.IsOpenPosMeasure
inst✝¹ : FiniteDimensional ℝ G
inst✝ : μ.IsAddLeftInvariant
ι : Type u_1
φ : ι → ContDiffBump 0
l : Filter ι
K : ℝ
hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g μ
this✝ : μ.IsAddHaarMeasure
x₀ : G
h₀ : Tendsto (fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ((Besicovitch.vitaliFamily μ).filterAt x₀) (𝓝 0)
hφ' : Tendsto (fun i => (φ i).rOut) l (𝓝[>] 0)
this : Tendsto (((fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ∘ fun r => closedBall x₀ r) ∘ fun i => (φ i).rOut) l (𝓝 0)
i : ι
x : G
hx : ‖x₀ - x‖ < (φ i).rOut
⊢ x ∈ closedBall x₀ (φ i).rOut