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'
x : G
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 : AddCommGroup G
inst_10 : μ.IsAddLeftInvariant
inst_11 : μ.IsNegInvariant
inst_12 : MeasurableNeg G
inst_13 : MeasurableAdd G
h1 : ∀ᵐ (x : G) ∂μ, f (-x) = f x
h2 : ∀ᵐ (x : G) ∂μ, g (-x) = g x
rw :
  Eq.{uF + 1} (α := F)
    (∫ (x_1 : G), (((L : (a : E) → E' →L[𝕜] F) (f (- -x_1)) : E' →L[𝕜] F) : (a : E') → F) (g (x + -x_1)) ∂μ)
    (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) ∂μ)
⊢ Eq.{uF + 1} (α := 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) (g (x - t)) ∂μ)

Tactic:
rw [← integral_neg_eq_self]

Premises used: MeasureTheory.integral_neg_eq_self
-- 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'
x : G
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 : AddCommGroup G
inst_10 : μ.IsAddLeftInvariant
inst_11 : μ.IsNegInvariant
inst_12 : MeasurableNeg G
inst_13 : MeasurableAdd G
h1 : ∀ᵐ (x : G) ∂μ, f (-x) = f x
h2 : ∀ᵐ (x : G) ∂μ, g (-x) = g x
⊢ Eq.{uF + 1} (α := F)
    (∫ (x_1 : G), (((L : (a : E) → E' →L[𝕜] F) (f (- -x_1)) : E' →L[𝕜] F) : (a : E') → F) (g (x + -x_1)) ∂μ)
    (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) ∂μ)

Tactic:
simp only [neg_neg, ← sub_eq_add_neg]

Premises used: sub_eq_add_neg, neg_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 : AddCommGroup G
inst_10 : μ.IsAddLeftInvariant
inst_11 : μ.IsNegInvariant
inst_12 : TopologicalSpace G
inst_13 : IsTopologicalAddGroup G
inst_14 : BorelSpace G
hcf : HasCompactSupport f
hf : Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hg : LocallyIntegrable g μ
rw : Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (g ⋆[L.flip, μ] f)
⊢ Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f ⋆[L, μ] g)

Tactic:
rw [← convolution_flip]

Premises used: MeasureTheory.convolution_flip
-- 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 : AddCommGroup G
inst_10 : μ.IsAddLeftInvariant
inst_11 : μ.IsNegInvariant
inst_12 : TopologicalSpace G
inst_13 : IsTopologicalAddGroup G
inst_14 : BorelSpace G
hcf : HasCompactSupport f
hf : Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hg : LocallyIntegrable g μ
⊢ Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (g ⋆[L.flip, μ] f)

Tactic:
hcf.continuous_convolution_right L.flip hg hf

Premises used: ContinuousLinearMap.flip, HasCompactSupport.continuous_convolution_right
-- 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 : AddCommGroup G
inst_10 : μ.IsAddLeftInvariant
inst_11 : μ.IsNegInvariant
inst_12 : TopologicalSpace G
inst_13 : IsTopologicalAddGroup G
inst_14 : BorelSpace G
hcf : HasCompactSupport f
hf : Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hg : LocallyIntegrable g μ
⊢ Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (g ⋆[L.flip, μ] f)

Tactic:
exact hcf.continuous_convolution_right L.flip hg hf

Premises used: ContinuousLinearMap.flip, HasCompactSupport.continuous_convolution_right
-- 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 : AddCommGroup G
inst_10 : μ.IsAddLeftInvariant
inst_11 : μ.IsNegInvariant
inst_12 : TopologicalSpace G
inst_13 : IsTopologicalAddGroup G
inst_14 : BorelSpace G
inst_15 : FirstCountableTopology G
inst_16 : SecondCountableTopologyEither G E
hbf : BddAbove (α := ℝ) (range fun (x : G) ↦ ‖f x‖)
hf : Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hg : Integrable g μ
rw : Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (g ⋆[L.flip, μ] f)
⊢ Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f ⋆[L, μ] g)

Tactic:
rw [← convolution_flip]

Premises used: MeasureTheory.convolution_flip
-- 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 : AddCommGroup G
inst_10 : μ.IsAddLeftInvariant
inst_11 : μ.IsNegInvariant
inst_12 : TopologicalSpace G
inst_13 : IsTopologicalAddGroup G
inst_14 : BorelSpace G
inst_15 : FirstCountableTopology G
inst_16 : SecondCountableTopologyEither G E
hbf : BddAbove (α := ℝ) (range fun (x : G) ↦ ‖f x‖)
hf : Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hg : Integrable g μ
⊢ Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (g ⋆[L.flip, μ] f)

Tactic:
hbf.continuous_convolution_right_of_integrable L.flip hg hf

Premises used: BddAbove.continuous_convolution_right_of_integrable, ContinuousLinearMap.flip
-- 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 : AddCommGroup G
inst_10 : μ.IsAddLeftInvariant
inst_11 : μ.IsNegInvariant
inst_12 : TopologicalSpace G
inst_13 : IsTopologicalAddGroup G
inst_14 : BorelSpace G
inst_15 : FirstCountableTopology G
inst_16 : SecondCountableTopologyEither G E
hbf : BddAbove (α := ℝ) (range fun (x : G) ↦ ‖f x‖)
hf : Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hg : Integrable g μ
⊢ Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (g ⋆[L.flip, μ] f)

Tactic:
exact hbf.continuous_convolution_right_of_integrable L.flip hg hf

Premises used: BddAbove.continuous_convolution_right_of_integrable, ContinuousLinearMap.flip
-- 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
x₀ : G
R : ℝ
hf : support f ⊆ ball 0 R
hg : ∀ x ∈ ball x₀ R, g x = g x₀
t : G
pos :
  ∀ (ht : t ∈ support f),
    Eq.{uF + 1} (α := 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) (g x₀) : F)
neg :
  ∀ (ht : t ∉ support f),
    Eq.{uF + 1} (α := 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) (g x₀) : F)
⊢ Eq.{uF + 1} (α := 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) (g x₀) : 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
x₀ : G
R : ℝ
hf : support f ⊆ ball 0 R
hg : ∀ x ∈ ball x₀ R, g x = g x₀
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
x₀ : G
R : ℝ
hf : support f ⊆ ball 0 R
hg : ∀ x ∈ ball x₀ R, g x = g x₀
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
x₀ : G
R : ℝ
hf : support f ⊆ ball 0 R
hg : ∀ x ∈ ball x₀ R, g x = g x₀
t : G
ht : t ∈ support f
h2t : ‖t‖ < R
⊢ x₀ - t ∈ ball x₀ R → g (x₀ - t) = g x₀

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
x₀ : G
R : ℝ
hf : support f ⊆ ball 0 R
t : G
ht : t ∈ support f
h2t : ‖t‖ < R
hg : x₀ - t ∈ ball x₀ R → g (x₀ - t) = g x₀
⊢ ‖t‖ < R → g (x₀ - t) = g x₀

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
x₀ : G
R : ℝ
hf : support f ⊆ ball 0 R
t : G
ht : t ∈ support f
h2t : ‖t‖ < R
hg : ‖t‖ < R → g (x₀ - t) = g x₀
pos pos₁ :
  Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g x₀) : F)
    ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g x₀) : F)
⊢ Eq.{uF + 1} (α := 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) (g x₀) : F)

Tactic:
rw [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
x₀ : G
R : ℝ
hf : support f ⊆ ball 0 R
hg : ∀ x ∈ ball x₀ R, g x = g x₀
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
x₀ : G
R : ℝ
hf : support f ⊆ ball 0 R
hg : ∀ x ∈ ball x₀ R, g x = g x₀
t : G
ht : f t = 0
neg :
  Eq.{uF + 1} (α := F) (((L : (a : E) → E' →L[𝕜] F) 0 : (a : E') → F) (g (x₀ - t)) : F)
    (((L : (a : E) → E' →L[𝕜] F) 0 : (a : E') → F) (g x₀) : F)
⊢ Eq.{uF + 1} (α := 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) (g x₀) : F)

Tactic:
simp_rw [ht, L.map_zero₂]

Premises used: 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
x₀ : G
R : ℝ
hf : support f ⊆ ball 0 R
hg : ∀ x ∈ ball x₀ R, g x = g x₀
⊢ ∀ (t : G),
    Eq.{uF + 1} (α := 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) (g x₀) : F)

Tactic:
have h2 : ∀ t, L (f t) (g (x₀ - t)) = L (f t) (g x₀) := fun t ↦ by
    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
      rw [hg h2t]
    · rw [notMem_support] at ht
      simp_rw [ht, L.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
x₀ : G
R : ℝ
hf : support f ⊆ ball 0 R
hg : ∀ x ∈ ball x₀ R, g x = g x₀
h2 :
  ∀ (t : G),
    Eq.{uF + 1} (α := 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) (g x₀) : F)
