awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.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 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedAddCommGroup P
inst_13 : NormedSpace 𝕜 P
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 1 (↿g) (SProd.sprod (β := Set G) s univ)
q₀ : P × G
hq₀ : q₀.1 ∈ s
g' : (x : P × G) → P × G →L[𝕜] E' := fderiv 𝕜 ↿g
A :
  ∀ p ∈ s,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (g p)
A' : ∀ (q : P × G), q.1 ∈ s → SProd.sprod (β := Set G) s univ ∈ 𝓝 q
g'_zero : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g' (p, x) = 0
ε C : ℝ
εpos : 0 < ε
h₀ε : ball q₀.1 ε ⊆ s
hε : ∀ (p : P) (x : G), ‖p - q₀.1‖ < ε → ‖g' (p, x)‖ ≤ C
I1 :
  ∀ᶠ (x : P × G) in 𝓝 q₀,
    AEStronglyMeasurable.{uG, uF} (β := F)
      (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g x.1 (x.2 - a))) μ
I2 :
  Integrable.{uF, uG} (ε := F)
    (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g q₀.1 (q₀.2 - a))) μ
⊢ HasCompactSupport (β := P × G →L[𝕜] E') fun (y : G) ↦ g' (q₀.1, y)

Tactic:
have T : HasCompactSupport fun y => g' (q₀.1, y) :=
      HasCompactSupport.intro hk fun x hx => g'_zero q₀.1 x hq₀ hx
-- Module: Mathlib.Analysis.Calculus.ContDiff.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 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedAddCommGroup P
inst_13 : NormedSpace 𝕜 P
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 1 (↿g) (SProd.sprod (β := Set G) s univ)
q₀ : P × G
hq₀ : q₀.1 ∈ s
g' : (x : P × G) → P × G →L[𝕜] E' := fderiv 𝕜 ↿g
A :
  ∀ p ∈ s,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (g p)
A' : ∀ (q : P × G), q.1 ∈ s → SProd.sprod (β := Set G) s univ ∈ 𝓝 q
g'_zero : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g' (p, x) = 0
ε C : ℝ
εpos : 0 < ε
h₀ε : ball q₀.1 ε ⊆ s
hε : ∀ (p : P) (x : G), ‖p - q₀.1‖ < ε → ‖g' (p, x)‖ ≤ C
I1 :
  ∀ᶠ (x : P × G) in 𝓝 q₀,
    AEStronglyMeasurable.{uG, uF} (β := F)
      (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g x.1 (x.2 - a))) μ
I2 :
  Integrable.{uF, uG} (ε := F)
    (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g q₀.1 (q₀.2 - a))) μ
T : HasCompactSupport (β := P × G →L[𝕜] E') fun (y : G) ↦ g' (q₀.1, y)
apply : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (y : G) ↦ g' (q₀.1, y)
⊢ AEStronglyMeasurable (β := P × G →L[𝕜] F)
    (fun (a : G) ↦
      ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) ((L : (a : E) → E' →L[𝕜] F) (f a)) (g' (q₀.1, q₀.2 - a)))
    μ

Tactic:
apply (HasCompactSupport.convolutionExists_right (L.precompR (P × G) :) T hf _ q₀.2).1

Premises used: HasCompactSupport.convolutionExists_right, And.left, Prod, Prod.snd, ContinuousLinearMap.precompR
-- Module: Mathlib.Analysis.Calculus.ContDiff.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 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedAddCommGroup P
inst_13 : NormedSpace 𝕜 P
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 1 (↿g) (SProd.sprod (β := Set G) s univ)
q₀ : P × G
hq₀ : q₀.1 ∈ s
g' : (x : P × G) → P × G →L[𝕜] E' := fderiv 𝕜 ↿g
A :
  ∀ p ∈ s,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (g p)
A' : ∀ (q : P × G), q.1 ∈ s → SProd.sprod (β := Set G) s univ ∈ 𝓝 q
g'_zero : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g' (p, x) = 0
ε C : ℝ
εpos : 0 < ε
h₀ε : ball q₀.1 ε ⊆ s
hε : ∀ (p : P) (x : G), ‖p - q₀.1‖ < ε → ‖g' (p, x)‖ ≤ C
I1 :
  ∀ᶠ (x : P × G) in 𝓝 q₀,
    AEStronglyMeasurable.{uG, uF} (β := F)
      (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g x.1 (x.2 - a))) μ
I2 :
  Integrable.{uF, uG} (ε := F)
    (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g q₀.1 (q₀.2 - a))) μ
T : HasCompactSupport (β := P × G →L[𝕜] E') fun (y : G) ↦ g' (q₀.1, y)
⊢ ContinuousOn g' (SProd.sprod (β := Set G) s univ)

Tactic:
have : ContinuousOn g' (s ×ˢ univ) :=
      hg.continuousOn_fderiv_of_isOpen (hs.prod isOpen_univ) le_rfl
-- Module: Mathlib.Analysis.Calculus.ContDiff.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 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedAddCommGroup P
inst_13 : NormedSpace 𝕜 P
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 1 (↿g) (SProd.sprod (β := Set G) s univ)
q₀ : P × G
hq₀ : q₀.1 ∈ s
g' : (x : P × G) → P × G →L[𝕜] E' := fderiv 𝕜 ↿g
A :
  ∀ p ∈ s,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (g p)
A' : ∀ (q : P × G), q.1 ∈ s → SProd.sprod (β := Set G) s univ ∈ 𝓝 q
g'_zero : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g' (p, x) = 0
ε C : ℝ
εpos : 0 < ε
h₀ε : ball q₀.1 ε ⊆ s
hε : ∀ (p : P) (x : G), ‖p - q₀.1‖ < ε → ‖g' (p, x)‖ ≤ C
I1 :
  ∀ᶠ (x : P × G) in 𝓝 q₀,
    AEStronglyMeasurable.{uG, uF} (β := F)
      (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g x.1 (x.2 - a))) μ
I2 :
  Integrable.{uF, uG} (ε := F)
    (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g q₀.1 (q₀.2 - a))) μ
T : HasCompactSupport (β := P × G →L[𝕜] E') fun (y : G) ↦ g' (q₀.1, y)
this : ContinuousOn g' (SProd.sprod (β := Set G) s univ)
apply : ∀ (x : G), (q₀.1, x) ∈ SProd.sprod (β := Set G) s univ
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (y : G) ↦ g' (q₀.1, y)

Tactic:
apply this.comp_continuous (.prodMk_right _)

Premises used: ContinuousOn.comp_continuous, Continuous.prodMk_right
-- Module: Mathlib.Analysis.Calculus.ContDiff.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 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedAddCommGroup P
inst_13 : NormedSpace 𝕜 P
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 1 (↿g) (SProd.sprod (β := Set G) s univ)
q₀ : P × G
hq₀ : q₀.1 ∈ s
g' : (x : P × G) → P × G →L[𝕜] E' := fderiv 𝕜 ↿g
A :
  ∀ p ∈ s,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (g p)
A' : ∀ (q : P × G), q.1 ∈ s → SProd.sprod (β := Set G) s univ ∈ 𝓝 q
g'_zero : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g' (p, x) = 0
ε C : ℝ
εpos : 0 < ε
h₀ε : ball q₀.1 ε ⊆ s
hε : ∀ (p : P) (x : G), ‖p - q₀.1‖ < ε → ‖g' (p, x)‖ ≤ C
I1 :
  ∀ᶠ (x : P × G) in 𝓝 q₀,
    AEStronglyMeasurable.{uG, uF} (β := F)
      (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g x.1 (x.2 - a))) μ
I2 :
  Integrable.{uF, uG} (ε := F)
    (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g q₀.1 (q₀.2 - a))) μ
T : HasCompactSupport (β := P × G →L[𝕜] E') fun (y : G) ↦ g' (q₀.1, y)
this : ContinuousOn g' (SProd.sprod (β := Set G) s univ)
x : G
⊢ (q₀.1, x) ∈ SProd.sprod (β := Set G) s univ

Tactic:
simpa only [prodMk_mem_set_prod_eq, mem_univ, and_true] using hq₀

Premises used: and_true, Set.prodMk_mem_set_prod_eq, Set.mem_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.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 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedAddCommGroup P
inst_13 : NormedSpace 𝕜 P
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 1 (↿g) (SProd.sprod (β := Set G) s univ)
q₀ : P × G
hq₀ : q₀.1 ∈ s
g' : (x : P × G) → P × G →L[𝕜] E' := fderiv 𝕜 ↿g
A :
  ∀ p ∈ s,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (g p)
A' : ∀ (q : P × G), q.1 ∈ s → SProd.sprod (β := Set G) s univ ∈ 𝓝 q
g'_zero : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g' (p, x) = 0
ε C : ℝ
εpos : 0 < ε
h₀ε : ball q₀.1 ε ⊆ s
hε : ∀ (p : P) (x : G), ‖p - q₀.1‖ < ε → ‖g' (p, x)‖ ≤ C
I1 :
  ∀ᶠ (x : P × G) in 𝓝 q₀,
    AEStronglyMeasurable.{uG, uF} (β := F)
      (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g x.1 (x.2 - a))) μ
I2 :
  Integrable.{uF, uG} (ε := F)
    (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g q₀.1 (q₀.2 - a))) μ
⊢ AEStronglyMeasurable (β := P × G →L[𝕜] F)
    (fun (a : G) ↦
      ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) ((L : (a : E) → E' →L[𝕜] F) (f a)) (g' (q₀.1, q₀.2 - a)))
    μ

Tactic:
have I3 : AEStronglyMeasurable (fun a : G => (L (f a)).comp (g' (q₀.fst, q₀.snd - a))) μ := by
    have T : HasCompactSupport fun y => g' (q₀.1, y) :=
      HasCompactSupport.intro hk fun x hx => g'_zero q₀.1 x hq₀ hx
    apply (HasCompactSupport.convolutionExists_right (L.precompR (P × G) :) T hf _ q₀.2).1
    have : ContinuousOn g' (s ×ˢ univ) :=
      hg.continuousOn_fderiv_of_isOpen (hs.prod isOpen_univ) le_rfl
    apply this.comp_continuous (.prodMk_right _)
    intro x
    simpa only [prodMk_mem_set_prod_eq, mem_univ, and_true] using hq₀
-- Module: Mathlib.Analysis.Calculus.ContDiff.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 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedAddCommGroup P
inst_13 : NormedSpace 𝕜 P
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 1 (↿g) (SProd.sprod (β := Set G) s univ)
q₀ : P × G
hq₀ : q₀.1 ∈ s
g' : (x : P × G) → P × G →L[𝕜] E' := fderiv 𝕜 ↿g
A :
  ∀ p ∈ s,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (g p)
A' : ∀ (q : P × G), q.1 ∈ s → SProd.sprod (β := Set G) s univ ∈ 𝓝 q
g'_zero : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g' (p, x) = 0
ε C : ℝ
εpos : 0 < ε
h₀ε : ball q₀.1 ε ⊆ s
hε : ∀ (p : P) (x : G), ‖p - q₀.1‖ < ε → ‖g' (p, x)‖ ≤ C
I1 :
  ∀ᶠ (x : P × G) in 𝓝 q₀,
    AEStronglyMeasurable.{uG, uF} (β := F)
      (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g x.1 (x.2 - a))) μ
I2 :
  Integrable.{uF, uG} (ε := F)
    (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g q₀.1 (q₀.2 - a))) μ
I3 :
  AEStronglyMeasurable (β := P × G →L[𝕜] F)
    (fun (a : G) ↦
      ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) ((L : (a : E) → E' →L[𝕜] F) (f a)) (g' (q₀.1, q₀.2 - a)))
    μ
⊢ let K' := -k + {q₀.2};
  K' = -k + {q₀.2}

Tactic:
set K' := (-k + {q₀.2} : Set G) with K'_def

