-- Mathlib/Analysis/Convolution.lean
theorem _root_.HasCompactSupport.convolutionExistsAt {x₀ : G}
    (h : HasCompactSupport fun t => L (f t) (g (x₀ - t))) (hf : LocallyIntegrable f μ)
    (hg : Continuous g) : ConvolutionExistsAt f g x₀ L μ

Proof state:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup E'
inst✝⁹ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace 𝕜 E'
inst✝⁵ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁴ : MeasurableSpace G
μ : Measure G
inst✝³ : AddGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : BorelSpace G
x₀ : G
h : HasCompactSupport fun t => (L (f t)) (g (x₀ - t))
hf : LocallyIntegrable f μ
hg : Continuous g
u : G ≃ₜ G := (Homeomorph.neg G).trans (Homeomorph.addRight x₀)
v : G ≃ₜ G := (Homeomorph.neg G).trans (Homeomorph.addLeft x₀)
A : AEStronglyMeasurable (g ∘ ⇑v) (μ.restrict (tsupport fun t => (L (f t)) (g (x₀ - t))))
⊢ AEStronglyMeasurable g
    (Measure.map (fun t => ↑(toAddUnits x₀) - t) (μ.restrict (tsupport fun t => (L (f t)) (g (x₀ - t)))))

Tactic:
convert ((v.continuous.measurable.measurePreserving
    (μ.restrict (tsupport fun t => L (f t) (g (x₀ - t))))).aestronglyMeasurable_comp_iff
  v.measurableEmbedding).1 A

Result:
case h.e'_7.h.e'_5.h.h.e
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup E'
inst✝⁹ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace 𝕜 E'
inst✝⁵ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁴ : MeasurableSpace G
μ : Measure G
inst✝³ : AddGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : BorelSpace G
x₀ : G
h : HasCompactSupport fun t => (L (f t)) (g (x₀ - t))
hf : LocallyIntegrable f μ
hg : Continuous g
u : G ≃ₜ G := (Homeomorph.neg G).trans (Homeomorph.addRight x₀)
v : G ≃ₜ G := (Homeomorph.neg G).trans (Homeomorph.addLeft x₀)
A : AEStronglyMeasurable (g ∘ ⇑v) (μ.restrict (tsupport fun t => (L (f t)) (g (x₀ - t))))
x✝ : G
⊢ HSub.hSub ↑(toAddUnits x₀) = ⇑v

Proof state:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup E'
inst✝⁹ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace 𝕜 E'
inst✝⁵ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁴ : MeasurableSpace G
μ : Measure G
inst✝³ : AddGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : BorelSpace G
x₀ : G
h : HasCompactSupport fun t => (L (f t)) (g (x₀ - t))
hf : LocallyIntegrable f μ
hg : Continuous g
u : G ≃ₜ G := (Homeomorph.neg G).trans (Homeomorph.addRight x₀)
v : G ≃ₜ G := (Homeomorph.neg G).trans (Homeomorph.addLeft x₀)
⊢ ConvolutionExistsAt f g x₀ L μ

Tactic:
apply ((u.isCompact_preimage.mpr h).bddAbove_image hg.norm.continuousOn).convolutionExistsAt' L
  isClosed_closure.measurableSet subset_closure (hf.integrableOn_isCompact h)

Result:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup E'
inst✝⁹ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace 𝕜 E'
inst✝⁵ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁴ : MeasurableSpace G
μ : Measure G
inst✝³ : AddGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : BorelSpace G
x₀ : G
h : HasCompactSupport fun t => (L (f t)) (g (x₀ - t))
hf : LocallyIntegrable f μ
hg : Continuous g
u : G ≃ₜ G := (Homeomorph.neg G).trans (Homeomorph.addRight x₀)
v : G ≃ₜ G := (Homeomorph.neg G).trans (Homeomorph.addLeft x₀)
⊢ AEStronglyMeasurable g
    (Measure.map (fun t => ↑(toAddUnits x₀) - t) (μ.restrict (tsupport fun t => (L (f t)) (g (x₀ - t)))))

