-- 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:
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 μ
⊢ ∀ᵐ (x₀ : G) ∂μ, Tendsto (fun i => ((φ i).normed μ ⋆[lsmul ℝ ℝ, μ] g) x₀) l (𝓝 (g x₀))

Tactic:
have : IsAddHaarMeasure μ := ⟨⟩

Result:
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) ∂μ, 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 => ((φ i).normed μ ⋆[lsmul ℝ ℝ, μ] g) x₀) l (𝓝 (g x₀))

Tactic:
simp only [convolution_eq_swap, lsmul_apply]

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)
⊢ Tendsto (fun i => ∫ (t : G), (φ i).normed μ (x₀ - t) • g t ∂μ) l (𝓝 (g x₀))

Proof state:
case h.hg
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)
⊢ Tendsto (fun i => ∫ (y : G), (φ i).normed μ (x₀ - y) ∂μ) l (𝓝 1)

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

Result:
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 : ι
⊢ 1 = ∫ (y : G), (φ i).normed μ (x₀ - y) ∂μ

Proof state:
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 : ι
⊢ 1 = ∫ (y : G), (φ i).normed μ (x₀ - y) ∂μ

Tactic:
rw [← integral_neg_eq_self]

Result:
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 : ι
⊢ 1 = ∫ (x : G), (φ i).normed μ (x₀ - -x) ∂μ