Premises used: HAdd.hAdd, Singleton.singleton, Prod.snd, Neg.neg
-- Module: Mathlib.Analysis.Calculus.ContDiff.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 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedAddCommGroup P
inst_13 : NormedSpace 𝕜 P
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 1 (↿g) (SProd.sprod (β := Set G) s univ)
q₀ : P × G
hq₀ : q₀.1 ∈ s
g' : (x : P × G) → P × G →L[𝕜] E' := fderiv 𝕜 ↿g
A :
  ∀ p ∈ s,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (g p)
A' : ∀ (q : P × G), q.1 ∈ s → SProd.sprod (β := Set G) s univ ∈ 𝓝 q
g'_zero : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g' (p, x) = 0
ε C : ℝ
εpos : 0 < ε
h₀ε : ball q₀.1 ε ⊆ s
hε : ∀ (p : P) (x : G), ‖p - q₀.1‖ < ε → ‖g' (p, x)‖ ≤ C
I1 :
  ∀ᶠ (x : P × G) in 𝓝 q₀,
    AEStronglyMeasurable.{uG, uF} (β := F)
      (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g x.1 (x.2 - a))) μ
I2 :
  Integrable.{uF, uG} (ε := F)
    (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g q₀.1 (q₀.2 - a))) μ
I3 :
  AEStronglyMeasurable (β := P × G →L[𝕜] F)
    (fun (a : G) ↦
      ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) ((L : (a : E) → E' →L[𝕜] F) (f a)) (g' (q₀.1, q₀.2 - a)))
    μ
K' : Set G := -k + {q₀.2}
K'_def : K' = -k + {q₀.2}
⊢ IsCompact K'

Tactic:
have hK' : IsCompact K' := hk.neg.add isCompact_singleton
-- Module: Mathlib.Analysis.Calculus.ContDiff.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 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedAddCommGroup P
inst_13 : NormedSpace 𝕜 P
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 1 (↿g) (SProd.sprod (β := Set G) s univ)
q₀ : P × G
hq₀ : q₀.1 ∈ s
g' : (x : P × G) → P × G →L[𝕜] E' := fderiv 𝕜 ↿g
A :
  ∀ p ∈ s,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (g p)
A' : ∀ (q : P × G), q.1 ∈ s → SProd.sprod (β := Set G) s univ ∈ 𝓝 q
g'_zero : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g' (p, x) = 0
ε C : ℝ
εpos : 0 < ε
h₀ε : ball q₀.1 ε ⊆ s
hε : ∀ (p : P) (x : G), ‖p - q₀.1‖ < ε → ‖g' (p, x)‖ ≤ C
I1 :
  ∀ᶠ (x : P × G) in 𝓝 q₀,
    AEStronglyMeasurable.{uG, uF} (β := F)
      (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g x.1 (x.2 - a))) μ
I2 :
  Integrable.{uF, uG} (ε := F)
    (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g q₀.1 (q₀.2 - a))) μ
I3 :
  AEStronglyMeasurable (β := P × G →L[𝕜] F)
    (fun (a : G) ↦
      ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) ((L : (a : E) → E' →L[𝕜] F) (f a)) (g' (q₀.1, q₀.2 - a)))
    μ
K' : Set G := -k + {q₀.2}
K'_def : K' = -k + {q₀.2}
hK' : IsCompact K'
⊢ ∃ (U : Set G), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U ∧ K' ⊆ U ∧ IntegrableOn f U μ

Tactic:
hf.integrableOn_nhds_isCompact hK'

Premises used: MeasureTheory.LocallyIntegrable.integrableOn_nhds_isCompact
-- Module: Mathlib.Analysis.Calculus.ContDiff.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 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedAddCommGroup P
inst_13 : NormedSpace 𝕜 P
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 1 (↿g) (SProd.sprod (β := Set G) s univ)
q₀ : P × G
hq₀ : q₀.1 ∈ s
g' : (x : P × G) → P × G →L[𝕜] E' := fderiv 𝕜 ↿g
A :
  ∀ p ∈ s,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (g p)
