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₀ ≤ ε
refine_1 :
  ∀ (y : ℝ),
    Membership.mem (γ := Set ℝ) ((fun (i : G) ↦ ‖g i‖) '' preimage (β := G) (fun (t : G) ↦ x₀ - t) (ball 0 R)) y →
      y ≤ ‖z₀‖ + ε
⊢ ∃ (x : ℝ),
    ∀ (y : ℝ),
      Membership.mem (γ := Set ℝ) ((fun (i : G) ↦ ‖g i‖) '' preimage (β := G) (fun (t : G) ↦ x₀ - t) (ball 0 R)) y →
        y ≤ x

Tactic:
refine ⟨‖z₀‖ + ε, ?_⟩
-- 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₀ ≤ ε
x : G
hx : Membership.mem (γ := Set G) (preimage (β := G) (fun (t : G) ↦ x₀ - t) (ball 0 R)) x
⊢ (fun (i : G) ↦ ‖g i‖) x ≤ ‖z₀‖ + ε

Tactic:
norm_le_norm_add_const_of_dist_le (hg x ?_)

Premises used: norm_le_norm_add_const_of_dist_le
-- 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₀ ≤ ε
x : G
hx : Membership.mem (γ := Set G) (preimage (β := G) (fun (t : G) ↦ x₀ - t) (ball 0 R)) x
refine_1 : x ∈ ball x₀ R
⊢ (fun (i : G) ↦ ‖g i‖) x ≤ ‖z₀‖ + ε

Tactic:
refine norm_le_norm_add_const_of_dist_le (hg x ?_)

Premises used: norm_le_norm_add_const_of_dist_le
-- 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₀ ≤ ε
x : G
hx : Membership.mem (γ := Set G) (preimage (β := G) (fun (t : G) ↦ x₀ - t) (ball 0 R)) x
refine_1 : ‖x - x₀‖ < R
refine_1₁ : ‖x₀ - x‖ < R
refine_1₂ refine_1₃ refine_1₄ refine_1₅ : Membership.mem (γ := Set G) (ball 0 R) (x₀ - x)
⊢ x ∈ ball x₀ R

Tactic:
rwa [mem_ball_iff_norm, norm_sub_rev, ← mem_ball_zero_iff]

Premises used: mem_ball_iff_norm, norm_sub_rev, mem_ball_zero_iff
-- 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₀ ≤ ε
⊢ ConvolutionExistsAt f g x₀ L μ

Tactic:
have hfg : ConvolutionExistsAt f g x₀ L μ := by
    refine BddAbove.convolutionExistsAt L ?_ Metric.isOpen_ball.measurableSet (Subset.trans ?_ hf)
      hif.integrableOn hmg
    swap; · refine fun t => mt fun ht : f t = 0 => ?_; simp_rw [ht, L.map_zero₂]
    rw [bddAbove_def]
    refine ⟨‖z₀‖ + ε, ?_⟩
    rintro _ ⟨x, hx, rfl⟩
    refine norm_le_norm_add_const_of_dist_le (hg x ?_)
    rwa [mem_ball_iff_norm, norm_sub_rev, ← mem_ball_zero_iff]
-- 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 μ
t : G
pos :
  ∀ (ht : t ∈ support f),
    dist.{uF} (α := 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) * ε
neg :
  ∀ (ht : t ∉ support f),
    dist.{uF} (α := 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) * ε
⊢ dist.{uF} (α := 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) * ε

Tactic:
by_cases ht : t ∈ support f

Premises used: Function.support
-- 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 μ
t : G
ht : t ∈ support f
⊢ Membership.mem (γ := Set G) (ball 0 R) t

Tactic:
have h2t := hf ht
-- 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 μ
t : G
ht : t ∈ support f
h2t : Membership.mem (γ := Set G) (ball 0 R) t
⊢ ‖t‖ < R

Tactic:
rw [mem_ball_zero_iff] at h2t

Premises used: mem_ball_zero_iff
-- 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 μ
t : G
ht : t ∈ support f
h2t : ‖t‖ < R
⊢ x₀ - t ∈ ball x₀ R → dist (g (x₀ - t)) z₀ ≤ ε

Tactic:
specialize hg (x₀ - t)

Premises used: HSub.hSub
-- 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 μ
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₀ ≤ ε
⊢ ‖t‖ < R → dist (g (x₀ - t)) z₀ ≤ ε

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

