-- Mathlib/Analysis/Convolution.lean
theorem _root_.HasCompactSupport.continuous_convolution_right (hcg : HasCompactSupport g)
    (hf : LocallyIntegrable f μ) (hg : Continuous g) : Continuous (f ⋆[L, μ] g)

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✝⁴ : NormedSpace ℝ F
inst✝³ : AddGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : BorelSpace G
hcg : HasCompactSupport g
hf : LocallyIntegrable f μ
hg : Continuous g
⊢ Continuous (f ⋆[L, μ] g)

Tactic:
rw [continuous_iff_continuousOn_univ]

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✝⁴ : NormedSpace ℝ F
inst✝³ : AddGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : BorelSpace G
hcg : HasCompactSupport g
hf : LocallyIntegrable f μ
hg : Continuous g
⊢ ContinuousOn (f ⋆[L, μ] g) univ

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✝⁴ : NormedSpace ℝ F
inst✝³ : AddGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : BorelSpace G
hcg : HasCompactSupport g
hf : LocallyIntegrable f μ
hg : Continuous g
g' : G → G → E' := fun x q => g q
this : ContinuousOn (↿g') (univ ×ˢ univ)
⊢ ContinuousOn (f ⋆[L, μ] g) univ

Tactic:
exact continuousOn_convolution_right_with_param_comp L
  (continuous_iff_continuousOn_univ.1 continuous_id) hcg
  (fun p x _ hx => image_eq_zero_of_nmem_tsupport hx) hf this

Result:
no goals

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✝⁴ : NormedSpace ℝ F
inst✝³ : AddGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : BorelSpace G
hcg : HasCompactSupport g
hf : LocallyIntegrable f μ
hg : Continuous g
g' : G → G → E' := fun x q => g q
⊢ ContinuousOn (f ⋆[L, μ] g) univ

Tactic:
have : ContinuousOn (↿g') (univ ×ˢ univ) := (hg.comp continuous_snd).continuousOn

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✝⁴ : NormedSpace ℝ F
inst✝³ : AddGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : BorelSpace G
hcg : HasCompactSupport g
hf : LocallyIntegrable f μ
hg : Continuous g
g' : G → G → E' := fun x q => g q
this : ContinuousOn (↿g') (univ ×ˢ univ)
⊢ ContinuousOn (f ⋆[L, μ] g) univ

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✝⁴ : NormedSpace ℝ F
inst✝³ : AddGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : BorelSpace G
hcg : HasCompactSupport g
hf : LocallyIntegrable f μ
hg : Continuous g
⊢ ContinuousOn (f ⋆[L, μ] g) univ

Tactic:
let g' : G → G → E' := fun _ q => g q

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✝⁴ : NormedSpace ℝ F
inst✝³ : AddGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : BorelSpace G
hcg : HasCompactSupport g
hf : LocallyIntegrable f μ
hg : Continuous g
g' : G → G → E' := fun x q => g q
⊢ ContinuousOn (f ⋆[L, μ] g) univ