A' : ∀ (q : P × G), q.1 ∈ s → SProd.sprod (β := Set G) s univ ∈ 𝓝 q
g'_zero : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g' (p, x) = 0
ε C : ℝ
εpos : 0 < ε
h₀ε : ball q₀.1 ε ⊆ s
hε : ∀ (p : P) (x : G), ‖p - q₀.1‖ < ε → ‖g' (p, x)‖ ≤ C
I1 :
  ∀ᶠ (x : P × G) in 𝓝 q₀,
    AEStronglyMeasurable.{uG, uF} (β := F)
      (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g x.1 (x.2 - a))) μ
I2 :
  Integrable.{uF, uG} (ε := F)
    (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g q₀.1 (q₀.2 - a))) μ
I3 :
  AEStronglyMeasurable (β := P × G →L[𝕜] F)
    (fun (a : G) ↦
      ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) ((L : (a : E) → E' →L[𝕜] F) (f a)) (g' (q₀.1, q₀.2 - a)))
    μ
K' : Set G := -k + {q₀.2}
K'_def : K' = -k + {q₀.2}
hK' : IsCompact K'
obtain :
  ∀ (U : Set G) (U_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) (K'U : K' ⊆ U)
    (hU : IntegrableOn f U μ),
    HasFDerivAt (𝕜 := 𝕜) (F := F) (fun (q : P × G) ↦ convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) f (g q.1) L μ q.2)
      (convolution (𝕜 := 𝕜) (E' := P × G →L[𝕜] E') f (fun (x : G) ↦ fderiv 𝕜 ↿g (q₀.1, x)) (precompR (P × G) L) μ q₀.2)
      q₀
⊢ HasFDerivAt (𝕜 := 𝕜) (F := F) (fun (q : P × G) ↦ convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) f (g q.1) L μ q.2)
    (convolution (𝕜 := 𝕜) (E' := P × G →L[𝕜] E') f (fun (x : G) ↦ fderiv 𝕜 ↿g (q₀.1, x)) (precompR (P × G) L) μ q₀.2) q₀

Tactic:
obtain ⟨U, U_open, K'U, hU⟩ : ∃ U, IsOpen U ∧ K' ⊆ U ∧ IntegrableOn f U μ :=
    hf.integrableOn_nhds_isCompact hK'

Premises used: MeasureTheory.LocallyIntegrable.integrableOn_nhds_isCompact
-- Module: Mathlib.Analysis.Calculus.ContDiff.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 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedAddCommGroup P
inst_13 : NormedSpace 𝕜 P
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 1 (↿g) (SProd.sprod (β := Set G) s univ)
q₀ : P × G
hq₀ : q₀.1 ∈ s
g' : (x : P × G) → P × G →L[𝕜] E' := fderiv 𝕜 ↿g
A :
  ∀ p ∈ s,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (g p)
A' : ∀ (q : P × G), q.1 ∈ s → SProd.sprod (β := Set G) s univ ∈ 𝓝 q
g'_zero : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g' (p, x) = 0
ε C : ℝ
εpos : 0 < ε
h₀ε : ball q₀.1 ε ⊆ s
hε : ∀ (p : P) (x : G), ‖p - q₀.1‖ < ε → ‖g' (p, x)‖ ≤ C
I1 :
  ∀ᶠ (x : P × G) in 𝓝 q₀,
    AEStronglyMeasurable.{uG, uF} (β := F)
      (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g x.1 (x.2 - a))) μ
I2 :
  Integrable.{uF, uG} (ε := F)
    (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g q₀.1 (q₀.2 - a))) μ
I3 :
  AEStronglyMeasurable (β := P × G →L[𝕜] F)
    (fun (a : G) ↦
      ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) ((L : (a : E) → E' →L[𝕜] F) (f a)) (g' (q₀.1, q₀.2 - a)))
    μ
K' : Set G := -k + {q₀.2}
K'_def : K' = -k + {q₀.2}
hK' : IsCompact K'
U : Set G
U_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
K'U : K' ⊆ U
hU : IntegrableOn f U μ
⊢ ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 0) V ∧ K' + V ⊆ U

Tactic:
compact_open_separated_add_right hK' U_open K'U

Premises used: compact_open_separated_add_right, Set.Mem