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
p : P
x : G
hp : (p, x).1 ∈ s
apply :
  ∀ (y : G),
    Eq.{uF + 1} (α := F)
      ((((L : (a : E) → E' →L[𝕜] F) (f y) : E' →L[𝕜] F) : (a : E') → F) (g (p, x).1 ((p, x).2 - y)) : F) (0 y : F)
⊢ Eq.{uF + 1} (α := F) ((fun (q : P × G) ↦ (f ⋆[L, μ] g q.1) q.2) (p, x)) ((fun (x : P × G) ↦ (0 : F)) (p, x))

Tactic:
apply integral_eq_zero_of_ae (Eventually.of_forall (fun y ↦ ?_))

Premises used: Filter.Eventually.of_forall, MeasureTheory.integral_eq_zero_of_ae
-- 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
p : P
x : G
hp : (p, x).1 ∈ s
y : G
⊢ Eq.{uF + 1} (α := F)
    ((((L : (a : E) → E' →L[𝕜] F) (f y) : E' →L[𝕜] F) : (a : E') → F) (g (p, x).1 ((p, x).2 - y)) : F) (0 y : F)

Tactic:
simp [H 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
rcases : ∀ (p : P) (hp : p ∈ s) (x : G) (hx : g p x ≠ 0), LocallyCompactSpace G
⊢ LocallyCompactSpace G

Tactic:
rcases H with ⟨p, hp, x, hx⟩
-- 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)
p : P
hp : p ∈ s
x : G
hx : g p x ≠ 0
⊢ support (g p) ⊆ k

Tactic:
have A : support (g p) ⊆ k := support_subset_iff'.2 (fun y hy ↦ hgs p y hp 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)
p : P
hp : p ∈ s
x : G
hx : g p x ≠ 0
A : support (g p) ⊆ k
⊢ Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (g p)

Tactic:
hg.comp_continuous (.prodMk_right _) fun x => ?_

Premises used: ContinuousOn.comp_continuous, Continuous.prodMk_right
-- 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)
p : P
hp : p ∈ s
x : G
hx : g p x ≠ 0
A : support (g p) ⊆ k
refine : ∀ (x : G), (p, x) ∈ SProd.sprod (β := Set G) s univ
⊢ Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (g p)

Tactic:
refine hg.comp_continuous (.prodMk_right _) fun x => ?_

Premises used: ContinuousOn.comp_continuous, Continuous.prodMk_right
-- 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)
p : P
hp : p ∈ s
x_1 : G
hx : g p x_1 ≠ 0
A : support (g p) ⊆ k
x : G
⊢ (p, x) ∈ SProd.sprod (β := Set G) s univ

Tactic:
simpa only [prodMk_mem_set_prod_eq, mem_univ, and_true] using hp

Premises used: and_true, Set.prodMk_mem_set_prod_eq, Set.mem_univ
-- 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)
p : P
hp : p ∈ s
x : G
hx : g p x ≠ 0
A : support (g p) ⊆ k
⊢ Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (g p)

Tactic:
have B : Continuous (g p) := by
      refine hg.comp_continuous (.prodMk_right _) fun x => ?_
      simpa only [prodMk_mem_set_prod_eq, mem_univ, and_true] using 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)
p : P
hp : p ∈ s
x : G
hx : g p x ≠ 0
A : support (g p) ⊆ k
B : Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (g p)
inl : ∀ (H : g p = 0), LocallyCompactSpace G
inr : ∀ (H : LocallyCompactSpace G), LocallyCompactSpace G
⊢ LocallyCompactSpace G

Tactic:
rcases eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_of_addGroup hk A B with H | H

Premises used: eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_of_addGroup
-- 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)
p : P
hp : p ∈ s
x : G
hx : g p x ≠ 0
A : support (g p) ⊆ k
B : Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (g p)
H : g p = 0
⊢ LocallyCompactSpace G

Tactic:
simp [H] at hx
-- 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)
p : P
hp : p ∈ s
x : G
hx : g p x ≠ 0
A : support (g p) ⊆ k
B : Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (g p)
H : LocallyCompactSpace G
⊢ LocallyCompactSpace G

Tactic:
H
-- 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)
p : P
hp : p ∈ s
x : G
hx : g p x ≠ 0
A : support (g p) ⊆ k
B : Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (g p)
H : LocallyCompactSpace G
⊢ LocallyCompactSpace G

Tactic:
exact H
-- 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
⊢ LocallyCompactSpace G

Tactic:
have : LocallyCompactSpace G := by
    rcases H with ⟨p, hp, x, hx⟩
    have A : support (g p) ⊆ k := support_subset_iff'.2 (fun y hy ↦ hgs p y hp hy)
    have B : Continuous (g p) := by
      refine hg.comp_continuous (.prodMk_right _) fun x => ?_
      simpa only [prodMk_mem_set_prod_eq, mem_univ, and_true] using hp
    rcases eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_of_addGroup hk A B with H | H
    · simp [H] at hx
    · exact H
-- 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), IsCompact t ∧ t ∈ 𝓝 x₀

Tactic:
exists_compact_mem_nhds x₀

Premises used: WeaklyLocallyCompactSpace.exists_compact_mem_nhds
-- 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
neg :
  ∀ (t : Set G) (t_comp : IsCompact t) (ht : t ∈ 𝓝 x₀),
    ContinuousWithinAt (Y := F) (fun (q : P × G) ↦ (f ⋆[L, μ] g q.1) q.2) (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:
obtain ⟨t, t_comp, ht⟩ : ∃ t, IsCompact t ∧ t ∈ 𝓝 x₀ := exists_compact_mem_nhds x₀

Premises used: WeaklyLocallyCompactSpace.exists_compact_mem_nhds, nhds
-- 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
⊢ IsCompact k'

Tactic:
have k'_comp : IsCompact k' := IsCompact.vadd_set hk.neg t_comp
-- 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
h : ∀ (y : (P × G) × G), uncurry g' y = (uncurry g ∘ fun (w : (P × G) × G) ↦ (w.1.1, w.1.2 - w.2)) y
⊢ uncurry g' = uncurry g ∘ fun (w : (P × G) × G) ↦ (w.1.1, w.1.2 - w.2)

Tactic:
ext y
-- 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
y : (P × G) × G
⊢ uncurry g' y = (uncurry g ∘ fun (w : (P × G) × G) ↦ (w.1.1, w.1.2 - w.2)) y

Tactic:
rfl
-- 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
⊢ uncurry g' = uncurry g ∘ fun (w : (P × G) × G) ↦ (w.1.1, w.1.2 - w.2)

Tactic:
have : g'.uncurry = g.uncurry ∘ (fun w ↦ (w.1.1, w.1.2 - w.2)) := by ext y; rfl
-- 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)
rw : ContinuousOn (uncurry g ∘ fun (w : (P × G) × G) ↦ (w.1.1, w.1.2 - w.2)) (SProd.sprod (β := Set G) s' univ)
⊢ ContinuousOn (uncurry g') (SProd.sprod (β := Set G) s' univ)

Tactic:
rw [this]
-- 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)
⊢ ContinuousOn (Y := P × G) (fun (w : (P × G) × G) ↦ (w.1.1, w.1.2 - w.2)) (SProd.sprod (β := Set G) s' univ)

Tactic:
fun_prop
-- 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)
refine :
  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)
⊢ ContinuousOn (uncurry g ∘ fun (w : (P × G) × G) ↦ (w.1.1, w.1.2 - w.2)) (SProd.sprod (β := Set G) s' univ)

Tactic:
refine hg.comp (by fun_prop) ?_

Premises used: ContinuousOn.comp