awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : SeminormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : SecondCountableTopology G
inst_12 : μ.IsAddLeftInvariant
inst_13 : 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),
    ‖HSub.hSub (α := F) (β := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
          ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀ : F)‖ ≤
      norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) * ε
rw :
  norm.{uF} (E := F)
      (∫ (a : G),
        HSub.hSub (α := F) (β := F) ((((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - a)) : F)
          ((((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) z₀ : F) ∂μ) ≤
    (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε
rw₁ : Integrable.{uF, uG} (ε := F) (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀) μ
⊢ ‖HSub.hSub (α := F) (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) ∂μ)
        (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀ ∂μ)‖ ≤
    (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε

Tactic:
rw [← integral_sub hfg.integrable]

Premises used: MeasureTheory.ConvolutionExistsAt.integrable, MeasureTheory.integral_sub
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : SeminormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : SecondCountableTopology G
inst_12 : μ.IsAddLeftInvariant
inst_13 : 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),
    ‖HSub.hSub (α := F) (β := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
          ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀ : F)‖ ≤
      norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) * ε
⊢ Integrable.{uF, uG} (ε := F) (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀) μ

Tactic:
(L.flip z₀).integrable_comp hif

Premises used: ContinuousLinearMap.integrable_comp, ContinuousLinearMap.flip, DFunLike.coe
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : SeminormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : SecondCountableTopology G
inst_12 : μ.IsAddLeftInvariant
inst_13 : 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),
    ‖HSub.hSub (α := F) (β := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
          ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀ : F)‖ ≤
      norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) * ε
⊢ Integrable.{uF, uG} (ε := F) (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀) μ

Tactic:
exact (L.flip z₀).integrable_comp hif

Premises used: ContinuousLinearMap.integrable_comp, ContinuousLinearMap.flip, DFunLike.coe
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : SeminormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : SecondCountableTopology G
inst_12 : μ.IsAddLeftInvariant
inst_13 : 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),
    ‖HSub.hSub (α := F) (β := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
          ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀ : F)‖ ≤
      norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) * ε
⊢ norm.{uF} (E := F)
      (∫ (a : G),
        HSub.hSub (α := F) (β := F) ((((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - a)) : F)
          ((((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) z₀ : F) ∂μ) ≤
    (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε

Tactic:
(norm_integral_le_of_norm_le ((L.integrable_comp hif).norm.mul_const ε)
    (Eventually.of_forall h2)).trans ?_

Premises used: MeasureTheory.norm_integral_le_of_norm_le, Filter.Eventually.of_forall, ContinuousLinearMap.integrable_comp, MeasureTheory.Integrable.mul_const, LE.le.trans, MeasureTheory.Integrable.norm
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : SeminormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : SecondCountableTopology G
inst_12 : μ.IsAddLeftInvariant
inst_13 : 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),
    ‖HSub.hSub (α := F) (β := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
          ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀ : F)‖ ≤
      norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) * ε
refine :
  ∫ (x : G), norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f x) : E' →L[𝕜] F) * ε ∂μ ≤
    (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε
⊢ norm.{uF} (E := F)
      (∫ (a : G),
        HSub.hSub (α := F) (β := F) ((((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - a)) : F)
          ((((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) z₀ : F) ∂μ) ≤
    (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε

Tactic:
refine (norm_integral_le_of_norm_le ((L.integrable_comp hif).norm.mul_const ε)
    (Eventually.of_forall h2)).trans ?_

Premises used: MeasureTheory.norm_integral_le_of_norm_le, Filter.Eventually.of_forall, ContinuousLinearMap.integrable_comp, MeasureTheory.Integrable.mul_const, LE.le.trans, MeasureTheory.Integrable.norm
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : SeminormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : SecondCountableTopology G
inst_12 : μ.IsAddLeftInvariant
inst_13 : 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),
    ‖HSub.hSub (α := F) (β := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
          ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀ : F)‖ ≤
      norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) * ε
rw :
  (∫ (a : G), norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) ∂μ) * ε ≤
    (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε
⊢ ∫ (x : G), norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f x) : E' →L[𝕜] F) * ε ∂μ ≤
    (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε

Tactic:
rw [integral_mul_const]

Premises used: MeasureTheory.integral_mul_const
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : SeminormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : SecondCountableTopology G
inst_12 : μ.IsAddLeftInvariant
inst_13 : 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),
    ‖HSub.hSub (α := F) (β := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
          ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀ : F)‖ ≤
      norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) * ε
hbc : ∫ (a : G), norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) ∂μ ≤ ‖L‖ * ∫ (x : G), ‖f x‖ ∂μ
⊢ (∫ (a : G), norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) ∂μ) * ε ≤
    (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : SeminormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : SecondCountableTopology G
inst_12 : μ.IsAddLeftInvariant
inst_13 : 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),
    ‖HSub.hSub (α := F) (β := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
          ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀ : F)‖ ≤
      norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) * ε
