awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
x : G
inst : MeasurableSpace G
μ : Measure G
inst_1 : AddGroup G
f g g' : G → ℝ
hfg : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
apply :
  LE.le.{uG} (α := G → ℝ)
    (fun (t : G) ↦ (((lsmul ℝ ℝ : (a : ℝ) → ℝ →L[ℝ] ℝ) (f t) : ℝ →L[ℝ] ℝ) : (a : ℝ) → ℝ) (g (x - t))) fun (t : G) ↦
    (((lsmul ℝ ℝ : (a : ℝ) → ℝ →L[ℝ] ℝ) (f t) : ℝ →L[ℝ] ℝ) : (a : ℝ) → ℝ) (g' (x - t))
⊢ (f ⋆[lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x

Tactic:
apply integral_mono hfg hfg'

Premises used: MeasureTheory.integral_mono
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
x : G
inst : MeasurableSpace G
μ : Measure G
inst_1 : AddGroup G
f g g' : G → ℝ
hfg : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
t : G
ha : 0 ≤ f t
hbc : g (x - t) ≤ g' (x - t)
⊢ f t * g (x - t) ≤ f t * g' (x - t)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
x : G
inst : MeasurableSpace G
μ : Measure G
inst_1 : AddGroup G
f g g' : G → ℝ
hfg : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
t : G
⊢ 0 ≤ f t

Tactic:
hf _
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
x : G
inst : MeasurableSpace G
μ : Measure G
inst_1 : AddGroup G
f g g' : G → ℝ
hfg : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
t : G
⊢ g (x - t) ≤ g' (x - t)

Tactic:
hg _
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
x : G
inst : MeasurableSpace G
μ : Measure G
inst_1 : AddGroup G
f g g' : G → ℝ
hfg : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
t : G
⊢ 0 ≤ f t

Tactic:
exacts [hf _, hg _]
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
x : G
inst : MeasurableSpace G
μ : Measure G
inst_1 : AddGroup G
f g g' : G → ℝ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
hg' : ∀ (x : G), 0 ≤ g' x
pos : ∀ (H : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ), (f ⋆[lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x
neg : ∀ (H : ¬ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ), (f ⋆[lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x
⊢ (f ⋆[lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x

Tactic:
by_cases H : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ

Premises used: Real, MeasureTheory.ConvolutionExistsAt, ContinuousLinearMap.lsmul
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
x : G
inst : MeasurableSpace G
μ : Measure G
inst_1 : AddGroup G
f g g' : G → ℝ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
hg' : ∀ (x : G), 0 ≤ g' x
H : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
⊢ (f ⋆[lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x

Tactic:
convolution_mono_right H hfg' hf hg

Premises used: MeasureTheory.convolution_mono_right
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
x : G
inst : MeasurableSpace G
μ : Measure G
inst_1 : AddGroup G
f g g' : G → ℝ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
hg' : ∀ (x : G), 0 ≤ g' x
H : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
⊢ (f ⋆[lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x

Tactic:
exact convolution_mono_right H hfg' hf hg

Premises used: MeasureTheory.convolution_mono_right
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
x : G
inst : MeasurableSpace G
μ : Measure G
inst_1 : AddGroup G
f g g' : G → ℝ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
hg' : ∀ (x : G), 0 ≤ g' x
H : ¬ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
⊢ (f ⋆[lsmul ℝ ℝ, μ] g) x = 0

Tactic:
have : (f ⋆[lsmul ℝ ℝ, μ] g) x = 0 := integral_undef H
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
x : G
inst : MeasurableSpace G
μ : Measure G
inst_1 : AddGroup G
f g g' : G → ℝ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
hg' : ∀ (x : G), 0 ≤ g' x
H : ¬ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
this : (f ⋆[lsmul ℝ ℝ, μ] g) x = 0
neg : 0 ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x
⊢ (f ⋆[lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x

Tactic:
rw [this]
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
x : G
inst : MeasurableSpace G
μ : Measure G
inst_1 : AddGroup G
f g g' : G → ℝ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
hg' : ∀ (x : G), 0 ≤ g' x
H : ¬ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
this : (f ⋆[lsmul ℝ ℝ, μ] g) x = 0
⊢ 0 ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x

Tactic:
integral_nonneg fun y => mul_nonneg (hf y) (hg' (x - y))

Premises used: mul_nonneg, MeasureTheory.integral_nonneg, HSub.hSub, MeasureTheory.convolution
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
x : G
inst : MeasurableSpace G
μ : Measure G
inst_1 : AddGroup G
f g g' : G → ℝ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
hg' : ∀ (x : G), 0 ≤ g' x
H : ¬ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
this : (f ⋆[lsmul ℝ ℝ, μ] g) x = 0
⊢ 0 ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x

Tactic:
exact integral_nonneg fun y => mul_nonneg (hf y) (hg' (x - y))

Premises used: MeasureTheory.integral_nonneg
-- 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' : 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 : MeasurableAdd₂ G
inst_11 : MeasurableNeg G
inst_12 : SFinite μ
inst_13 : μ.IsAddRightInvariant
h1 : f =ᶠ[ae μ] f'
h2 : g =ᶠ[ae μ] g'
h : ∀ (x : G), (f ⋆[L, μ] g) x = (f' ⋆[L, μ] g') x
⊢ 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' : 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 : MeasurableAdd₂ G
inst_11 : MeasurableNeg G
inst_12 : SFinite μ
inst_13 : μ.IsAddRightInvariant
h1 : f =ᶠ[ae μ] f'
h2 : g =ᶠ[ae μ] g'
x : G
h :
  EventuallyEq.{uG, uF} (β := F) (ae μ)
    (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g (x - a))) fun (a : G) ↦
    (((L : (a : E) → E' →L[𝕜] F) (f' a) : E' →L[𝕜] F) : (a : E') → F) (g' (x - a))
⊢ (f ⋆[L, μ] g) x = (f' ⋆[L, μ] g') x

Tactic:
apply integral_congr_ae

Premises used: MeasureTheory.integral_congr_ae
-- 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' : 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 : MeasurableAdd₂ G
inst_11 : MeasurableNeg G
inst_12 : SFinite μ
inst_13 : μ.IsAddRightInvariant
h1 : f =ᶠ[ae μ] f'
h2 : g =ᶠ[ae μ] g'
x : G
⊢ EventuallyEq.{uG, uF} (β := F) (ae μ)
    (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g (x - a))) fun (a : G) ↦
    (((L : (a : E) → E' →L[𝕜] F) (f' a) : E' →L[𝕜] F) : (a : E') → F) (g' (x - a))

Tactic:
(h1.prodMk <| h2.comp_tendsto
    (quasiMeasurePreserving_sub_left_of_right_invariant μ x).tendsto_ae).fun_comp ↿fun x y ↦ L x y

Premises used: Filter.EventuallyEq.comp_tendsto, MeasureTheory.quasiMeasurePreserving_sub_left_of_right_invariant, MeasureTheory.Measure.QuasiMeasurePreserving.tendsto_ae, Function.HasUncurry.uncurry, Filter.EventuallyEq.fun_comp, DFunLike.coe, Filter.EventuallyEq.prodMk
-- 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' : 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 : MeasurableAdd₂ G
inst_11 : MeasurableNeg G
inst_12 : SFinite μ
inst_13 : μ.IsAddRightInvariant
h1 : f =ᶠ[ae μ] f'
h2 : g =ᶠ[ae μ] g'
x : G
⊢ EventuallyEq.{uG, uF} (β := F) (ae μ)
    (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g (x - a))) fun (a : G) ↦
    (((L : (a : E) → E' →L[𝕜] F) (f' a) : E' →L[𝕜] F) : (a : E') → F) (g' (x - a))

Tactic:
exact (h1.prodMk <| h2.comp_tendsto
    (quasiMeasurePreserving_sub_left_of_right_invariant μ x).tendsto_ae).fun_comp ↿fun x y ↦ L x y

Premises used: Filter.EventuallyEq.comp_tendsto, MeasureTheory.quasiMeasurePreserving_sub_left_of_right_invariant, MeasureTheory.Measure.QuasiMeasurePreserving.tendsto_ae, Function.HasUncurry.uncurry, Filter.EventuallyEq.fun_comp, DFunLike.coe, Filter.EventuallyEq.prodMk
-- 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
x : G
h2x : x ∈ support (f ⋆[L, μ] g)
by_contra : ∀ (hx : x ∉ support g + support f), False
⊢ x ∈ support g + support f

Tactic:
by_contra hx
-- 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
x : G
h2x : x ∈ support (f ⋆[L, μ] g)
hx : x ∉ support g + support f
apply : (f ⋆[L, μ] g) x = 0
⊢ False

Tactic:
apply h2x
-- 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
x : G
h2x : x ∈ support (f ⋆[L, μ] g)
hx : x ∉ support g + support f
⊢ ∀ (x_1 x_2 : G), g x_1 = 0 ∨ f x_2 = 0 ∨ ¬x_1 + x_2 = x

Tactic:
simp_rw [Set.mem_add, ← exists_and_left, not_exists, not_and_or, notMem_support] at hx

Premises used: not_exists, exists_and_left, Function.notMem_support, not_and_or, Set.mem_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 → 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
h2x : x ∈ support (f ⋆[L, μ] g)
hx : ∀ (x_1 x_2 : G), g x_1 = 0 ∨ f x_2 = 0 ∨ ¬x_1 + x_2 = x
rw : Eq.{uF + 1} (α := F) (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) ∂μ) 0
⊢ (f ⋆[L, μ] g) x = 0

Tactic:
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 : AddGroup G
x : G
h2x : x ∈ support (f ⋆[L, μ] g)
hx : ∀ (x_1 x_2 : G), g x_1 = 0 ∨ f x_2 = 0 ∨ ¬x_1 + x_2 = x
⊢ Eq.{uF + 1} (α := F) (∫ (x : G), 0 ∂μ) 0

Tactic:
integral_zero G F

Premises used: 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 → 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
h2x : x ∈ support (f ⋆[L, μ] g)
hx : ∀ (x_1 x_2 : G), g x_1 = 0 ∨ f x_2 = 0 ∨ ¬x_1 + x_2 = x
h :
  Eq (α := G → F) (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)))
    fun (x : G) ↦ 0
⊢ Eq.{uF + 1} (α := F) (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) ∂μ) 0

Tactic:
convert! integral_zero G F using 2

Premises used: 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 → 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
h2x : x ∈ support (f ⋆[L, μ] g)
hx : ∀ (x_1 x_2 : G), g x_1 = 0 ∨ f x_2 = 0 ∨ ¬x_1 + x_2 = x
h :
  ∀ (t : G),
    Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) (0 : F)
⊢ Eq (α := G → F) (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)))
    fun (x : G) ↦ 0

Tactic:
ext 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 : AddGroup G
x : G
h2x : x ∈ support (f ⋆[L, μ] g)
hx : ∀ (x_1 x_2 : G), g x_1 = 0 ∨ f x_2 = 0 ∨ ¬x_1 + x_2 = x
t : G
h :
  ∀ (h : g (x - t) = 0),
    Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) (0 : F)
h₁ :
  ∀ (h : f t = 0),
    Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) (0 : F)
h₂ :
  ∀ (h : ¬x - t + t = x),
    Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) (0 : F)
⊢ Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) (0 : F)

Tactic:
rcases hx (x - t) t with (h | h | h)

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 : AddGroup G
x : G
h2x : x ∈ support (f ⋆[L, μ] g)
hx : ∀ (x_1 x_2 : G), g x_1 = 0 ∨ f x_2 = 0 ∨ ¬x_1 + x_2 = x
t : G
h : g (x - t) = 0
h₁ : Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) 0 : F) (0 : F)
h₂ h₃ : Eq.{uF + 1} (α := F) 0 0
⊢ Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) (0 : F)

Tactic:
rw [h, (L _).map_zero]

Premises used: ContinuousLinearMap.map_zero, 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 : AddGroup G
x : G
h2x : x ∈ support (f ⋆[L, μ] g)
hx : ∀ (x_1 x_2 : G), g x_1 = 0 ∨ f x_2 = 0 ∨ ¬x_1 + x_2 = x
t : G
h : f t = 0
h₁ : Eq.{uF + 1} (α := F) (((L : (a : E) → E' →L[𝕜] F) 0 : (a : E') → F) (g (x - t)) : F) (0 : F)
h₂ h₃ : Eq.{uF + 1} (α := F) 0 0
⊢ Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) (0 : F)

Tactic:
rw [h, 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 : AddGroup G
x : G
h2x : x ∈ support (f ⋆[L, μ] g)
hx : ∀ (x_1 x_2 : G), g x_1 = 0 ∨ f x_2 = 0 ∨ ¬x_1 + x_2 = x
t : G
h : ¬x - t + t = x
⊢ Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) (0 : F)

Tactic:
(h <| sub_add_cancel x t).elim

Premises used: False.elim, sub_add_cancel
-- 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
x : G
h2x : x ∈ support (f ⋆[L, μ] g)
hx : ∀ (x_1 x_2 : G), g x_1 = 0 ∨ f x_2 = 0 ∨ ¬x_1 + x_2 = x
t : G
h : ¬x - t + t = x
⊢ Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) (0 : F)

Tactic:
exact (h <| sub_add_cancel x t).elim

Premises used: False.elim, sub_add_cancel
-- 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 : MeasurableAdd₂ G
inst_11 : MeasurableNeg G
inst_12 : SFinite μ
inst_13 : μ.IsAddRightInvariant
hf : Integrable f μ
hg : Integrable g μ
⊢ Integrable (f ⋆[L, μ] g) μ

Tactic:
(hf.convolution_integrand L hg).integral_prod_left

Premises used: MeasureTheory.Integrable.integral_prod_left, MeasureTheory.Integrable.convolution_integrand, MeasureTheory.convolution
-- 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 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : T2Space G
hcf : HasCompactSupport f
hcg : HasCompactSupport g
⊢ HasCompactSupport (f ⋆[L, μ] g)

Tactic:
(hcg.isCompact.add hcf).of_isClosed_subset isClosed_closure <|
    closure_minimal
      ((support_convolution_subset_swap L).trans <| add_subset_add subset_closure subset_closure)
      (hcg.isCompact.add hcf).isClosed

Premises used: subset_closure, closure_minimal, HasSubset.Subset.trans, HasCompactSupport.isCompact, IsCompact.of_isClosed_subset, Set.add_subset_add, MeasureTheory.support_convolution_subset_swap, isClosed_closure, IsCompact.add, HasCompactSupport, IsCompact.isClosed
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
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
inst_10 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : BorelSpace G
inst_13 : TopologicalSpace P
g : P → G → E'
s : Set P
k : Set G
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContinuousOn (↿g) (SProd.sprod (β := Set G) s univ)
pos :
  ∀ (H : ∀ p ∈ s, ∀ (x : G), g p x = 0),
    ContinuousOn (Y := F) (fun (q : P × G) ↦ (f ⋆[L, μ] g q.1) q.2) (SProd.sprod (β := Set G) s univ)
neg :
  ∀ (H : ∃ p ∈ s, ∃ (x : G), g p x ≠ 0),
    ContinuousOn (Y := F) (fun (q : P × G) ↦ (f ⋆[L, μ] g q.1) q.2) (SProd.sprod (β := Set G) s univ)
⊢ ContinuousOn (Y := F) (fun (q : P × G) ↦ (f ⋆[L, μ] g q.1) q.2) (SProd.sprod (β := Set G) s univ)

Tactic:
by_cases! H : ∀ p ∈ s, ∀ x, g p x = 0
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
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
inst_10 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : BorelSpace G
inst_13 : TopologicalSpace P
g : P → G → E'
s : Set P
k : Set G
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContinuousOn (↿g) (SProd.sprod (β := Set G) s univ)
H : ∀ p ∈ s, ∀ (x : G), g p x = 0
pos : EqOn (β := F) (fun (q : P × G) ↦ (f ⋆[L, μ] g q.1) q.2) (fun (x : P × G) ↦ 0) (SProd.sprod (β := Set G) s univ)
⊢ ContinuousOn (Y := F) (fun (q : P × G) ↦ (f ⋆[L, μ] g q.1) q.2) (SProd.sprod (β := Set G) s univ)

Tactic:
apply (continuousOn_const (c := 0)).congr

Premises used: continuousOn_const, ContinuousOn.congr