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))) μ
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 μ
δ : ℝ
δpos : 0 < δ
δε : δ ≤ ε
hδ : K' + ball 0 δ ⊆ U
this : Norm (E →L[𝕜] (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) :=
  hasOpNorm (𝕜 := 𝕜) (𝕜₂ := 𝕜) (E := E) (F := (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (σ₁₂ := RingHom.id 𝕜)
bound : G → ℝ :=
  U.indicator fun (t : G) ↦ norm (E := E →L[𝕜] (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (precompR (P × G) L) * ‖f t‖ * C
a : G
x : P × G
hx : max ‖x.1 - q₀.1‖ ‖x.2 - q₀.2‖ < δ
apply : (-tsupport (α := P × G →L[𝕜] E') fun (a : G) ↦ g' (x.1, a)) + ball q₀.2 δ ⊆ K' + ball 0 δ
⊢ (-tsupport (α := P × G →L[𝕜] E') fun (a : G) ↦ g' (x.1, a)) + ball q₀.2 δ ⊆ U

Tactic:
apply Subset.trans _ hδ

Premises used: Set.Subset.trans
-- 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 μ
δ : ℝ
δpos : 0 < δ
δε : δ ≤ ε
hδ : K' + ball 0 δ ⊆ U
this : Norm (E →L[𝕜] (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) :=
  hasOpNorm (𝕜 := 𝕜) (𝕜₂ := 𝕜) (E := E) (F := (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (σ₁₂ := RingHom.id 𝕜)
bound : G → ℝ :=
  U.indicator fun (t : G) ↦ norm (E := E →L[𝕜] (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (precompR (P × G) L) * ‖f t‖ * C
a : G
x : P × G
hx : max ‖x.1 - q₀.1‖ ‖x.2 - q₀.2‖ < δ
rw :
  (-tsupport (α := P × G →L[𝕜] E') fun (a : G) ↦ g' (x.1, a)) + ball q₀.2 δ ⊆
    -k + HAdd.hAdd (α := Set G) {q₀.2} (ball 0 δ)
⊢ (-tsupport (α := P × G →L[𝕜] E') fun (a : G) ↦ g' (x.1, a)) + ball q₀.2 δ ⊆ K' + ball 0 δ

Tactic:
rw [K'_def, add_assoc]

Premises used: add_assoc
-- 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 μ
δ : ℝ
δpos : 0 < δ
δε : δ ≤ ε
hδ : K' + ball 0 δ ⊆ U
this : Norm (E →L[𝕜] (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) :=
  hasOpNorm (𝕜 := 𝕜) (𝕜₂ := 𝕜) (E := E) (F := (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (σ₁₂ := RingHom.id 𝕜)
bound : G → ℝ :=
  U.indicator fun (t : G) ↦ norm (E := E →L[𝕜] (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (precompR (P × G) L) * ‖f t‖ * C
a : G
x : P × G
hx : max ‖x.1 - q₀.1‖ ‖x.2 - q₀.2‖ < δ
a₁ : (-tsupport (α := P × G →L[𝕜] E') fun (a : G) ↦ g' (x.1, a)) ⊆ -k
a₂ : ball q₀.2 δ ⊆ HAdd.hAdd (α := Set G) {q₀.2} (ball 0 δ)
⊢ (-tsupport (α := P × G →L[𝕜] E') fun (a : G) ↦ g' (x.1, a)) + ball q₀.2 δ ⊆
    -k + HAdd.hAdd (α := Set G) {q₀.2} (ball 0 δ)

Tactic:
apply add_subset_add

Premises used: Set.add_subset_add
-- 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 μ
δ : ℝ
δpos : 0 < δ
δε : δ ≤ ε
hδ : K' + ball 0 δ ⊆ U
this : Norm (E →L[𝕜] (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) :=
  hasOpNorm (𝕜 := 𝕜) (𝕜₂ := 𝕜) (E := E) (F := (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (σ₁₂ := RingHom.id 𝕜)
bound : G → ℝ :=
  U.indicator fun (t : G) ↦ norm (E := E →L[𝕜] (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (precompR (P × G) L) * ‖f t‖ * C
a : G
x : P × G
hx : max ‖x.1 - q₀.1‖ ‖x.2 - q₀.2‖ < δ
a₁ : (tsupport (α := P × G →L[𝕜] E') fun (a : G) ↦ g' (x.1, a)) ⊆ k
⊢ (-tsupport (α := P × G →L[𝕜] E') fun (a : G) ↦ g' (x.1, a)) ⊆ -k

Tactic:
rw [neg_subset_neg]

Premises used: Set.neg_subset_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}
hK' : IsCompact K'
U : Set G
U_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
K'U : K' ⊆ U
hU : IntegrableOn f U μ
δ : ℝ
δpos : 0 < δ
δε : δ ≤ ε
hδ : K' + ball 0 δ ⊆ U
this : Norm (E →L[𝕜] (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) :=
  hasOpNorm (𝕜 := 𝕜) (𝕜₂ := 𝕜) (E := E) (F := (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (σ₁₂ := RingHom.id 𝕜)
bound : G → ℝ :=
  U.indicator fun (t : G) ↦ norm (E := E →L[𝕜] (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (precompR (P × G) L) * ‖f t‖ * C
a : G
x : P × G
hx : max ‖x.1 - q₀.1‖ ‖x.2 - q₀.2‖ < δ
⊢ (tsupport (α := P × G →L[𝕜] E') fun (a : G) ↦ g' (x.1, a)) ⊆ k

Tactic:
closure_minimal (support_subset_iff'.2 fun z hz => ?_) hk.isClosed

Premises used: Iff.mpr, closure_minimal, tsupport, Function.support_subset_iff', IsCompact.isClosed
-- 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 μ
δ : ℝ
δpos : 0 < δ
δε : δ ≤ ε
hδ : K' + ball 0 δ ⊆ U
this : Norm (E →L[𝕜] (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) :=
  hasOpNorm (𝕜 := 𝕜) (𝕜₂ := 𝕜) (E := E) (F := (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (σ₁₂ := RingHom.id 𝕜)
bound : G → ℝ :=
  U.indicator fun (t : G) ↦ norm (E := E →L[𝕜] (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (precompR (P × G) L) * ‖f t‖ * C
a : G
x : P × G
hx : max ‖x.1 - q₀.1‖ ‖x.2 - q₀.2‖ < δ
a₁ : ∀ (z : G) (hz : z ∉ k), g' (x.1, z) = 0
⊢ (tsupport (α := P × G →L[𝕜] E') fun (a : G) ↦ g' (x.1, a)) ⊆ k

Tactic:
refine closure_minimal (support_subset_iff'.2 fun z hz => ?_) hk.isClosed

Premises used: Iff.mpr, closure_minimal, Function.support_subset_iff', IsCompact.isClosed
-- 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 μ
δ : ℝ
δpos : 0 < δ
δε : δ ≤ ε
hδ : K' + ball 0 δ ⊆ U
this : Norm (E →L[𝕜] (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) :=
  hasOpNorm (𝕜 := 𝕜) (𝕜₂ := 𝕜) (E := E) (F := (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (σ₁₂ := RingHom.id 𝕜)
bound : G → ℝ :=
  U.indicator fun (t : G) ↦ norm (E := E →L[𝕜] (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (precompR (P × G) L) * ‖f t‖ * C
a : G
x : P × G
hx : max ‖x.1 - q₀.1‖ ‖x.2 - q₀.2‖ < δ
z : G
hz : z ∉ k
apply : x.1 ∈ ball q₀.1 ε
⊢ g' (x.1, z) = 0

Tactic:
apply g'_zero x.1 z (h₀ε _) hz

Premises used: Prod.fst
-- 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 μ
δ : ℝ
δpos : 0 < δ
δε : δ ≤ ε
hδ : K' + ball 0 δ ⊆ U
this : Norm (E →L[𝕜] (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) :=
  hasOpNorm (𝕜 := 𝕜) (𝕜₂ := 𝕜) (E := E) (F := (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (σ₁₂ := RingHom.id 𝕜)
bound : G → ℝ :=
  U.indicator fun (t : G) ↦ norm (E := E →L[𝕜] (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (precompR (P × G) L) * ‖f t‖ * C
a : G
x : P × G
hx : max ‖x.1 - q₀.1‖ ‖x.2 - q₀.2‖ < δ
z : G
hz : z ∉ k
rw : ‖x.1 - q₀.1‖ < ε
⊢ x.1 ∈ ball q₀.1 ε

Tactic:
rw [mem_ball_iff_norm]

Premises used: mem_ball_iff_norm
-- 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 μ
δ : ℝ
δpos : 0 < δ
δε : δ ≤ ε
hδ : K' + ball 0 δ ⊆ U
this : Norm (E →L[𝕜] (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) :=
  hasOpNorm (𝕜 := 𝕜) (𝕜₂ := 𝕜) (E := E) (F := (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (σ₁₂ := RingHom.id 𝕜)
bound : G → ℝ :=
  U.indicator fun (t : G) ↦ norm (E := E →L[𝕜] (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (precompR (P × G) L) * ‖f t‖ * C
a : G
x : P × G
hx : max ‖x.1 - q₀.1‖ ‖x.2 - q₀.2‖ < δ
z : G
hz : z ∉ k
⊢ ‖x.1 - q₀.1‖ < ε

Tactic:
((le_max_left _ _).trans_lt hx).trans_le δε

Premises used: LT.lt.trans_le, le_max_left, LE.le.trans_lt