awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
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)
p : P
x : G
hp : (p, x).1 ∈ s
⊢ fderiv 𝕜 (fun (q : P × G) ↦ convolution.{u𝕜, uP, uE, uP, uP} (𝕜 := 𝕜) f (g q.1) L μ q.2) (p, x) = ↿f' (p, x)

Tactic:
(A (p, x) hp).fderiv

Premises used: setOf, Prod.mk, MeasureTheory.convolution, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
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)
p : P
x : G
hp : (p, x).1 ∈ s
⊢ fderiv 𝕜 (fun (q : P × G) ↦ convolution.{u𝕜, uP, uE, uP, uP} (𝕜 := 𝕜) f (g q.1) L μ q.2) (p, x) = ↿f' (p, x)

Tactic:
exact (A (p, x) hp).fderiv

Premises used: Prod.mk, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
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 : 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)

Tactic:
suffices H : ContDiffOn 𝕜 n ↿f' (s ×ˢ univ) by
        apply H.congr
        rintro ⟨p, x⟩ ⟨hp, -⟩
        exact (A (p, x) hp).fderiv
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
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
apply : uncurry g =ᶠ[𝓝 (p, x)] fun (x : P × G) ↦ 0
⊢ Eq (α := P × G →L[𝕜] E') (fderiv 𝕜 (uncurry g) (p, x) : P × G →L[𝕜] E') (0 : P × G →L[𝕜] E')

Tactic:
apply (hasFDerivAt_zero_of_eventually_const (0 : E') _).fderiv

Premises used: hasFDerivAt_zero_of_eventually_const, HasFDerivAt.fderiv, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
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
⊢ kᶜ ∈ 𝓝 x

Tactic:
have M2 : kᶜ ∈ 𝓝 x := IsOpen.mem_nhds hk.isClosed.isOpen_compl hx
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
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
⊢ s ∈ 𝓝 p

Tactic:
have M1 : s ∈ 𝓝 p := hs.mem_nhds hp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
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
rw : uncurry g =ᶠ[𝓝 p ×ˢ 𝓝 x] fun (x : P × G) ↦ 0
⊢ uncurry g =ᶠ[𝓝 (p, x)] fun (x : P × G) ↦ 0

Tactic:
rw [nhds_prod_eq]

Premises used: nhds_prod_eq
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
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
h : ∀ a ∈ s ×ˢ kᶜ, uncurry g a = 0
⊢ uncurry g =ᶠ[𝓝 p ×ˢ 𝓝 x] fun (x : P × G) ↦ 0

Tactic:
filter_upwards [prod_mem_prod M1 M2]

Premises used: Filter.prod_mem_prod
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
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_1 : P
x : G
hp_1 : p_1 ∈ s
hx : x ∉ k
M2 : kᶜ ∈ 𝓝 x
M1 : s ∈ 𝓝 p_1
p : P
y : G
hp : (p, y).1 ∈ s
hy : (p, y).2 ∈ kᶜ
⊢ uncurry g (p, y) = 0

Tactic:
hgs p y hp hy
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
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_1 : P
x : G
hp_1 : p_1 ∈ s
hx : x ∉ k
M2 : kᶜ ∈ 𝓝 x
M1 : s ∈ 𝓝 p_1
p : P
y : G
hp : (p, y).1 ∈ s
hy : (p, y).2 ∈ kᶜ
⊢ uncurry g (p, y) = 0

Tactic:
exact hgs p y hp hy