Premises used: add_mem_ball_iff_norm, sub_eq_add_neg, norm_neg
-- 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 μ
hfg : ConvolutionExistsAt f g x₀ L μ
t : G
ht : t ∈ support f
h2t : ‖t‖ < R
hg : ‖t‖ < R → dist (g (x₀ - t)) z₀ ≤ ε
⊢ dist.{uF} (α := 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) * ε

Tactic:
((L (f t)).dist_le_opNorm _ _).trans ?_

Premises used: LE.le.trans, DFunLike.coe, ContinuousLinearMap.dist_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 μ
hfg : ConvolutionExistsAt f g x₀ L μ
t : G
ht : t ∈ support f
h2t : ‖t‖ < R
hg : ‖t‖ < R → dist (g (x₀ - t)) z₀ ≤ ε
pos :
  norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) * dist (g (x₀ - t)) z₀ ≤
    norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) * ε
⊢ dist.{uF} (α := 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) * ε

Tactic:
refine ((L (f t)).dist_le_opNorm _ _).trans ?_

Premises used: LE.le.trans, DFunLike.coe, ContinuousLinearMap.dist_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 μ
hfg : ConvolutionExistsAt f g x₀ L μ
t : G
ht : t ∈ support f
h2t : ‖t‖ < R
hg : ‖t‖ < R → dist (g (x₀ - t)) z₀ ≤ ε
pos : dist (g (x₀ - t)) z₀ ≤ ε
⊢ norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) * dist (g (x₀ - t)) z₀ ≤
    norm (E := E' →L[𝕜] F) ((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) * ε

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 μ
hfg : ConvolutionExistsAt f g x₀ L μ
t : G
ht : t ∈ support f
h2t : ‖t‖ < R
hg : ‖t‖ < R → dist (g (x₀ - t)) z₀ ≤ ε
⊢ dist (g (x₀ - t)) z₀ ≤ ε

Tactic:
hg h2t
-- 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 μ
hfg : ConvolutionExistsAt f g x₀ L μ
t : G
ht : t ∈ support f
h2t : ‖t‖ < R
hg : ‖t‖ < R → dist (g (x₀ - t)) z₀ ≤ ε
⊢ dist (g (x₀ - t)) z₀ ≤ ε

Tactic:
exact hg h2t
-- 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 μ
t : G
ht : t ∉ support f
⊢ f t = 0

Tactic:
rw [notMem_support] at ht

Premises used: Function.notMem_support
-- 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 μ
t : G
ht : f t = 0
neg : LE.le (α := ℝ) 0 0
⊢ dist.{uF} (α := 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) * ε

Tactic:
simp_rw [ht, L.map_zero₂, L.map_zero, norm_zero, zero_mul, dist_self]

Premises used: ContinuousLinearMap.map_zero, MulZeroClass.zero_mul, norm_zero, dist_self, ContinuousLinearMap.map_zero₂
-- 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 μ
t : G
ht : f t = 0
⊢ LE.le (α := ℝ) 0 0

Tactic:
rfl
-- 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 μ
⊢ ∀ (t : G),
    dist.{uF} (α := 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) * ε

Tactic:
have h2 : ∀ t, dist (L (f t) (g (x₀ - t))) (L (f t) z₀) ≤ ‖L (f t)‖ * ε := by
    intro t; by_cases ht : t ∈ support f
    · have h2t := hf ht
      rw [mem_ball_zero_iff] at h2t
      specialize hg (x₀ - t)
      rw [sub_eq_add_neg, add_mem_ball_iff_norm, norm_neg, ← sub_eq_add_neg] at hg
      refine ((L (f t)).dist_le_opNorm _ _).trans ?_
      gcongr
      exact hg h2t
    · rw [notMem_support] at ht
      simp_rw [ht, L.map_zero₂, L.map_zero, norm_zero, zero_mul, dist_self]
      rfl
-- 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),
    dist.{uF} (α := 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) * ε
simp_rw :
  dist.{uF} (α := 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‖ ∂μ) * ε
⊢ dist ((f ⋆[L, μ] g) x₀) (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) z₀ ∂μ) ≤
    (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε

Tactic:
simp_rw [convolution_def]

Premises used: MeasureTheory.convolution_def
-- 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),
    dist.{uF} (α := 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) * ε
simp_rw :
  ∀
    (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) * ε),
    ‖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‖ ∂μ) * ε
⊢ dist.{uF} (α := 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:
simp_rw [dist_eq_norm] at h2 ⊢

Premises used: dist_eq_norm