awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Convolution (goal)
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
p : P
x : G
hp : (p, x).1 ∈ s
⊢ HasCompactSupport (g (p, x).1)
have h : tsupport (g (p, x).1) ⊆ k
Tactic: apply hk.of_isClosed_subset (isClosed_tsupport _)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Convolution (hypothesis)
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
⊢ 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₀
have 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))) μ
Tactic: have I1 :
    ∀ᶠ x : P × G in 𝓝 q₀, AEStronglyMeasurable (fun a : G => L (f a) (g x.1 (x.2 - a))) μ := by
    filter_upwards [A' q₀ hq₀]
    rintro ⟨p, x⟩ ⟨hp, -⟩
    refine (HasCompactSupport.convolutionExists_right L ?_ hf (A _ hp) _).1
    apply hk.of_isClosed_subset (isClosed_tsupport _)
    exact closure_minimal (support_subset_iff'.2 fun z hz => hgs _ _ hp hz) hk.isClosed
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Convolution (hypothesis)
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))) μ
⊢ 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))) μ
have M : HasCompactSupport (g q₀.1)
Tactic: have M : HasCompactSupport (g q₀.1) := HasCompactSupport.intro hk fun x hx => hgs q₀.1 x hq₀ hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Convolution (hypothesis)
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))) μ
⊢ 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₀
have 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))) μ
Tactic: have I2 : Integrable (fun a : G => L (f a) (g q₀.1 (q₀.2 - a))) μ := by
    have M : HasCompactSupport (g q₀.1) := HasCompactSupport.intro hk fun x hx => hgs q₀.1 x hq₀ hx
    apply M.convolutionExists_right L hf (A q₀.1 hq₀) q₀.2
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Convolution (hypothesis)
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)))
    μ
have T : 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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Convolution (goal)
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)
⊢ 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)))
    μ
have apply : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (y : G) ↦ g' (q₀.1, y)
Tactic: apply (HasCompactSupport.convolutionExists_right (L.precompR (P × G) :) T hf _ q₀.2).1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Convolution (hypothesis)
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)
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (y : G) ↦ g' (q₀.1, y)
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Convolution (goal)
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)
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (y : G) ↦ g' (q₀.1, y)
have apply : ∀ (x : G), (q₀.1, x) ∈ SProd.sprod (β := Set G) s univ
Tactic: apply this.comp_continuous (.prodMk_right _)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Convolution (hypothesis)
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))) μ
⊢ 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₀
have 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)))
  μ
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₀
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Convolution (hypothesis)
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)))
    μ
⊢ 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₀
have K'_def : let K' := -k + {q₀.2};
K' = -k + {q₀.2}
Tactic: set K' := (-k + {q₀.2} : Set G) with K'_def
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Convolution (hypothesis)
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}
⊢ 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₀
have hK' : IsCompact K'
Tactic: have hK' : IsCompact K' := hk.neg.add isCompact_singleton