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
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
this_1 : LocallyCompactSpace G
q₀ : P
x₀ : G
hq₀ : (q₀, x₀).1 ∈ s
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := -k +ᵥ t
k'_comp : IsCompact k'
g' : P × G → G → E' := fun (p : P × G) (x : G) ↦ g p.1 (p.2 - x)
s' : Set (P × G) := s ×ˢ t
this : uncurry g' = uncurry g ∘ fun (w : (P × G) × G) ↦ (w.1.1, w.1.2 - w.2)
⊢ MapsTo (fun (w : (P × G) × G) ↦ (w.1.1, w.1.2 - w.2)) (SProd.sprod (β := Set G) s' univ)
    (SProd.sprod (β := Set G) s univ)

Tactic:
simp +contextual [s', MapsTo]

Premises used: Set.MapsTo
-- 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
this : LocallyCompactSpace G
q₀ : P
x₀ : G
hq₀ : (q₀, x₀).1 ∈ s
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := -k +ᵥ t
k'_comp : IsCompact k'
g' : P × G → G → E' := fun (p : P × G) (x : G) ↦ g p.1 (p.2 - x)
s' : Set (P × G) := s ×ˢ t
⊢ ContinuousOn (uncurry g') (SProd.sprod (β := Set G) s' univ)

Tactic:
have A : ContinuousOn g'.uncurry (s' ×ˢ univ) := by
    have : g'.uncurry = g.uncurry ∘ (fun w ↦ (w.1.1, w.1.2 - w.2)) := by ext y; rfl
    rw [this]
    refine hg.comp (by fun_prop) ?_
    simp +contextual [s', MapsTo]
-- 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
this : LocallyCompactSpace G
q₀ : P
x₀ : G
hq₀ : (q₀, x₀).1 ∈ s
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := -k +ᵥ t
k'_comp : IsCompact k'
g' : P × G → G → E' := fun (p : P × G) (x : G) ↦ g p.1 (p.2 - x)
s' : Set (P × G) := s ×ˢ t
A : ContinuousOn (uncurry g') (SProd.sprod (β := Set G) s' univ)
apply : ∀ (p : P × G) (x : G), p ∈ s' → x ∉ k' → g' p x = 0
⊢ ContinuousOn (Y := F)
    (fun (a : P × G) ↦ ∫ (x : G), (((L : (a : E) → E' →L[𝕜] F) (f x) : E' →L[𝕜] F) : (a : E') → F) (g' a x) ∂μ) s'

Tactic:
apply continuousOn_integral_bilinear_of_locally_integrable_of_compact_support L k'_comp A _
      (hf.integrableOn_isCompact k'_comp)

Premises used: MeasureTheory.LocallyIntegrable.integrableOn_isCompact, continuousOn_integral_bilinear_of_locally_integrable_of_compact_support
-- 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
this : LocallyCompactSpace G
q₀ : P
x₀ : G
hq₀ : (q₀, x₀).1 ∈ s
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := -k +ᵥ t
k'_comp : IsCompact k'
g' : P × G → G → E' := fun (p : P × G) (x : G) ↦ g p.1 (p.2 - x)
s' : Set (P × G) := s ×ˢ t
A : ContinuousOn (uncurry g') (SProd.sprod (β := Set G) s' univ)
p : P
x y : G
hp : (p, x).1 ∈ s
hx : (p, x).2 ∈ t
hy : y ∉ k'
apply : (p, x).2 - y ∉ k
⊢ g' (p, x) y = 0

Tactic:
apply hgs p _ hp
-- 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
this : LocallyCompactSpace G
q₀ : P
x₀ : G
hq₀ : (q₀, x₀).1 ∈ s
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := -k +ᵥ t
k'_comp : IsCompact k'
g' : P × G → G → E' := fun (p : P × G) (x : G) ↦ g p.1 (p.2 - x)
s' : Set (P × G) := s ×ˢ t
A : ContinuousOn (uncurry g') (SProd.sprod (β := Set G) s' univ)
p : P
x y : G
hp : (p, x).1 ∈ s
hx : (p, x).2 ∈ t
hy : y ∉ k'
contrapose : ∀ (hy : (p, x).2 - y ∈ k), y ∈ k'
⊢ (p, x).2 - y ∉ k

Tactic:
contrapose hy
-- 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
this : LocallyCompactSpace G
q₀ : P
x₀ : G
hq₀ : (q₀, x₀).1 ∈ s
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := -k +ᵥ t
k'_comp : IsCompact k'
g' : P × G → G → E' := fun (p : P × G) (x : G) ↦ g p.1 (p.2 - x)
s' : Set (P × G) := s ×ˢ t
A : ContinuousOn (uncurry g') (SProd.sprod (β := Set G) s' univ)
p : P
x y : G
hp : (p, x).1 ∈ s
hx : (p, x).2 ∈ t
hy : (p, x).2 - y ∈ k
⊢ y - x ∈ -k

Tactic:
simpa using hy
-- 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
this : LocallyCompactSpace G
q₀ : P
x₀ : G
hq₀ : (q₀, x₀).1 ∈ s
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := -k +ᵥ t
k'_comp : IsCompact k'
g' : P × G → G → E' := fun (p : P × G) (x : G) ↦ g p.1 (p.2 - x)
s' : Set (P × G) := s ×ˢ t
A : ContinuousOn (uncurry g') (SProd.sprod (β := Set G) s' univ)
p : P
x y : G
hp : (p, x).1 ∈ s
hx : (p, x).2 ∈ t
hy : (p, x).2 - y ∈ k
⊢ (fun (x1 x2 : G) ↦ x1 + x2) (y - x) x = y

Tactic:
simp
-- 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
this : LocallyCompactSpace G
q₀ : P
x₀ : G
hq₀ : (q₀, x₀).1 ∈ s
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := -k +ᵥ t
k'_comp : IsCompact k'
g' : P × G → G → E' := fun (p : P × G) (x : G) ↦ g p.1 (p.2 - x)
s' : Set (P × G) := s ×ˢ t
A : ContinuousOn (uncurry g') (SProd.sprod (β := Set G) s' univ)
p : P
x y : G
hp : (p, x).1 ∈ s
hx : (p, x).2 ∈ t
hy : (p, x).2 - y ∈ k
⊢ y ∈ k'

Tactic:
exact ⟨y - x, by simpa using hy, x, hx, by simp⟩
-- 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
this : LocallyCompactSpace G
q₀ : P
x₀ : G
hq₀ : (q₀, x₀).1 ∈ s
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := -k +ᵥ t
k'_comp : IsCompact k'
g' : P × G → G → E' := fun (p : P × G) (x : G) ↦ g p.1 (p.2 - x)
s' : Set (P × G) := s ×ˢ t
A : ContinuousOn (uncurry g') (SProd.sprod (β := Set G) s' univ)
⊢ ContinuousOn (Y := F)
    (fun (a : P × G) ↦ ∫ (x : G), (((L : (a : E) → E' →L[𝕜] F) (f x) : E' →L[𝕜] F) : (a : E') → F) (g' a x) ∂μ) s'

Tactic:
have B : ContinuousOn (fun a ↦ ∫ x, L (f x) (g' a x) ∂μ) s' := by
    apply continuousOn_integral_bilinear_of_locally_integrable_of_compact_support L k'_comp A _
      (hf.integrableOn_isCompact k'_comp)
    rintro ⟨p, x⟩ y ⟨hp, hx⟩ hy
    apply hgs p _ hp
    contrapose hy
    exact ⟨y - x, by simpa using hy, x, hx, by simp⟩
-- 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
this : LocallyCompactSpace G
q₀ : P
x₀ : G
hq₀ : (q₀, x₀).1 ∈ s
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := -k +ᵥ t
k'_comp : IsCompact k'
g' : P × G → G → E' := fun (p : P × G) (x : G) ↦ g p.1 (p.2 - x)
s' : Set (P × G) := s ×ˢ t
A : ContinuousOn (uncurry g') (SProd.sprod (β := Set G) s' univ)
B :
  ContinuousOn (Y := F)
    (fun (a : P × G) ↦ ∫ (x : G), (((L : (a : E) → E' →L[𝕜] F) (f x) : E' →L[𝕜] F) : (a : E') → F) (g' a x) ∂μ) s'
neg : s' ∈ 𝓝[SProd.sprod (β := Set G) s univ] (q₀, x₀)
⊢ ContinuousWithinAt (Y := F) (fun (q : P × G) ↦ (f ⋆[L, μ] g q.1) q.2) (SProd.sprod (β := Set G) s univ) (q₀, x₀)

Tactic:
apply ContinuousWithinAt.mono_of_mem_nhdsWithin (B (q₀, x₀) ⟨hq₀, mem_of_mem_nhds ht⟩)

Premises used: Prod.mk, mem_of_mem_nhds, ContinuousWithinAt.mono_of_mem_nhdsWithin, And.intro
-- 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
this : LocallyCompactSpace G
q₀ : P
x₀ : G
hq₀ : (q₀, x₀).1 ∈ s
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := -k +ᵥ t
k'_comp : IsCompact k'
g' : P × G → G → E' := fun (p : P × G) (x : G) ↦ g p.1 (p.2 - x)
s' : Set (P × G) := s ×ˢ t
A : ContinuousOn (uncurry g') (SProd.sprod (β := Set G) s' univ)
B :
  ContinuousOn (Y := F)
    (fun (a : P × G) ↦ ∫ (x : G), (((L : (a : E) → E' →L[𝕜] F) (f x) : E' →L[𝕜] F) : (a : E') → F) (g' a x) ∂μ) s'
⊢ s' ∈ 𝓝[SProd.sprod (β := Set G) s univ] (q₀, x₀)

Tactic:
mem_nhdsWithin_prod_iff.2 ⟨s, self_mem_nhdsWithin, t, nhdsWithin_le_nhds ht, Subset.rfl⟩

Premises used: Iff.mpr, Set.Mem, nhdsWithin_le_nhds, Set.Subset.rfl, self_mem_nhdsWithin, mem_nhdsWithin_prod_iff, And.intro, Exists.intro
-- 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
this : LocallyCompactSpace G
q₀ : P
x₀ : G
hq₀ : (q₀, x₀).1 ∈ s
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := -k +ᵥ t
k'_comp : IsCompact k'
g' : P × G → G → E' := fun (p : P × G) (x : G) ↦ g p.1 (p.2 - x)
s' : Set (P × G) := s ×ˢ t
A : ContinuousOn (uncurry g') (SProd.sprod (β := Set G) s' univ)
B :
  ContinuousOn (Y := F)
    (fun (a : P × G) ↦ ∫ (x : G), (((L : (a : E) → E' →L[𝕜] F) (f x) : E' →L[𝕜] F) : (a : E') → F) (g' a x) ∂μ) s'
⊢ s' ∈ 𝓝[SProd.sprod (β := Set G) s univ] (q₀, x₀)

Tactic:
exact mem_nhdsWithin_prod_iff.2 ⟨s, self_mem_nhdsWithin, t, nhdsWithin_le_nhds ht, Subset.rfl⟩

Premises used: Iff.mpr, nhdsWithin_le_nhds, Set.Subset.rfl, self_mem_nhdsWithin, mem_nhdsWithin_prod_iff, And.intro, Exists.intro
-- 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
s : Set P
v : P → G
hv : ContinuousOn v s
g : P → G → E'
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)
L₁ : MapsTo (fun (x : P) ↦ (id x, v x)) s (SProd.sprod (β := Set G) s univ)
⊢ ContinuousOn.{uP, uF} (Y := F) (fun (x : P) ↦ (f ⋆[L, μ] g x) (v x)) s

Tactic:
apply
    (continuousOn_convolution_right_with_param L hk hgs hf hg).comp (continuousOn_id.prodMk hv)

Premises used: ContinuousOn.comp, MeasureTheory.continuousOn_convolution_right_with_param, ContinuousOn.prodMk, continuousOn_id
-- 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
s : Set P
v : P → G
hv : ContinuousOn v s
g : P → G → E'
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)
x : P
hx : x ∈ s
⊢ (fun (x : P) ↦ (id x, v x)) x ∈ SProd.sprod (β := Set G) s univ

Tactic:
simp only [hx, prodMk_mem_set_prod_eq, mem_univ, and_self_iff, _root_.id]

Premises used: id, Set.prodMk_mem_set_prod_eq, Set.mem_univ, and_self_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 : AddGroup G
inst_10 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : BorelSpace G
hcg : HasCompactSupport g
hf : LocallyIntegrable f μ
hg : Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
rw : ContinuousOn (f ⋆[L, μ] g) univ
⊢ Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f ⋆[L, μ] g)

Tactic:
rw [← continuousOn_univ]

Premises used: continuousOn_univ
-- 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 : BorelSpace G
hcg : HasCompactSupport g
hf : LocallyIntegrable f μ
hg : Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g' : G → G → E' := fun (x q : G) ↦ g q
⊢ ContinuousOn (↿g') (SProd.sprod (α := Set G) (β := Set G) univ univ)

Tactic:
have : ContinuousOn ↿g' (univ ×ˢ univ) := (hg.comp continuous_snd).continuousOn
-- 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 : BorelSpace G
hcg : HasCompactSupport g
hf : LocallyIntegrable f μ
hg : Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g' : G → G → E' := fun (x q : G) ↦ g q
this : ContinuousOn (↿g') (SProd.sprod (α := Set G) (β := Set G) univ univ)
⊢ ContinuousOn (f ⋆[L, μ] g) univ

Tactic:
continuousOn_convolution_right_with_param_comp L
    (continuousOn_univ.2 continuous_id) hcg
    (fun p x _ hx => image_eq_zero_of_notMem_tsupport hx) hf this

Premises used: Iff.mpr, image_eq_zero_of_notMem_tsupport, MeasureTheory.continuousOn_convolution_right_with_param_comp, continuous_id, continuousOn_univ
-- 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 : BorelSpace G
hcg : HasCompactSupport g
hf : LocallyIntegrable f μ
hg : Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g' : G → G → E' := fun (x q : G) ↦ g q
this : ContinuousOn (↿g') (SProd.sprod (α := Set G) (β := Set G) univ univ)
⊢ ContinuousOn (f ⋆[L, μ] g) univ

Tactic:
exact continuousOn_convolution_right_with_param_comp L
    (continuousOn_univ.2 continuous_id) hcg
    (fun p x _ hx => image_eq_zero_of_notMem_tsupport hx) hf this

Premises used: Iff.mpr, image_eq_zero_of_notMem_tsupport, MeasureTheory.continuousOn_convolution_right_with_param_comp, continuous_id, continuousOn_univ
-- 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 : BorelSpace G
inst_13 : FirstCountableTopology G
inst_14 : SecondCountableTopologyEither G E'
hbg : BddAbove (α := ℝ) (range fun (x : G) ↦ ‖g x‖)
hf : Integrable f μ
hg : Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
⊢ Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f ⋆[L, μ] g)

Tactic:
continuous_iff_continuousAt.mpr fun x₀ => ?_

Premises used: Iff.mpr, continuous_iff_continuousAt