t : G
⊢ norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) ≤ ‖L‖ * ‖f t‖

Tactic:
L.le_opNorm (f t)

Premises used: ContinuousLinearMap.le_opNorm
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : SeminormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : SecondCountableTopology G
inst_12 : μ.IsAddLeftInvariant
inst_13 : 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),
    ‖HSub.hSub (α := F) (β := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
          ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀ : F)‖ ≤
      norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) * ε
t : G
⊢ norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) ≤ ‖L‖ * ‖f t‖

Tactic:
exact L.le_opNorm (f t)

Premises used: ContinuousLinearMap.le_opNorm
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : SeminormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : SecondCountableTopology G
inst_12 : μ.IsAddLeftInvariant
inst_13 : 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),
    ‖HSub.hSub (α := F) (β := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
          ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀ : F)‖ ≤
      norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) * ε
⊢ ∀ (t : G), norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) ≤ ‖L‖ * ‖f t‖

Tactic:
have h3 : ∀ t, ‖L (f t)‖ ≤ ‖L‖ * ‖f t‖ := by
    intro t
    exact L.le_opNorm (f t)
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : SeminormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : SecondCountableTopology G
inst_12 : μ.IsAddLeftInvariant
inst_13 : 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),
    ‖HSub.hSub (α := F) (β := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
          ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀ : F)‖ ≤
      norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) * ε
h3 : ∀ (t : G), norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) ≤ ‖L‖ * ‖f t‖
⊢ ∫ (a : G), norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) ∂μ ≤ ‖L‖ * ∫ (x : G), ‖f x‖ ∂μ

Tactic:
(integral_mono (L.integrable_comp hif).norm (hif.norm.const_mul _) h3).trans_eq ?_

Premises used: LE.le.trans_eq, MeasureTheory.Integrable.const_mul, MeasureTheory.integral_mono, ContinuousLinearMap.integrable_comp, MeasureTheory.Integrable.norm
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : SeminormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : SecondCountableTopology G
inst_12 : μ.IsAddLeftInvariant
inst_13 : 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),
    ‖HSub.hSub (α := F) (β := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
          ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀ : F)‖ ≤
      norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) * ε
h3 : ∀ (t : G), norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) ≤ ‖L‖ * ‖f t‖
hbc : ∫ (x : G), ‖L‖ * ‖f x‖ ∂μ = ‖L‖ * ∫ (x : G), ‖f x‖ ∂μ
⊢ ∫ (a : G), norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) ∂μ ≤ ‖L‖ * ∫ (x : G), ‖f x‖ ∂μ

Tactic:
refine (integral_mono (L.integrable_comp hif).norm (hif.norm.const_mul _) h3).trans_eq ?_

Premises used: LE.le.trans_eq, MeasureTheory.Integrable.const_mul, MeasureTheory.integral_mono, ContinuousLinearMap.integrable_comp, MeasureTheory.Integrable.norm
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : SeminormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : SecondCountableTopology G
inst_12 : μ.IsAddLeftInvariant
inst_13 : 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),
    ‖HSub.hSub (α := F) (β := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
          ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀ : F)‖ ≤
      norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) * ε
h3 : ∀ (t : G), norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) ≤ ‖L‖ * ‖f t‖
hbc hbc₁ : ‖L‖ * ∫ (a : G), ‖f a‖ ∂μ = ‖L‖ * ∫ (x : G), ‖f x‖ ∂μ
⊢ ∫ (x : G), ‖L‖ * ‖f x‖ ∂μ = ‖L‖ * ∫ (x : G), ‖f x‖ ∂μ

Tactic:
rw [integral_const_mul]

Premises used: MeasureTheory.integral_const_mul
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : SeminormedAddCommGroup G
inst_3 : BorelSpace G
inst_4 : SecondCountableTopology G
inst_5 : μ.IsAddLeftInvariant
inst_6 : SFinite μ
inst_7 : NormedSpace ℝ E'
inst_8 : CompleteSpace E'
f : G → ℝ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hf : support f ⊆ ball 0 R
hnf : ∀ (x : G), 0 ≤ f x
hintf : Eq (α := ℝ) (∫ (x : G), f x ∂μ) 1
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
⊢ Integrable f μ

Tactic:
have hif : Integrable f μ := integrable_of_integral_eq_one hintf
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : SeminormedAddCommGroup G
inst_3 : BorelSpace G
inst_4 : SecondCountableTopology G
inst_5 : μ.IsAddLeftInvariant
inst_6 : SFinite μ
inst_7 : NormedSpace ℝ E'
inst_8 : CompleteSpace E'
f : G → ℝ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hf : support f ⊆ ball 0 R
hnf : ∀ (x : G), 0 ≤ f x
hintf : Eq (α := ℝ) (∫ (x : G), f x ∂μ) 1
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hif : Integrable f μ
⊢ dist ((f ⋆[lsmul ℝ ℝ, μ] g) x₀)
      (∫ (t : G), (((lsmul ℝ ℝ : (a : ℝ) → E' →L[ℝ] E') (f t) : E' →L[ℝ] E') : (a : E') → E') z₀ ∂μ) ≤
    ε

Tactic:
(dist_convolution_le' (lsmul ℝ ℝ) hε hif hf hmg hg).trans _

Premises used: Real, MeasureTheory.dist_convolution_le', LE.le.trans, ContinuousLinearMap.lsmul
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : SeminormedAddCommGroup G
inst_3 : BorelSpace G
inst_4 : SecondCountableTopology G
inst_5 : μ.IsAddLeftInvariant
inst_6 : SFinite μ
inst_7 : NormedSpace ℝ E'
inst_8 : CompleteSpace E'
f : G → ℝ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hf : support f ⊆ ball 0 R
hnf : ∀ (x : G), 0 ≤ f x
hintf : Eq (α := ℝ) (∫ (x : G), f x ∂μ) 1
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hif : Integrable f μ
h : z₀ = ∫ (t : G), (((lsmul ℝ ℝ : (a : ℝ) → E' →L[ℝ] E') (f t) : E' →L[ℝ] E') : (a : E') → E') z₀ ∂μ
convert_2 : (norm.{uE'} (E := ℝ →L[ℝ] E' →L[ℝ] E') (lsmul ℝ ℝ) * ∫ (x : G), ‖f x‖ ∂μ) * ε ≤ ε
⊢ dist ((f ⋆[lsmul ℝ ℝ, μ] g) x₀) z₀ ≤ ε

Tactic:
convert! (dist_convolution_le' (lsmul ℝ ℝ) hε hif hf hmg hg).trans _

Premises used: Real, MeasureTheory.dist_convolution_le', LE.le.trans, ContinuousLinearMap.lsmul
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : SeminormedAddCommGroup G
inst_3 : BorelSpace G
inst_4 : SecondCountableTopology G
inst_5 : μ.IsAddLeftInvariant
inst_6 : SFinite μ
inst_7 : NormedSpace ℝ E'
inst_8 : CompleteSpace E'
f : G → ℝ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hf : support f ⊆ ball 0 R
hnf : ∀ (x : G), 0 ≤ f x
hintf : Eq (α := ℝ) (∫ (x : G), f x ∂μ) 1
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hif : Integrable f μ
h : z₀ = ∫ (t : G), f t • z₀ ∂μ
h₁ : z₀ = HSMul.hSMul (α := ℝ) (∫ (x : G), f x ∂μ) z₀
h₂ : z₀ = HSMul.hSMul (α := ℝ) 1 z₀
⊢ z₀ = ∫ (t : G), (((lsmul ℝ ℝ : (a : ℝ) → E' →L[ℝ] E') (f t) : E' →L[ℝ] E') : (a : E') → E') z₀ ∂μ

Tactic:
simp_rw [lsmul_apply, integral_smul_const, hintf, one_smul]

Premises used: integral_smul_const, ContinuousLinearMap.lsmul_apply, one_smul
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : SeminormedAddCommGroup G
inst_3 : BorelSpace G
inst_4 : SecondCountableTopology G
inst_5 : μ.IsAddLeftInvariant
inst_6 : SFinite μ
inst_7 : NormedSpace ℝ E'
inst_8 : CompleteSpace E'
f : G → ℝ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hf : support f ⊆ ball 0 R
hnf : ∀ (x : G), 0 ≤ f x
hintf : Eq (α := ℝ) (∫ (x : G), f x ∂μ) 1
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hif : Integrable f μ
convert_2 : norm.{uE'} (E := ℝ →L[ℝ] E' →L[ℝ] E') (lsmul ℝ ℝ) * ε ≤ ε
⊢ (norm.{uE'} (E := ℝ →L[ℝ] E' →L[ℝ] E') (lsmul ℝ ℝ) * ∫ (x : G), ‖f x‖ ∂μ) * ε ≤ ε

Tactic:
simp_rw [Real.norm_of_nonneg (hnf _), hintf, mul_one]

Premises used: mul_one, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : SeminormedAddCommGroup G
inst_3 : BorelSpace G
inst_4 : SecondCountableTopology G
inst_5 : μ.IsAddLeftInvariant
inst_6 : SFinite μ
inst_7 : NormedSpace ℝ E'
inst_8 : CompleteSpace E'
f : G → ℝ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hf : support f ⊆ ball 0 R
hnf : ∀ (x : G), 0 ≤ f x
hintf : Eq (α := ℝ) (∫ (x : G), f x ∂μ) 1
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hif : Integrable f μ
⊢ norm.{uE'} (E := ℝ →L[ℝ] E' →L[ℝ] E') (lsmul ℝ ℝ) * ε ≤ ε

Tactic:
(mul_le_mul_of_nonneg_right opNorm_lsmul_le hε).trans_eq (one_mul ε)

Premises used: LE.le.trans_eq, mul_le_mul_of_nonneg_right, ContinuousLinearMap.opNorm_lsmul_le, one_mul