-- Mathlib/Analysis/Convolution.lean
theorem dist_convolution_le' {x₀ : G} {R ε : ℝ} {z₀ : E'} (hε : 0 ≤ ε) (hif : Integrable f μ)
    (hf : support f ⊆ ball (0 : G) R) (hmg : AEStronglyMeasurable g μ)
    (hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε) :
    dist ((f ⋆[L, μ] g : G → F) x₀) (∫ t, L (f t) z₀ ∂μ) ≤ (‖L‖ * ∫ x, ‖f 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✝⁴ : SeminormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hfg : ConvolutionExistsAt f g x₀ L μ
h2 : ∀ (t : G), ‖(L (f t)) (g (x₀ - t)) - (L (f t)) z₀‖ ≤ ‖L (f t)‖ * ε
⊢ ∫ (a : G), ‖L (f a)‖ ∂μ ≤ ‖L‖ * ∫ (x : G), ‖f x‖ ∂μ

Tactic:
have h3 : ∀ t, ‖L (f t)‖ ≤ ‖L‖ * ‖f t‖ := by
  intro t
  exact L.le_opNorm (f 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✝⁴ : SeminormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hfg : ConvolutionExistsAt f g x₀ L μ
h2 : ∀ (t : G), ‖(L (f t)) (g (x₀ - t)) - (L (f t)) z₀‖ ≤ ‖L (f t)‖ * ε
h3 : ∀ (t : G), ‖L (f t)‖ ≤ ‖L‖ * ‖f t‖
⊢ ∫ (a : G), ‖L (f a)‖ ∂μ ≤ ‖L‖ * ∫ (x : G), ‖f x‖ ∂μ

Proof state:
case pos
𝕜 : 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✝⁴ : SeminormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hfg : ConvolutionExistsAt f g x₀ L μ
t : G
ht : t ∈ support f
h2t : ‖t‖ < R
hg : x₀ - t ∈ ball x₀ R → dist (g (x₀ - t)) z₀ ≤ ε
⊢ dist ((L (f t)) (g (x₀ - t))) ((L (f t)) z₀) ≤ ‖L (f t)‖ * ε

Tactic:
rw [sub_eq_add_neg, add_mem_ball_iff_norm, norm_neg, ← sub_eq_add_neg] at hg

Result:
case pos
𝕜 : 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✝⁴ : SeminormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hfg : ConvolutionExistsAt f g x₀ L μ
t : G
ht : t ∈ support f
h2t : ‖t‖ < R
hg : ‖t‖ < R → dist (g (x₀ - t)) z₀ ≤ ε
⊢ dist ((L (f t)) (g (x₀ - t))) ((L (f t)) z₀) ≤ ‖L (f 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✝⁵ : NormedSpace ℝ F
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hfg : ConvolutionExistsAt f g x₀ L μ
h2 : ∀ (t : G), ‖(L (f t)) (g (x₀ - t)) - (L (f t)) z₀‖ ≤ ‖L (f t)‖ * ε
t : G
⊢ ‖L (f t)‖ ≤ ‖L‖ * ‖f t‖

Tactic:
exact L.le_opNorm (f 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✝⁴ : SeminormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hfg : ConvolutionExistsAt f g x₀ L μ
h2 : ∀ (t : G), dist ((L (f t)) (g (x₀ - t))) ((L (f t)) z₀) ≤ ‖L (f t)‖ * ε
⊢ dist (∫ (t : G), (L (f t)) (g (x₀ - t)) ∂μ) (∫ (t : G), (L (f t)) z₀ ∂μ) ≤ (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε

Tactic:
simp_rw [dist_eq_norm] at h2 ⊢

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✝⁴ : SeminormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hfg : ConvolutionExistsAt f g x₀ L μ
h2 : ∀ (t : G), ‖(L (f t)) (g (x₀ - t)) - (L (f t)) z₀‖ ≤ ‖L (f t)‖ * ε
⊢ ‖∫ (t : G), (L (f t)) (g (x₀ - t)) ∂μ - ∫ (t : G), (L (f t)) z₀ ∂μ‖ ≤ (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε