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 : AddCommGroup G
inst_9 : MeasurableNeg G
inst_10 : μ.IsAddLeftInvariant
inst_11 : MeasurableAdd₂ G
inst_12 : SFinite μ
x₀ : G
s : Set G
hbg : BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' (fun (t : G) ↦ x₀ - t) ⁻¹' s)
hs : MeasurableSet s
h2s :
  (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))) ⊆
    s
hf : IntegrableOn f s μ
hmg : AEStronglyMeasurable g μ
⊢ AEStronglyMeasurable (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x₀ - t) μ)

Tactic:
have : AEStronglyMeasurable g (map (fun t : G => x₀ - t) μ) :=
      hmg.mono_ac (quasiMeasurePreserving_sub_left_of_right_invariant μ x₀).absolutelyContinuous
-- 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 : AddCommGroup G
inst_9 : MeasurableNeg G
inst_10 : μ.IsAddLeftInvariant
inst_11 : MeasurableAdd₂ G
inst_12 : SFinite μ
x₀ : G
s : Set G
hbg : BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' (fun (t : G) ↦ x₀ - t) ⁻¹' s)
hs : MeasurableSet s
h2s :
  (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))) ⊆
    s
hf : IntegrableOn f s μ
hmg : AEStronglyMeasurable g μ
this : AEStronglyMeasurable (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x₀ - t) μ)
refine_2 :
  LE.le (α := Measure G) (Measure.map (fun (t : G) ↦ x₀ - t) (μ.restrict s)) (Measure.map (fun (t : G) ↦ x₀ - t) μ)
⊢ AEStronglyMeasurable (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x₀ - t) (μ.restrict s))

Tactic:
apply this.mono_measure

Premises used: MeasureTheory.AEStronglyMeasurable.mono_measure
-- 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 : AddCommGroup G
inst_9 : MeasurableNeg G
inst_10 : μ.IsAddLeftInvariant
inst_11 : MeasurableAdd₂ G
inst_12 : SFinite μ
x₀ : G
s : Set G
hbg : BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' (fun (t : G) ↦ x₀ - t) ⁻¹' s)
hs : MeasurableSet s
h2s :
  (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))) ⊆
    s
hf : IntegrableOn f s μ
hmg : AEStronglyMeasurable g μ
this : AEStronglyMeasurable (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x₀ - t) μ)
⊢ LE.le (α := Measure G) (Measure.map (fun (t : G) ↦ x₀ - t) (μ.restrict s)) (Measure.map (fun (t : G) ↦ x₀ - t) μ)

Tactic:
map_mono restrict_le_self (measurable_const.sub measurable_id')

Premises used: Measurable.sub, MeasureTheory.Measure.restrict_le_self, measurable_id', MeasureTheory.Measure.map_mono, measurable_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 : AddCommGroup G
inst_9 : MeasurableNeg G
inst_10 : μ.IsAddLeftInvariant
inst_11 : MeasurableAdd₂ G
inst_12 : SFinite μ
x₀ : G
s : Set G
hbg : BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' (fun (t : G) ↦ x₀ - t) ⁻¹' s)
hs : MeasurableSet s
h2s :
  (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))) ⊆
    s
hf : IntegrableOn f s μ
hmg : AEStronglyMeasurable g μ
this : AEStronglyMeasurable (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x₀ - t) μ)
⊢ LE.le (α := Measure G) (Measure.map (fun (t : G) ↦ x₀ - t) (μ.restrict s)) (Measure.map (fun (t : G) ↦ x₀ - t) μ)

Tactic:
exact map_mono restrict_le_self (measurable_const.sub measurable_id')
-- 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 : AddCommGroup G
inst_9 : MeasurableNeg G
inst_10 : μ.IsAddLeftInvariant
inst_11 : MeasurableAdd G
inst_12 : μ.IsNegInvariant
simp_rw :
  Integrable.{uF, uG} (ε := F)
      (fun (t : G) ↦ (((L.flip : (a : E') → E →L[𝕜] F) (g t) : E →L[𝕜] F) : (a : E) → F) (f (x - t))) μ ↔
    Integrable.{uF, uG} (ε := F)
      (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t))) μ
simp_rw₁ :
  Integrable.{uF, uG} (ε := F)
      (fun (t : G) ↦ (((L.flip : (a : E') → E →L[𝕜] F) (g t) : E →L[𝕜] F) : (a : E) → F) (f (x - t))) μ ↔
    Integrable.{uF, uG} (ε := F)
      (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f (x - t)) : E' →L[𝕜] F) : (a : E') → F) (g (x - (x - t)))) μ
simp_rw₂ :
  Integrable.{uF, uG} (ε := F)
      (fun (t : G) ↦ (((L.flip : (a : E') → E →L[𝕜] F) (g t) : E →L[𝕜] F) : (a : E) → F) (f (x - t))) μ ↔
    Integrable.{uF, uG} (ε := F)
      (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f (x - t)) : E' →L[𝕜] F) : (a : E') → F) (g t)) μ
⊢ ConvolutionExistsAt g f x L.flip μ ↔ ConvolutionExistsAt f g x L μ

Tactic:
simp_rw [ConvolutionExistsAt, ← integrable_comp_sub_left (fun t => L (f t) (g (x - t))) x,
    sub_sub_cancel, flip_apply]

Premises used: HSub.hSub, ContinuousLinearMap.flip_apply, MeasureTheory.ConvolutionExistsAt, MeasureTheory.integrable_comp_sub_left, sub_sub_cancel, 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'
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 : AddCommGroup G
inst_9 : MeasurableNeg G
inst_10 : μ.IsAddLeftInvariant
inst_11 : MeasurableAdd G
inst_12 : μ.IsNegInvariant
h : ConvolutionExistsAt f g x L μ
⊢ Integrable.{uF, uG} (ε := F)
    (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f (x - t)) : E' →L[𝕜] F) : (a : E') → F) (g (x - (x - t)))) μ

Tactic:
h.comp_sub_left x

Premises used: MeasureTheory.Integrable.comp_sub_left
-- 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 : AddCommGroup G
inst_9 : MeasurableNeg G
inst_10 : μ.IsAddLeftInvariant
inst_11 : MeasurableAdd G
inst_12 : μ.IsNegInvariant
h : ConvolutionExistsAt f g x L μ
h₁ : ∀ (x_1 : G), x_1 = x - (x - x_1)
⊢ Integrable.{uF, uG} (ε := F)
    (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f (x - t)) : E' →L[𝕜] F) : (a : E') → F) (g t)) μ

Tactic:
convert! h.comp_sub_left x

Premises used: MeasureTheory.Integrable.comp_sub_left
-- 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 : AddCommGroup G
inst_9 : MeasurableNeg G
inst_10 : μ.IsAddLeftInvariant
inst_11 : MeasurableAdd G
inst_12 : μ.IsNegInvariant
h : ConvolutionExistsAt f g x L μ
x_1 : G
⊢ x_1 = x - (x - x_1)

Tactic:
simp_rw [sub_sub_self]

Premises used: sub_sub_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 : AddCommGroup G
inst_9 : MeasurableNeg G
inst_10 : μ.IsAddLeftInvariant
inst_11 : MeasurableAdd G
inst_12 : μ.IsNegInvariant
⊢ ConvolutionExistsAt f g x L μ ↔
    Integrable.{uF, uG} (ε := F)
      (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f (x - t)) : E' →L[𝕜] F) : (a : E') → F) (g t)) μ

Tactic:
convolutionExistsAt_flip.symm

Premises used: MeasureTheory.convolutionExistsAt_flip, MeasureTheory.ConvolutionExistsAt, Iff.symm
-- 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 : AddCommGroup G
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup G
inst_11 : BorelSpace G
inst_12 : μ.IsAddLeftInvariant
inst_13 : μ.IsNegInvariant
hcf : HasCompactSupport f
hf : Continuous[inst_9, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hg : LocallyIntegrable g μ
⊢ ConvolutionExists f g L μ

Tactic:
fun x₀ =>
  convolutionExistsAt_flip.mp <| hcf.convolutionExists_right L.flip hg hf x₀

Premises used: MeasureTheory.ConvolutionExists, HasCompactSupport.convolutionExists_right, MeasureTheory.convolutionExistsAt_flip, ContinuousLinearMap.flip, Iff.mp
-- 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 : AddCommGroup G
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup G
inst_11 : BorelSpace G
inst_12 : μ.IsAddLeftInvariant
inst_13 : μ.IsNegInvariant
hcg : HasCompactSupport g
hf : Continuous[inst_9, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hg : LocallyIntegrable g μ
⊢ ConvolutionExists f g L μ

Tactic:
fun x₀ =>
  convolutionExistsAt_flip.mp <| hcg.convolutionExists_left_of_continuous_right L.flip hg hf x₀

Premises used: MeasureTheory.ConvolutionExists, HasCompactSupport.convolutionExists_left_of_continuous_right, MeasureTheory.convolutionExistsAt_flip, ContinuousLinearMap.flip, Iff.mp
-- 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 : Sub G
⊢ (f ⋆[L, μ] g) x = ∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) ∂μ

Tactic:
rfl

Premises used: MeasureTheory.convolution, rfl
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
F : Type uF
inst : NormedAddCommGroup F
x : G
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 F
inst_3 : MeasurableSpace G
μ : Measure G
inst_4 : NormedSpace ℝ F
inst_5 : Sub G
f : G → 𝕜
g : G → F
⊢ Eq (α := F) (convolution (𝕜 := 𝕜) f g (lsmul 𝕜 𝕜) μ x) (∫ (t : G), f t • g (x - t) ∂μ)

Tactic:
rfl

Premises used: MeasureTheory.convolution, rfl
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
x : G
inst : NontriviallyNormedField 𝕜
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : Sub G
inst_3 : NormedSpace ℝ 𝕜
f g : G → 𝕜
⊢ Eq (α := 𝕜) (convolution (𝕜 := 𝕜) f g (mul 𝕜 𝕜) μ x) (∫ (t : G), f t * g (x - t) ∂μ)

Tactic:
rfl

Premises used: MeasureTheory.convolution, 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 : AddGroup G
inst_10 : SMulCommClass ℝ 𝕜 F
y : 𝕜
h : ∀ (x : G), (y • f ⋆[L, μ] g) x = (y • (f ⋆[L, μ] g)) x
⊢ y • f ⋆[L, μ] g = y • (f ⋆[L, μ] g)

Tactic:
ext
-- 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 : AddGroup G
inst_10 : SMulCommClass ℝ 𝕜 F
y : 𝕜
x : G
⊢ (y • f ⋆[L, μ] g) x = (y • (f ⋆[L, μ] g)) x

Tactic:
simp only [Pi.smul_apply, convolution_def, ← integral_smul, L.map_smul₂]

Premises used: MeasureTheory.integral_smul, MeasureTheory.convolution_def, ContinuousLinearMap.map_smul₂, Pi.smul_apply
-- 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 : AddGroup G
inst_10 : SMulCommClass ℝ 𝕜 F
y : 𝕜
h : ∀ (x : G), (f ⋆[L, μ] y • g) x = (y • (f ⋆[L, μ] g)) x
⊢ f ⋆[L, μ] y • g = y • (f ⋆[L, μ] g)

Tactic:
ext
-- 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 : AddGroup G
inst_10 : SMulCommClass ℝ 𝕜 F
y : 𝕜
x : G
⊢ (f ⋆[L, μ] y • g) x = (y • (f ⋆[L, μ] g)) x

Tactic:
simp only [Pi.smul_apply, convolution_def, ← integral_smul, (L _).map_smul]

Premises used: MeasureTheory.integral_smul, MeasureTheory.convolution_def, DFunLike.coe, ContinuousLinearMap.map_smul, Pi.smul_apply
-- 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
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 : AddGroup G
h : ∀ (x : G), (0 ⋆[L, μ] g) x = 0 x
⊢ 0 ⋆[L, μ] g = 0

Tactic:
ext
-- 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
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 : AddGroup G
x : G
h : Eq.{uF + 1} (α := F) (∫ (t : G), ((L : (a : E) → E' →L[𝕜] F) (0 t) : (a : E') → F) (g (x - t)) ∂μ) (0 x)
h₁ : Eq.{uF + 1} (α := F) (∫ (t : G), ((L : (a : E) → E' →L[𝕜] F) 0 : (a : E') → F) (g (x - t)) ∂μ) 0
h₂ : Eq.{uF + 1} (α := F) (∫ (t : G), 0 ∂μ) 0
⊢ (0 ⋆[L, μ] g) x = 0 x

Tactic:
simp_rw [convolution_def, Pi.zero_apply, L.map_zero₂, integral_zero]

Premises used: MeasureTheory.convolution_def, Pi.zero_apply, ContinuousLinearMap.map_zero₂, MeasureTheory.integral_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
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 : AddGroup G
h : ∀ (x : G), (f ⋆[L, μ] 0) x = 0 x
⊢ f ⋆[L, μ] 0 = 0

Tactic:
ext
-- 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
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 : AddGroup G
x : G
h :
  Eq.{uF + 1} (α := F) (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (0 (x - t)) ∂μ)
    (0 x)
h₁ : Eq.{uF + 1} (α := F) (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) 0 ∂μ) 0
h₂ : Eq.{uF + 1} (α := F) (∫ (t : G), 0 ∂μ) 0
⊢ (f ⋆[L, μ] 0) x = 0 x

Tactic:
simp_rw [convolution_def, Pi.zero_apply, (L _).map_zero, integral_zero]

Premises used: ContinuousLinearMap.map_zero, MeasureTheory.convolution_def, Pi.zero_apply, DFunLike.coe, MeasureTheory.integral_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' : 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 : AddGroup G
x : G
hfg : ConvolutionExistsAt f g x L μ
hfg' : ConvolutionExistsAt f g' x L μ
⊢ (f ⋆[L, μ] (g + g')) x = (f ⋆[L, μ] g) x + (f ⋆[L, μ] g') x

Tactic:
simp only [convolution_def, (L _).map_add, Pi.add_apply, integral_add hfg hfg']

Premises used: MeasureTheory.convolution_def, Pi.add_apply, ContinuousLinearMap.map_add, DFunLike.coe, MeasureTheory.integral_add
-- 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' : 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 : AddGroup G
hfg : ConvolutionExists f g L μ
hfg' : ConvolutionExists f g' L μ
h : ∀ (x : G), (f ⋆[L, μ] (g + g')) x = (f ⋆[L, μ] g + f ⋆[L, μ] g') x
⊢ f ⋆[L, μ] (g + g') = f ⋆[L, μ] g + f ⋆[L, μ] g'

Tactic:
ext x
-- 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' : 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 : AddGroup G
hfg : ConvolutionExists f g L μ
hfg' : ConvolutionExists f g' L μ
x : G
⊢ (f ⋆[L, μ] (g + g')) x = (f ⋆[L, μ] g + f ⋆[L, μ] g') x

Tactic:
(hfg x).distrib_add (hfg' x)

Premises used: MeasureTheory.ConvolutionExistsAt.distrib_add
-- 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' : 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 : AddGroup G
hfg : ConvolutionExists f g L μ
hfg' : ConvolutionExists f g' L μ
x : G
⊢ (f ⋆[L, μ] (g + g')) x = (f ⋆[L, μ] g + f ⋆[L, μ] g') x

Tactic:
exact (hfg x).distrib_add (hfg' x)

Premises used: MeasureTheory.ConvolutionExistsAt.distrib_add
-- 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 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 : AddGroup G
x : G
hfg : ConvolutionExistsAt f g x L μ
hfg' : ConvolutionExistsAt f' g x L μ
⊢ ((f + f') ⋆[L, μ] g) x = (f ⋆[L, μ] g) x + (f' ⋆[L, μ] g) x

Tactic:
simp only [convolution_def, L.map_add₂, Pi.add_apply, integral_add hfg hfg']

Premises used: MeasureTheory.convolution_def, Pi.add_apply, ContinuousLinearMap.map_add₂, MeasureTheory.integral_add
-- 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 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 : AddGroup G
hfg : ConvolutionExists f g L μ
hfg' : ConvolutionExists f' g L μ
h : ∀ (x : G), ((f + f') ⋆[L, μ] g) x = (f ⋆[L, μ] g + f' ⋆[L, μ] g) x
⊢ (f + f') ⋆[L, μ] g = f ⋆[L, μ] g + f' ⋆[L, μ] g

Tactic:
ext x
-- 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 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 : AddGroup G
hfg : ConvolutionExists f g L μ
hfg' : ConvolutionExists f' g L μ
x : G
⊢ ((f + f') ⋆[L, μ] g) x = (f ⋆[L, μ] g + f' ⋆[L, μ] g) x

Tactic:
(hfg x).add_distrib (hfg' x)

Premises used: MeasureTheory.ConvolutionExistsAt.add_distrib
-- 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 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 : AddGroup G
hfg : ConvolutionExists f g L μ
hfg' : ConvolutionExists f' g L μ
x : G
⊢ ((f + f') ⋆[L, μ] g) x = (f ⋆[L, μ] g + f' ⋆[L, μ] g) x

Tactic:
exact (hfg x).add_distrib (hfg' x)

Premises used: MeasureTheory.ConvolutionExistsAt.add_distrib