awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Convolution (hypothesis)
Goal:
𝕜 : Type u𝕜
E : Type uE
inst : NormedAddCommGroup E
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
G P : Type uP
inst_3 : MeasurableSpace G
μ : Measure G
inst_4 : NormedAddCommGroup G
inst_5 : BorelSpace G
inst_6 : NormedSpace 𝕜 G
inst_7 : NormedAddCommGroup P
inst_8 : NormedSpace 𝕜 P
f : G → E
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hf : LocallyIntegrable f μ
n : ℕ
ih :
  ∀ {E' F : Type uP} [inst_14 : NormedAddCommGroup E'] [inst_15 : NormedAddCommGroup F] [inst_16 : NormedSpace 𝕜 E']
    [inst_17 : NormedSpace ℝ F] [inst_18 : NormedSpace 𝕜 F]
    (L : ContinuousLinearMap.{u𝕜, u𝕜, uE, uP} (RingHom.id 𝕜) E (E' →L[𝕜] F)) {g : P → G → E'}
    (hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0)
    (hg : ContDiffOn 𝕜 (↑(↑n : ℕ∞) : WithTop ℕ∞) (↿g) (SProd.sprod (β := Set G) s univ)),
    ContDiffOn 𝕜 (F := F) (↑(↑n : ℕ∞) : WithTop ℕ∞)
      (fun (q : P × G) ↦ convolution.{u𝕜, uP, uE, uP, uP} (𝕜 := 𝕜) f (g q.1) L μ q.2) (SProd.sprod (β := Set G) s univ)
E' F : Type uP
inst_9 : NormedAddCommGroup E'
inst_10 : NormedAddCommGroup F
inst_11 : NormedSpace 𝕜 E'
inst_12 : NormedSpace ℝ F
inst_13 : NormedSpace 𝕜 F
L : ContinuousLinearMap.{u𝕜, u𝕜, uE, uP} (RingHom.id 𝕜) E (E' →L[𝕜] F)
g : P → G → E'
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hg :
  DifferentiableOn 𝕜 (↿g) (SProd.sprod (β := Set G) s univ) ∧
    (Eq (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) ⊤ → AnalyticOn 𝕜 (↿g) (SProd.sprod (β := Set G) s univ)) ∧
      ContDiffOn 𝕜 (F := P × G →L[𝕜] E') (↑n : WithTop ℕ∞) (fderiv 𝕜 ↿g) (SProd.sprod (β := Set G) s univ)
f' : P → G → P × G →L[𝕜] F :=
  fun (p : P) (a : G) ↦
    convolution.{u𝕜, uP, uE, uP, uP} (𝕜 := 𝕜) (E' := P × G →L[𝕜] E') f (fun (x : G) ↦ fderiv 𝕜 (uncurry g) (p, x))
      (precompR (P × G) L) μ a
A :
  ∀ (q₀ : P × G),
    q₀.1 ∈ s →
      HasFDerivAt (fun (q : P × G) ↦ convolution.{u𝕜, uP, uE, uP, uP} (𝕜 := 𝕜) f (g q.1) L μ q.2) (f' q₀.1 q₀.2) q₀
p : P
x : G
hp : p ∈ s
hx : x ∉ k
M2 : kᶜ ∈ 𝓝 x
⊢ uncurry g =ᶠ[𝓝 (p, x)] fun (x : P × G) ↦ 0
have M1 : s ∈ 𝓝 p
Tactic: have M1 : s ∈ 𝓝 p := hs.mem_nhds hp
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Convolution (goal)
Goal:
𝕜 : Type u𝕜
E : Type uE
inst : NormedAddCommGroup E
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
G P : Type uP
inst_3 : MeasurableSpace G
μ : Measure G
inst_4 : NormedAddCommGroup G
inst_5 : BorelSpace G
inst_6 : NormedSpace 𝕜 G
inst_7 : NormedAddCommGroup P
inst_8 : NormedSpace 𝕜 P
f : G → E
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hf : LocallyIntegrable f μ
n : ℕ
ih :
  ∀ {E' F : Type uP} [inst_14 : NormedAddCommGroup E'] [inst_15 : NormedAddCommGroup F] [inst_16 : NormedSpace 𝕜 E']
    [inst_17 : NormedSpace ℝ F] [inst_18 : NormedSpace 𝕜 F]
    (L : ContinuousLinearMap.{u𝕜, u𝕜, uE, uP} (RingHom.id 𝕜) E (E' →L[𝕜] F)) {g : P → G → E'}
    (hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0)
    (hg : ContDiffOn 𝕜 (↑(↑n : ℕ∞) : WithTop ℕ∞) (↿g) (SProd.sprod (β := Set G) s univ)),
    ContDiffOn 𝕜 (F := F) (↑(↑n : ℕ∞) : WithTop ℕ∞)
      (fun (q : P × G) ↦ convolution.{u𝕜, uP, uE, uP, uP} (𝕜 := 𝕜) f (g q.1) L μ q.2) (SProd.sprod (β := Set G) s univ)
E' F : Type uP
inst_9 : NormedAddCommGroup E'
inst_10 : NormedAddCommGroup F
inst_11 : NormedSpace 𝕜 E'
inst_12 : NormedSpace ℝ F
inst_13 : NormedSpace 𝕜 F
L : ContinuousLinearMap.{u𝕜, u𝕜, uE, uP} (RingHom.id 𝕜) E (E' →L[𝕜] F)
g : P → G → E'
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hg :
  DifferentiableOn 𝕜 (↿g) (SProd.sprod (β := Set G) s univ) ∧
    (Eq (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) ⊤ → AnalyticOn 𝕜 (↿g) (SProd.sprod (β := Set G) s univ)) ∧
      ContDiffOn 𝕜 (F := P × G →L[𝕜] E') (↑n : WithTop ℕ∞) (fderiv 𝕜 ↿g) (SProd.sprod (β := Set G) s univ)
f' : P → G → P × G →L[𝕜] F :=
  fun (p : P) (a : G) ↦
    convolution.{u𝕜, uP, uE, uP, uP} (𝕜 := 𝕜) (E' := P × G →L[𝕜] E') f (fun (x : G) ↦ fderiv 𝕜 (uncurry g) (p, x))
      (precompR (P × G) L) μ a
A :
  ∀ (q₀ : P × G),
    q₀.1 ∈ s →
      HasFDerivAt (fun (q : P × G) ↦ convolution.{u𝕜, uP, uE, uP, uP} (𝕜 := 𝕜) f (g q.1) L μ q.2) (f' q₀.1 q₀.2) q₀
p : P
x : G
hp : p ∈ s
hx : x ∉ k
M2 : kᶜ ∈ 𝓝 x
M1 : s ∈ 𝓝 p
⊢ uncurry g =ᶠ[𝓝 (p, x)] fun (x : P × G) ↦ 0
have rw : uncurry g =ᶠ[𝓝 p ×ˢ 𝓝 x] fun (x : P × G) ↦ 0
Tactic: rw [nhds_prod_eq]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Convolution (goal)
Goal:
𝕜 : Type u𝕜
E : Type uE
inst : NormedAddCommGroup E
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
G P : Type uP
inst_3 : MeasurableSpace G
μ : Measure G
inst_4 : NormedAddCommGroup G
inst_5 : BorelSpace G
inst_6 : NormedSpace 𝕜 G
inst_7 : NormedAddCommGroup P
inst_8 : NormedSpace 𝕜 P
f : G → E
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hf : LocallyIntegrable f μ
n : ℕ
ih :
  ∀ {E' F : Type uP} [inst_14 : NormedAddCommGroup E'] [inst_15 : NormedAddCommGroup F] [inst_16 : NormedSpace 𝕜 E']
    [inst_17 : NormedSpace ℝ F] [inst_18 : NormedSpace 𝕜 F]
    (L : ContinuousLinearMap.{u𝕜, u𝕜, uE, uP} (RingHom.id 𝕜) E (E' →L[𝕜] F)) {g : P → G → E'}
    (hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0)
    (hg : ContDiffOn 𝕜 (↑(↑n : ℕ∞) : WithTop ℕ∞) (↿g) (SProd.sprod (β := Set G) s univ)),
    ContDiffOn 𝕜 (F := F) (↑(↑n : ℕ∞) : WithTop ℕ∞)
      (fun (q : P × G) ↦ convolution.{u𝕜, uP, uE, uP, uP} (𝕜 := 𝕜) f (g q.1) L μ q.2) (SProd.sprod (β := Set G) s univ)
E' F : Type uP
inst_9 : NormedAddCommGroup E'
inst_10 : NormedAddCommGroup F
inst_11 : NormedSpace 𝕜 E'
inst_12 : NormedSpace ℝ F
inst_13 : NormedSpace 𝕜 F
L : ContinuousLinearMap.{u𝕜, u𝕜, uE, uP} (RingHom.id 𝕜) E (E' →L[𝕜] F)
g : P → G → E'
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hg :
  DifferentiableOn 𝕜 (↿g) (SProd.sprod (β := Set G) s univ) ∧
    (Eq (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) ⊤ → AnalyticOn 𝕜 (↿g) (SProd.sprod (β := Set G) s univ)) ∧
      ContDiffOn 𝕜 (F := P × G →L[𝕜] E') (↑n : WithTop ℕ∞) (fderiv 𝕜 ↿g) (SProd.sprod (β := Set G) s univ)
f' : P → G → P × G →L[𝕜] F :=
  fun (p : P) (a : G) ↦
    convolution.{u𝕜, uP, uE, uP, uP} (𝕜 := 𝕜) (E' := P × G →L[𝕜] E') f (fun (x : G) ↦ fderiv 𝕜 (uncurry g) (p, x))
      (precompR (P × G) L) μ a
A :
  ∀ (q₀ : P × G),
    q₀.1 ∈ s →
      HasFDerivAt (fun (q : P × G) ↦ convolution.{u𝕜, uP, uE, uP, uP} (𝕜 := 𝕜) f (g q.1) L μ q.2) (f' q₀.1 q₀.2) q₀
p : P
x : G
hp : p ∈ s
hx : x ∉ k
M2 : kᶜ ∈ 𝓝 x
M1 : s ∈ 𝓝 p
⊢ uncurry g =ᶠ[𝓝 p ×ˢ 𝓝 x] fun (x : P × G) ↦ 0
have h : ∀ a ∈ s ×ˢ kᶜ, uncurry g a = 0
Tactic: filter_upwards [prod_mem_prod M1 M2]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Convolution (hypothesis)
Goal:
𝕜 : Type u𝕜
E : Type uE
inst : NormedAddCommGroup E
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
G P : Type uP
inst_3 : MeasurableSpace G
μ : Measure G
inst_4 : NormedAddCommGroup G
inst_5 : BorelSpace G
inst_6 : NormedSpace 𝕜 G
inst_7 : NormedAddCommGroup P
inst_8 : NormedSpace 𝕜 P
f : G → E
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hf : LocallyIntegrable f μ
n : ℕ
ih :
  ∀ {E' F : Type uP} [inst_14 : NormedAddCommGroup E'] [inst_15 : NormedAddCommGroup F] [inst_16 : NormedSpace 𝕜 E']
    [inst_17 : NormedSpace ℝ F] [inst_18 : NormedSpace 𝕜 F]
    (L : ContinuousLinearMap.{u𝕜, u𝕜, uE, uP} (RingHom.id 𝕜) E (E' →L[𝕜] F)) {g : P → G → E'}
    (hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0)
    (hg : ContDiffOn 𝕜 (↑(↑n : ℕ∞) : WithTop ℕ∞) (↿g) (SProd.sprod (β := Set G) s univ)),
    ContDiffOn 𝕜 (F := F) (↑(↑n : ℕ∞) : WithTop ℕ∞)
      (fun (q : P × G) ↦ convolution.{u𝕜, uP, uE, uP, uP} (𝕜 := 𝕜) f (g q.1) L μ q.2) (SProd.sprod (β := Set G) s univ)
E' F : Type uP
inst_9 : NormedAddCommGroup E'
inst_10 : NormedAddCommGroup F
inst_11 : NormedSpace 𝕜 E'
inst_12 : NormedSpace ℝ F
inst_13 : NormedSpace 𝕜 F
L : ContinuousLinearMap.{u𝕜, u𝕜, uE, uP} (RingHom.id 𝕜) E (E' →L[𝕜] F)
g : P → G → E'
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hg :
  DifferentiableOn 𝕜 (↿g) (SProd.sprod (β := Set G) s univ) ∧
    (Eq (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) ⊤ → AnalyticOn 𝕜 (↿g) (SProd.sprod (β := Set G) s univ)) ∧
      ContDiffOn 𝕜 (F := P × G →L[𝕜] E') (↑n : WithTop ℕ∞) (fderiv 𝕜 ↿g) (SProd.sprod (β := Set G) s univ)
f' : P → G → P × G →L[𝕜] F :=
  fun (p : P) (a : G) ↦
    convolution.{u𝕜, uP, uE, uP, uP} (𝕜 := 𝕜) (E' := P × G →L[𝕜] E') f (fun (x : G) ↦ fderiv 𝕜 (uncurry g) (p, x))
      (precompR (P × G) L) μ a
A :
  ∀ (q₀ : P × G),
    q₀.1 ∈ s →
      HasFDerivAt (fun (q : P × G) ↦ convolution.{u𝕜, uP, uE, uP, uP} (𝕜 := 𝕜) f (g q.1) L μ q.2) (f' q₀.1 q₀.2) q₀
⊢ ContDiffOn 𝕜 (↑n : WithTop ℕ∞) (↿f') (SProd.sprod (β := Set G) s univ)
have B : ∀ (p : P) (x : G),
  p ∈ s → x ∉ k → Eq (α := P × G →L[𝕜] E') (fderiv 𝕜 (uncurry g) (p, x) : P × G →L[𝕜] E') (0 : P × G →L[𝕜] E')
Tactic: have B : ∀ (p : P) (x : G), p ∈ s → x ∉ k → fderiv 𝕜 (uncurry g) (p, x) = 0 := by
        intro p x hp hx
        apply (hasFDerivAt_zero_of_eventually_const (0 : E') _).fderiv
        have M2 : kᶜ ∈ 𝓝 x := IsOpen.mem_nhds hk.isClosed.isOpen_compl hx
        have M1 : s ∈ 𝓝 p := hs.mem_nhds hp
        rw [nhds_prod_eq]
        filter_upwards [prod_mem_prod M1 M2]
        rintro ⟨p, y⟩ ⟨hp, hy⟩
        exact hgs p y hp hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Convolution (goal)
Goal:
𝕜 : Type u𝕜
E : Type uE
inst : NormedAddCommGroup E
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
G P : Type uP
inst_3 : MeasurableSpace G
μ : Measure G
inst_4 : NormedAddCommGroup G
inst_5 : BorelSpace G
inst_6 : NormedSpace 𝕜 G
inst_7 : NormedAddCommGroup P
inst_8 : NormedSpace 𝕜 P
f : G → E
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hf : LocallyIntegrable f μ
n : ℕ
ih :
  ∀ {E' F : Type uP} [inst_14 : NormedAddCommGroup E'] [inst_15 : NormedAddCommGroup F] [inst_16 : NormedSpace 𝕜 E']
    [inst_17 : NormedSpace ℝ F] [inst_18 : NormedSpace 𝕜 F]
    (L : ContinuousLinearMap.{u𝕜, u𝕜, uE, uP} (RingHom.id 𝕜) E (E' →L[𝕜] F)) {g : P → G → E'}
    (hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0)
    (hg : ContDiffOn 𝕜 (↑(↑n : ℕ∞) : WithTop ℕ∞) (↿g) (SProd.sprod (β := Set G) s univ)),
    ContDiffOn 𝕜 (F := F) (↑(↑n : ℕ∞) : WithTop ℕ∞)
      (fun (q : P × G) ↦ convolution.{u𝕜, uP, uE, uP, uP} (𝕜 := 𝕜) f (g q.1) L μ q.2) (SProd.sprod (β := Set G) s univ)
E' F : Type uP
inst_9 : NormedAddCommGroup E'
inst_10 : NormedAddCommGroup F
inst_11 : NormedSpace 𝕜 E'
inst_12 : NormedSpace ℝ F
inst_13 : NormedSpace 𝕜 F
L : ContinuousLinearMap.{u𝕜, u𝕜, uE, uP} (RingHom.id 𝕜) E (E' →L[𝕜] F)
g : P → G → E'
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hg :
  DifferentiableOn 𝕜 (↿g) (SProd.sprod (β := Set G) s univ) ∧
    (Eq (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) ⊤ → AnalyticOn 𝕜 (↿g) (SProd.sprod (β := Set G) s univ)) ∧
      ContDiffOn 𝕜 (F := P × G →L[𝕜] E') (↑n : WithTop ℕ∞) (fderiv 𝕜 ↿g) (SProd.sprod (β := Set G) s univ)
f' : P → G → P × G →L[𝕜] F :=
  fun (p : P) (a : G) ↦
    convolution.{u𝕜, uP, uE, uP, uP} (𝕜 := 𝕜) (E' := P × G →L[𝕜] E') f (fun (x : G) ↦ fderiv 𝕜 (uncurry g) (p, x))
      (precompR (P × G) L) μ a
A :
  ∀ (q₀ : P × G),
    q₀.1 ∈ s →
      HasFDerivAt (fun (q : P × G) ↦ convolution.{u𝕜, uP, uE, uP, uP} (𝕜 := 𝕜) f (g q.1) L μ q.2) (f' q₀.1 q₀.2) q₀
B :
  ∀ (p : P) (x : G),
    p ∈ s → x ∉ k → Eq (α := P × G →L[𝕜] E') (fderiv 𝕜 (uncurry g) (p, x) : P × G →L[𝕜] E') (0 : P × G →L[𝕜] E')
⊢ ContDiffOn 𝕜 (↑n : WithTop ℕ∞) (↿f') (SProd.sprod (β := Set G) s univ)
have succ : ContDiffOn 𝕜 (↑(↑n : ℕ∞) : WithTop ℕ∞)
  (HasUncurry.uncurry (α := P → G → P × G →L[𝕜] E') fun (p : P) (x : G) ↦ fderiv 𝕜 (uncurry g) (p, x))
  (SProd.sprod (β := Set G) s univ)
Tactic: apply ih (L.precompR (P × G) :) B
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Convolution (goal)
Goal:
𝕜 : Type u𝕜
E : Type uE
inst : NormedAddCommGroup E
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
G P : Type uP
inst_3 : MeasurableSpace G
μ : Measure G
inst_4 : NormedAddCommGroup G
inst_5 : BorelSpace G
inst_6 : NormedSpace 𝕜 G
inst_7 : NormedAddCommGroup P
inst_8 : NormedSpace 𝕜 P
f : G → E
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hf : LocallyIntegrable f μ
ih :
  ∀ (n : ℕ) {E' F : Type uP} [inst_14 : NormedAddCommGroup E'] [inst_15 : NormedAddCommGroup F]
    [inst_16 : NormedSpace 𝕜 E'] [inst_17 : NormedSpace ℝ F] [inst_18 : NormedSpace 𝕜 F]
    (L : ContinuousLinearMap.{u𝕜, u𝕜, uE, uP} (RingHom.id 𝕜) E (E' →L[𝕜] F)) {g : P → G → E'}
    (hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0)
    (hg : ContDiffOn 𝕜 (↑(↑n : ℕ∞) : WithTop ℕ∞) (↿g) (SProd.sprod (β := Set G) s univ)),
    ContDiffOn 𝕜 (F := F) (↑(↑n : ℕ∞) : WithTop ℕ∞)
      (fun (q : P × G) ↦ convolution.{u𝕜, uP, uE, uP, uP} (𝕜 := 𝕜) f (g q.1) L μ q.2) (SProd.sprod (β := Set G) s univ)
E' F : Type uP
inst_9 : NormedAddCommGroup E'
inst_10 : NormedAddCommGroup F
inst_11 : NormedSpace 𝕜 E'
inst_12 : NormedSpace ℝ F
inst_13 : NormedSpace 𝕜 F
L : ContinuousLinearMap.{u𝕜, u𝕜, uE, uP} (RingHom.id 𝕜) E (E' →L[𝕜] F)
g : P → G → E'
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hg : ContDiffOn 𝕜 (↑⊤ : WithTop ℕ∞) (↿g) (SProd.sprod (β := Set G) s univ)
⊢ ContDiffOn 𝕜 (F := F) (↑⊤ : WithTop ℕ∞)
    (fun (q : P × G) ↦ convolution.{u𝕜, uP, uE, uP, uP} (𝕜 := 𝕜) f (g q.1) L μ q.2) (SProd.sprod (β := Set G) s univ)
have top : ∀ (hg : ∀ (n : ℕ), ContDiffOn 𝕜 (↑n : WithTop ℕ∞) (↿g) (SProd.sprod (β := Set G) s univ)) (n : ℕ),
  ContDiffOn 𝕜 (F := F) (↑n : WithTop ℕ∞)
    (fun (q : P × G) ↦ convolution.{u𝕜, uP, uE, uP, uP} (𝕜 := 𝕜) f (g q.1) L μ q.2) (SProd.sprod (β := Set G) s univ)
Tactic: rw [contDiffOn_infty] at hg ⊢
Cleared hypotheses: hg
-- 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
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
f : G → E
n : ℕ∞
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 𝕜 (↑n : WithTop ℕ∞) (↿g) (SProd.sprod (β := Set G) s univ)
eG : Type (max uG uE' uF uP) := ULift.{max uE' uF uP, uG} G
⊢ ContDiffOn 𝕜 (F := F) (↑n : WithTop ℕ∞)
    (fun (q : P × G) ↦ convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) f (g q.1) L μ q.2) (SProd.sprod (β := Set G) s univ)
have this : let this := borel eG;
BorelSpace eG
Tactic: borelize eG
-- 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
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
f : G → E
n : ℕ∞
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 𝕜 (↑n : WithTop ℕ∞) (↿g) (SProd.sprod (β := Set G) s univ)
eG : Type (max uG uE' uF uP) := ULift.{max uE' uF uP, uG} G
this : MeasurableSpace eG := borel eG
this_1 : BorelSpace eG
eE' : Type (max uE' uG uF uP) := ULift.{max uG uF uP, uE'} E'
eF : Type (max uF uG uE' uP) := ULift.{max uG uE' uP, uF} F
eP : Type (max uP uG uE' uF) := ULift.{max uG uE' uF, uP} P
isoG : eG ≃L[𝕜] G := ContinuousLinearEquiv.ulift
isoE' : eE' ≃L[𝕜] E' := ContinuousLinearEquiv.ulift
isoF : eF ≃L[𝕜] F := ContinuousLinearEquiv.ulift
isoP : eP ≃L[𝕜] P := ContinuousLinearEquiv.ulift
ef : eG → E := f ∘ (⇑isoG : (a : eG) → G)
eμ : Measure eG := Measure.map (⇑isoG.symm : (a : G) → eG) μ
eg : eP → eG → eE' :=
  fun (ep : eP) (ex : eG) ↦ (isoE'.symm : (a : E') → eE') (g ((isoP : (a : eP) → P) ep) ((isoG : (a : eG) → G) ex))
eL : E →L[𝕜] eE' →L[𝕜] eF :=
  ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
    (↑(ContinuousLinearEquiv.symm (isoE'.arrowCongr (𝕜 := 𝕜) (E := eE') (F := E') (G := F) (H := eF) isoF)) :
      (E' →L[𝕜] F) →L[𝕜] eE' →L[𝕜] eF)
    L
R : (q : eP × eG) → eF := fun (q : eP × eG) ↦ convolution (𝕜 := 𝕜) ef (eg q.1) eL eμ q.2
⊢ ContDiffOn 𝕜 (↑n : WithTop ℕ∞) R (SProd.sprod (α := Set eP) (β := Set eG) ((⇑isoP : (a : eP) → P) ⁻¹' s) univ)
have hek : IsCompact (X := eG) ((⇑isoG : (a : eG) → G) ⁻¹' k)
Tactic: have hek : IsCompact (isoG ⁻¹' k) := isoG.toHomeomorph.isClosedEmbedding.isCompact_preimage hk
-- 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
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
f : G → E
n : ℕ∞
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 𝕜 (↑n : WithTop ℕ∞) (↿g) (SProd.sprod (β := Set G) s univ)
eG : Type (max uG uE' uF uP) := ULift.{max uE' uF uP, uG} G
this : MeasurableSpace eG := borel eG
this_1 : BorelSpace eG
eE' : Type (max uE' uG uF uP) := ULift.{max uG uF uP, uE'} E'
eF : Type (max uF uG uE' uP) := ULift.{max uG uE' uP, uF} F
eP : Type (max uP uG uE' uF) := ULift.{max uG uE' uF, uP} P
isoG : eG ≃L[𝕜] G := ContinuousLinearEquiv.ulift
isoE' : eE' ≃L[𝕜] E' := ContinuousLinearEquiv.ulift
isoF : eF ≃L[𝕜] F := ContinuousLinearEquiv.ulift
isoP : eP ≃L[𝕜] P := ContinuousLinearEquiv.ulift
ef : eG → E := f ∘ (⇑isoG : (a : eG) → G)
eμ : Measure eG := Measure.map (⇑isoG.symm : (a : G) → eG) μ
eg : eP → eG → eE' :=
  fun (ep : eP) (ex : eG) ↦ (isoE'.symm : (a : E') → eE') (g ((isoP : (a : eP) → P) ep) ((isoG : (a : eG) → G) ex))
eL : E →L[𝕜] eE' →L[𝕜] eF :=
  ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
    (↑(ContinuousLinearEquiv.symm (isoE'.arrowCongr (𝕜 := 𝕜) (E := eE') (F := E') (G := F) (H := eF) isoF)) :
      (E' →L[𝕜] F) →L[𝕜] eE' →L[𝕜] eF)
    L
R : (q : eP × eG) → eF := fun (q : eP × eG) ↦ convolution (𝕜 := 𝕜) ef (eg q.1) eL eμ q.2
hek : IsCompact (X := eG) ((⇑isoG : (a : eG) → G) ⁻¹' k)
⊢ ContDiffOn 𝕜 (↑n : WithTop ℕ∞) R (SProd.sprod (α := Set eP) (β := Set eG) ((⇑isoP : (a : eP) → P) ⁻¹' s) univ)
have hes : IsOpen[ULift.topologicalSpace] ((⇑isoP : (a : eP) → P) ⁻¹' s)
Tactic: have hes : IsOpen (isoP ⁻¹' s) := isoP.continuous.isOpen_preimage _ hs
-- 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
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
f : G → E
n : ℕ∞
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 𝕜 (↑n : WithTop ℕ∞) (↿g) (SProd.sprod (β := Set G) s univ)
eG : Type (max uG uE' uF uP) := ULift.{max uE' uF uP, uG} G
this : MeasurableSpace eG := borel eG
this_1 : BorelSpace eG
eE' : Type (max uE' uG uF uP) := ULift.{max uG uF uP, uE'} E'
eF : Type (max uF uG uE' uP) := ULift.{max uG uE' uP, uF} F
eP : Type (max uP uG uE' uF) := ULift.{max uG uE' uF, uP} P
isoG : eG ≃L[𝕜] G := ContinuousLinearEquiv.ulift
isoE' : eE' ≃L[𝕜] E' := ContinuousLinearEquiv.ulift
isoF : eF ≃L[𝕜] F := ContinuousLinearEquiv.ulift
isoP : eP ≃L[𝕜] P := ContinuousLinearEquiv.ulift
ef : eG → E := f ∘ (⇑isoG : (a : eG) → G)
eμ : Measure eG := Measure.map (⇑isoG.symm : (a : G) → eG) μ
eg : eP → eG → eE' :=
  fun (ep : eP) (ex : eG) ↦ (isoE'.symm : (a : E') → eE') (g ((isoP : (a : eP) → P) ep) ((isoG : (a : eG) → G) ex))
eL : E →L[𝕜] eE' →L[𝕜] eF :=
  ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
    (↑(ContinuousLinearEquiv.symm (isoE'.arrowCongr (𝕜 := 𝕜) (E := eE') (F := E') (G := F) (H := eF) isoF)) :
      (E' →L[𝕜] F) →L[𝕜] eE' →L[𝕜] eF)
    L
R : (q : eP × eG) → eF := fun (q : eP × eG) ↦ convolution (𝕜 := 𝕜) ef (eg q.1) eL eμ q.2
hek : IsCompact (X := eG) ((⇑isoG : (a : eG) → G) ⁻¹' k)
hes : IsOpen[ULift.topologicalSpace] ((⇑isoP : (a : eP) → P) ⁻¹' s)
⊢ ContDiffOn 𝕜 (↑n : WithTop ℕ∞) R (SProd.sprod (α := Set eP) (β := Set eG) ((⇑isoP : (a : eP) → P) ⁻¹' s) univ)
have refine_1 : ∀ (p : eP) (x : eG),
  Membership.mem (γ := Set eP) ((⇑isoP : (a : eP) → P) ⁻¹' s) p → x ∉ (⇑isoG : (a : eG) → G) ⁻¹' k → eg p x = 0
Tactic: refine contDiffOn_convolution_right_with_param_aux eL hes hek ?_ ?_ ?_
-- 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
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
f : G → E
n : ℕ∞
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 𝕜 (↑n : WithTop ℕ∞) (↿g) (SProd.sprod (β := Set G) s univ)
eG : Type (max uG uE' uF uP) := ULift.{max uE' uF uP, uG} G
this : MeasurableSpace eG := borel eG
this_1 : BorelSpace eG
eE' : Type (max uE' uG uF uP) := ULift.{max uG uF uP, uE'} E'
eF : Type (max uF uG uE' uP) := ULift.{max uG uE' uP, uF} F
eP : Type (max uP uG uE' uF) := ULift.{max uG uE' uF, uP} P
isoG : eG ≃L[𝕜] G := ContinuousLinearEquiv.ulift
isoE' : eE' ≃L[𝕜] E' := ContinuousLinearEquiv.ulift
isoF : eF ≃L[𝕜] F := ContinuousLinearEquiv.ulift
isoP : eP ≃L[𝕜] P := ContinuousLinearEquiv.ulift
ef : eG → E := f ∘ (⇑isoG : (a : eG) → G)
eμ : Measure eG := Measure.map (⇑isoG.symm : (a : G) → eG) μ
eg : eP → eG → eE' :=
  fun (ep : eP) (ex : eG) ↦ (isoE'.symm : (a : E') → eE') (g ((isoP : (a : eP) → P) ep) ((isoG : (a : eG) → G) ex))
eL : E →L[𝕜] eE' →L[𝕜] eF :=
  ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
    (↑(ContinuousLinearEquiv.symm (isoE'.arrowCongr (𝕜 := 𝕜) (E := eE') (F := E') (G := F) (H := eF) isoF)) :
      (E' →L[𝕜] F) →L[𝕜] eE' →L[𝕜] eF)
    L
R : (q : eP × eG) → eF := fun (q : eP × eG) ↦ convolution (𝕜 := 𝕜) ef (eg q.1) eL eμ q.2
hek : IsCompact (X := eG) ((⇑isoG : (a : eG) → G) ⁻¹' k)
hes : IsOpen[ULift.topologicalSpace] ((⇑isoP : (a : eP) → P) ⁻¹' s)
refine_1 :
  ∀ (p : eP) (x : eG),
    Membership.mem (γ := Set eP) ((⇑isoP : (a : eP) → P) ⁻¹' s) p → x ∉ (⇑isoG : (a : eG) → G) ⁻¹' k → eg p x = 0
⊢ ContDiffOn 𝕜 (↑n : WithTop ℕ∞) R (SProd.sprod (α := Set eP) (β := Set eG) ((⇑isoP : (a : eP) → P) ⁻¹' s) univ)
have refine_2 : LocallyIntegrable ef eμ
Tactic: refine contDiffOn_convolution_right_with_param_aux eL hes hek ?_ ?_ ?_