Proof state:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup E'
inst✝⁹ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace 𝕜 E'
inst✝⁵ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁴ : MeasurableSpace G
μ : Measure G
inst✝³ : AddGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : BorelSpace G
x₀ : G
h : HasCompactSupport fun t => (L (f t)) (g (x₀ - t))
hf : LocallyIntegrable f μ
hg : Continuous g
u : G ≃ₜ G := (Homeomorph.neg G).trans (Homeomorph.addRight x₀)
v : G ≃ₜ G := (Homeomorph.neg G).trans (Homeomorph.addLeft x₀)
⊢ AEStronglyMeasurable g
    (Measure.map (fun t => ↑(toAddUnits x₀) - t) (μ.restrict (tsupport fun t => (L (f t)) (g (x₀ - t)))))

Tactic:
have A : AEStronglyMeasurable (g ∘ v)
    (μ.restrict (tsupport fun t : G => L (f t) (g (x₀ - t)))) := by
  apply (hg.comp v.continuous).continuousOn.aestronglyMeasurable_of_isCompact h
  exact (isClosed_tsupport _).measurableSet

Result:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup E'
inst✝⁹ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace 𝕜 E'
inst✝⁵ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁴ : MeasurableSpace G
μ : Measure G
inst✝³ : AddGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : BorelSpace G
x₀ : G
h : HasCompactSupport fun t => (L (f t)) (g (x₀ - t))
hf : LocallyIntegrable f μ
hg : Continuous g
u : G ≃ₜ G := (Homeomorph.neg G).trans (Homeomorph.addRight x₀)
v : G ≃ₜ G := (Homeomorph.neg G).trans (Homeomorph.addLeft x₀)
A : AEStronglyMeasurable (g ∘ ⇑v) (μ.restrict (tsupport fun t => (L (f t)) (g (x₀ - t))))
⊢ AEStronglyMeasurable g
    (Measure.map (fun t => ↑(toAddUnits x₀) - t) (μ.restrict (tsupport fun t => (L (f t)) (g (x₀ - t)))))

Proof state:
case h.e'_7.h.e'_5.h.h.e
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup E'
inst✝⁹ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace 𝕜 E'
inst✝⁵ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁴ : MeasurableSpace G
μ : Measure G
inst✝³ : AddGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : BorelSpace G
x₀ : G
h : HasCompactSupport fun t => (L (f t)) (g (x₀ - t))
hf : LocallyIntegrable f μ
hg : Continuous g
u : G ≃ₜ G := (Homeomorph.neg G).trans (Homeomorph.addRight x₀)
v : G ≃ₜ G := (Homeomorph.neg G).trans (Homeomorph.addLeft x₀)
A : AEStronglyMeasurable (g ∘ ⇑v) (μ.restrict (tsupport fun t => (L (f t)) (g (x₀ - t))))
x✝ : G
⊢ HSub.hSub ↑(toAddUnits x₀) = ⇑v

Tactic:
ext x

Result:
case h.e'_7.h.e'_5.h.h.e.h
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup E'
inst✝⁹ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace 𝕜 E'
inst✝⁵ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁴ : MeasurableSpace G
μ : Measure G
inst✝³ : AddGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : BorelSpace G
x₀ : G
h : HasCompactSupport fun t => (L (f t)) (g (x₀ - t))
hf : LocallyIntegrable f μ
hg : Continuous g
u : G ≃ₜ G := (Homeomorph.neg G).trans (Homeomorph.addRight x₀)
v : G ≃ₜ G := (Homeomorph.neg G).trans (Homeomorph.addLeft x₀)
A : AEStronglyMeasurable (g ∘ ⇑v) (μ.restrict (tsupport fun t => (L (f t)) (g (x₀ - t))))
x✝ x : G
⊢ ↑(toAddUnits x₀) - x = v x