-- Mathlib/Analysis/Convolution.lean
theorem _root_.BddAbove.continuous_convolution_right_of_integrable
    [FirstCountableTopology G] [SecondCountableTopologyEither G E']
    (hbg : BddAbove (range fun x => ‖g x‖)) (hf : Integrable 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
inst✝¹ : FirstCountableTopology G
inst✝ : SecondCountableTopologyEither G E'
hbg : BddAbove (range fun x => ‖g x‖)
hf : Integrable f μ
hg : Continuous g
x₀ : G
this : ∀ᶠ (x : G) in 𝓝 x₀, ∀ᵐ (t : G) ∂μ, ‖(L (f t)) (g (x - t))‖ ≤ ‖L‖ * ‖f t‖ * ⨆ i, ‖g i‖
⊢ ContinuousAt (f ⋆[L, μ] g) x₀

Tactic:
refine continuousAt_of_dominated ?_ this ?_ ?_

Result:
case refine_1
𝕜 : 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
inst✝¹ : FirstCountableTopology G
inst✝ : SecondCountableTopologyEither G E'
hbg : BddAbove (range fun x => ‖g x‖)
hf : Integrable f μ
hg : Continuous g
x₀ : G
this : ∀ᶠ (x : G) in 𝓝 x₀, ∀ᵐ (t : G) ∂μ, ‖(L (f t)) (g (x - t))‖ ≤ ‖L‖ * ‖f t‖ * ⨆ i, ‖g i‖
⊢ ∀ᶠ (x : G) in 𝓝 x₀, AEStronglyMeasurable (fun a => (L (f a)) (g (x - a))) μ

case refine_2
𝕜 : 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
inst✝¹ : FirstCountableTopology G
inst✝ : SecondCountableTopologyEither G E'
hbg : BddAbove (range fun x => ‖g x‖)
hf : Integrable f μ
hg : Continuous g
x₀ : G
this : ∀ᶠ (x : G) in 𝓝 x₀, ∀ᵐ (t : G) ∂μ, ‖(L (f t)) (g (x - t))‖ ≤ ‖L‖ * ‖f t‖ * ⨆ i, ‖g i‖
⊢ Integrable (fun a => ‖L‖ * ‖f a‖ * ⨆ i, ‖g i‖) μ

case refine_3
𝕜 : 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
inst✝¹ : FirstCountableTopology G
inst✝ : SecondCountableTopologyEither G E'
hbg : BddAbove (range fun x => ‖g x‖)
hf : Integrable f μ
hg : Continuous g
x₀ : G
this : ∀ᶠ (x : G) in 𝓝 x₀, ∀ᵐ (t : G) ∂μ, ‖(L (f t)) (g (x - t))‖ ≤ ‖L‖ * ‖f t‖ * ⨆ i, ‖g i‖
⊢ ∀ᵐ (a : G) ∂μ, ContinuousAt (fun x => (L (f a)) (g (x - a))) x₀

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
inst✝¹ : FirstCountableTopology G
inst✝ : SecondCountableTopologyEither G E'
hbg : BddAbove (range fun x => ‖g x‖)
hf : Integrable f μ
hg : Continuous g
x₀ : G
⊢ ∀ᶠ (x : G) in 𝓝 x₀, ∀ᵐ (t : G) ∂μ, ‖(L (f t)) (g (x - t))‖ ≤ ‖L‖ * ‖f t‖ * ⨆ i, ‖g i‖

Tactic:
filter_upwards with x

Result:
case 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✝⁶ : NormedSpace ℝ F
inst✝⁵ : AddGroup G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalAddGroup G
inst✝² : BorelSpace G
inst✝¹ : FirstCountableTopology G
inst✝ : SecondCountableTopologyEither G E'
hbg : BddAbove (range fun x => ‖g x‖)
hf : Integrable f μ
hg : Continuous g
x₀ x : G
⊢ ∀ᵐ (t : G) ∂μ, ‖(L (f t)) (g (x - t))‖ ≤ ‖L‖ * ‖f t‖ * ⨆ i, ‖g i‖

Proof state:
case h.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✝⁶ : NormedSpace ℝ F
inst✝⁵ : AddGroup G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalAddGroup G
inst✝² : BorelSpace G
inst✝¹ : FirstCountableTopology G
inst✝ : SecondCountableTopologyEither G E'
hbg : BddAbove (range fun x => ‖g x‖)
hf : Integrable f μ
hg : Continuous g
x₀ x t : G
⊢ ‖(L (f t)) (g (x - t))‖ ≤ ‖L‖ * ‖f t‖ * ⨆ i, ‖g i‖

Tactic:
apply_rules [L.le_of_opNorm₂_le_of_le, le_rfl, le_ciSup hbg (x - t)]

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
inst✝¹ : FirstCountableTopology G
inst✝ : SecondCountableTopologyEither G E'
hbg : BddAbove (range fun x => ‖g x‖)
hf : Integrable f μ
hg : Continuous g
x₀ : G
⊢ ContinuousAt (f ⋆[L, μ] g) x₀

Tactic:
have : ∀ᶠ x in 𝓝 x₀, ∀ᵐ t : G ∂μ, ‖L (f t) (g (x - t))‖ ≤ ‖L‖ * ‖f t‖ * ⨆ i, ‖g i‖ := by
  filter_upwards with x; filter_upwards with t
  apply_rules [L.le_of_opNorm₂_le_of_le, le_rfl, le_ciSup hbg (x - t)]

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
inst✝¹ : FirstCountableTopology G
inst✝ : SecondCountableTopologyEither G E'
hbg : BddAbove (range fun x => ‖g x‖)
hf : Integrable f μ
hg : Continuous g
x₀ : G
this : ∀ᶠ (x : G) in 𝓝 x₀, ∀ᵐ (t : G) ∂μ, ‖(L (f t)) (g (x - t))‖ ≤ ‖L‖ * ‖f t‖ * ⨆ i, ‖g i‖
⊢ ContinuousAt (f ⋆[L, μ] g) x₀