simp_rw :
  Eq.{uF + 1} (α := 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) (g x₀) ∂μ)
⊢ (f ⋆[L, μ] g) x₀ = ∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g x₀) ∂μ

Tactic:
simp_rw [convolution_def, h2]

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₀ ≤ ε
⊢ ConvolutionExistsAt f g x₀ L μ

Tactic:
BddAbove.convolutionExistsAt L ?_ Metric.isOpen_ball.measurableSet (Subset.trans ?_ hf)
      hif.integrableOn hmg

Premises used: Set.Subset.trans, IsOpen.measurableSet, Metric.isOpen_ball, MeasureTheory.Integrable.integrableOn, BddAbove.convolutionExistsAt
-- 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 : BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' preimage (β := G) (fun (t : G) ↦ x₀ - t) (ball 0 R))
refine_2 :
  (support.{uG, uF} (M := F) fun (t : G) ↦
      (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))) ⊆
    support f
⊢ ConvolutionExistsAt f g x₀ L μ

Tactic:
refine BddAbove.convolutionExistsAt L ?_ Metric.isOpen_ball.measurableSet (Subset.trans ?_ hf)
      hif.integrableOn hmg

Premises used: Set.Subset.trans, IsOpen.measurableSet, Metric.isOpen_ball, MeasureTheory.Integrable.integrableOn, BddAbove.convolutionExistsAt
-- 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₀ ≤ ε
⊢ (support.{uG, uF} (M := F) fun (t : G) ↦
      (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))) ⊆
    support f

Tactic:
fun t => mt fun ht : f t = 0 => ?_

Premises used: Set.Mem, setOf, mt, Set.Subset, Function.support, Not
-- 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_2 :
  ∀ (t : G) (ht : f t = 0),
    Eq.{uF + 1} (α := F)
      ((fun (t : G) ↦ ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)) t) 0
⊢ (support.{uG, uF} (M := F) fun (t : G) ↦
      (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))) ⊆
    support f

Tactic:
refine fun t => mt fun ht : f t = 0 => ?_

Premises used: mt
-- 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₀ ≤ ε
t : G
ht : f t = 0
refine_2 refine_2₁ :
  Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F) (0 : F)
refine_2₂ : Eq.{uF + 1} (α := F) (((L : (a : E) → E' →L[𝕜] F) 0 : (a : E') → F) (g (x₀ - t)) : F) (0 : F)
⊢ Eq.{uF + 1} (α := F)
    ((fun (t : G) ↦ ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)) t) 0

Tactic:
simp_rw [ht, L.map_zero₂]

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

Tactic:
⟨‖z₀‖ + ε, ?_⟩

Premises used: Norm.norm, HAdd.hAdd, Exists.intro