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
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
I4 :
  ∀ᵐ (a : G) ∂μ,
    ∀ (x : P × G),
      dist x q₀ < δ →
        norm (E := P × G →L[𝕜] F)
            ((((precompR (P × G) L : (a : E) → (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (f a) :
                    (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) :
                  (a : P × G →L[𝕜] E') → P × G →L[𝕜] F)
                (g' (x.1, x.2 - a)) :
              P × G →L[𝕜] F) ≤
          bound a
I5 : Integrable bound μ
a : G
x : P × G
hx : dist x q₀ < δ
N : SProd.sprod (β := Set G) s univ ∈ 𝓝 (x.1, x.2 - a)
Z : HasFDerivAt (↿g) (fderiv 𝕜 ↿g (x.1, x.2 - a)) (x.1, x.2 - a)
⊢ (fun (x : P × G) ↦ (x.1, x.2 - a)) = HSub.hSub (α := (a : P × G) → P × G) id fun (x : P × G) ↦ (0, a)
have h : ∀ (x : P × G),
  (x.1, x.2 - a).1 = (HSub.hSub (α := (a : P × G) → P × G) (β := (x : P × G) → P × G) id (fun (x : P × G) ↦ (0, a)) x).1
Tactic: ext x
-- 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 μ
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 𝕜 (↑0 : WithTop ℕ∞) (↿g) (SProd.sprod (β := Set G) s univ)
⊢ ContDiffOn 𝕜 (F := F) (↑0 : 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 zero : ∀ (hg : ContinuousOn (↿g) (SProd.sprod (β := Set G) s univ)),
  ContinuousOn (Y := F) (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 [WithTop.coe_zero, contDiffOn_zero] at hg ⊢
Cleared hypotheses: hg
-- 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 : ContDiffOn 𝕜 (↑(↑n.succ : ℕ∞) : WithTop ℕ∞) (↿g) (SProd.sprod (β := Set G) s univ)
⊢ ContDiffOn 𝕜 (F := F) (↑(↑n.succ : ℕ∞) : 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 hg₁ : ContDiffOn 𝕜 (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) (↿g) (SProd.sprod (β := Set G) s univ)
Tactic: simp only [Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one, WithTop.coe_add,
      WithTop.coe_natCast, WithTop.coe_one] at hg ⊢
Cleared hypotheses: hg
-- 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 : ContDiffOn 𝕜 (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) (↿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
⊢ ContDiffOn 𝕜 (F := F) (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1)
    (fun (q : P × G) ↦ convolution.{u𝕜, uP, uE, uP, uP} (𝕜 := 𝕜) f (g q.1) L μ q.2) (SProd.sprod (β := Set G) s univ)
have 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₀
Tactic: have A : ∀ q₀ : P × G, q₀.1 ∈ s →
        HasFDerivAt (fun q : P × G => (f ⋆[L, μ] g q.1) q.2) (f' q₀.1 q₀.2) q₀ :=
      hasFDerivAt_convolution_right_with_param L hs hk hgs hf hg.one_of_succ
-- 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₀
⊢ DifferentiableOn 𝕜 (F := F) (fun (q : P × G) ↦ convolution.{u𝕜, uP, uE, uP, uP} (𝕜 := 𝕜) f (g q.1) L μ q.2)
      (SProd.sprod (β := Set G) s univ) ∧
    (Eq (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) ⊤ →
        AnalyticOn 𝕜 (F := F) (fun (q : P × G) ↦ convolution.{u𝕜, uP, uE, uP, uP} (𝕜 := 𝕜) f (g q.1) L μ q.2)
          (SProd.sprod (β := Set G) s univ)) ∧
      ContDiffOn 𝕜 (F := P × G →L[𝕜] F) (↑n : WithTop ℕ∞)
        (fderiv 𝕜 fun (q : P × G) ↦ convolution.{u𝕜, uP, uE, uP, uP} (𝕜 := 𝕜) f (g q.1) L μ q.2)
        (SProd.sprod (β := Set G) s univ)
have succ : DifferentiableOn 𝕜 (F := F) (fun (q : P × G) ↦ convolution.{u𝕜, uP, uE, uP, uP} (𝕜 := 𝕜) f (g q.1) L μ q.2)
  (SProd.sprod (β := Set G) s univ)
Tactic: refine ⟨?_, by simp, ?_⟩
-- 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₀
succ :
  DifferentiableOn 𝕜 (F := F) (fun (q : P × G) ↦ convolution.{u𝕜, uP, uE, uP, uP} (𝕜 := 𝕜) f (g q.1) L μ q.2)
    (SProd.sprod (β := Set G) s univ)
⊢ DifferentiableOn 𝕜 (F := F) (fun (q : P × G) ↦ convolution.{u𝕜, uP, uE, uP, uP} (𝕜 := 𝕜) f (g q.1) L μ q.2)
      (SProd.sprod (β := Set G) s univ) ∧
    (Eq (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) ⊤ →
        AnalyticOn 𝕜 (F := F) (fun (q : P × G) ↦ convolution.{u𝕜, uP, uE, uP, uP} (𝕜 := 𝕜) f (g q.1) L μ q.2)
          (SProd.sprod (β := Set G) s univ)) ∧
      ContDiffOn 𝕜 (F := P × G →L[𝕜] F) (↑n : WithTop ℕ∞)
        (fderiv 𝕜 fun (q : P × G) ↦ convolution.{u𝕜, uP, uE, uP, uP} (𝕜 := 𝕜) f (g q.1) L μ q.2)
        (SProd.sprod (β := Set G) s univ)
have succ₁ : ContDiffOn 𝕜 (F := P × G →L[𝕜] F) (↑n : WithTop ℕ∞)
  (fderiv 𝕜 fun (q : P × G) ↦ convolution.{u𝕜, uP, uE, uP, uP} (𝕜 := 𝕜) f (g q.1) L μ q.2)
  (SProd.sprod (β := Set G) s univ)
Tactic: refine ⟨?_, by simp, ?_⟩
-- 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₀
H : ContDiffOn 𝕜 (↑n : WithTop ℕ∞) (↿f') (SProd.sprod (β := Set G) s univ)
⊢ ContDiffOn 𝕜 (F := P × G →L[𝕜] F) (↑n : WithTop ℕ∞)
    (fderiv 𝕜 fun (q : P × G) ↦ convolution.{u𝕜, uP, uE, uP, uP} (𝕜 := 𝕜) f (g q.1) L μ q.2)
    (SProd.sprod (β := Set G) s univ)
have apply : ∀ x ∈ SProd.sprod (β := Set G) s univ,
  fderiv 𝕜 (fun (q : P × G) ↦ convolution.{u𝕜, uP, uE, uP, uP} (𝕜 := 𝕜) f (g q.1) L μ q.2) x = ↿f' x
Tactic: apply H.congr
-- 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₀
⊢ ContDiffOn 𝕜 (F := P × G →L[𝕜] F) (↑n : WithTop ℕ∞)
    (fderiv 𝕜 fun (q : P × G) ↦ convolution.{u𝕜, uP, uE, uP, uP} (𝕜 := 𝕜) f (g q.1) L μ q.2)
    (SProd.sprod (β := Set G) s univ)
have succ : ContDiffOn 𝕜 (↑n : WithTop ℕ∞) (↿f') (SProd.sprod (β := Set G) s univ)
Tactic: suffices H : ContDiffOn 𝕜 n ↿f' (s ×ˢ univ) by
        apply H.congr
        rintro ⟨p, x⟩ ⟨hp, -⟩
        exact (A (p, x) hp).fderiv
-- 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
⊢ Eq (α := P × G →L[𝕜] E') (fderiv 𝕜 (uncurry g) (p, x) : P × G →L[𝕜] E') (0 : P × G →L[𝕜] E')
have apply : uncurry g =ᶠ[𝓝 (p, x)] fun (x : P × G) ↦ 0
Tactic: apply (hasFDerivAt_zero_of_eventually_const (0 : E') _).fderiv
-- 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
⊢ uncurry g =ᶠ[𝓝 (p, x)] fun (x : P × G) ↦ 0
have M2 : kᶜ ∈ 𝓝 x
Tactic: have M2 : kᶜ ∈ 𝓝 x := IsOpen.mem_nhds hk.isClosed.isOpen_compl hx