Module: Mathlib.Analysis.Calculus.ContDiff.Convolution

Goal state before:
pp: case succ.refine_1
𝕜 : Type u𝕜
E : Type uE
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : RCLike 𝕜
inst✝¹¹ : NormedSpace 𝕜 E
G P : Type uP
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : BorelSpace G
inst✝⁷ : NormedSpace 𝕜 G
inst✝⁶ : NormedAddCommGroup P
inst✝⁵ : 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 : NormedAddCommGroup E'] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 E']
    [inst_3 : NormedSpace ℝ F] [inst_4 : NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) {g : P → G → E'},
    (∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) →
      ContDiffOn 𝕜 (↑↑n) (↿g) (s ×ˢ univ) → ContDiffOn 𝕜 (↑↑n) (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ)
E' F : Type uP
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hg :
  DifferentiableOn 𝕜 (↿g) (s ×ˢ univ) ∧
    (↑n = ⊤ → AnalyticOn 𝕜 (↿g) (s ×ˢ univ)) ∧ ContDiffOn 𝕜 (↑n) (fderiv 𝕜 ↿g) (s ×ˢ univ)
f' : P → G → P × G →L[𝕜] F := fun p a ↦ (f ⋆[precompR (P × G) L, μ] fun x ↦ fderiv 𝕜 (uncurry g) (p, x)) a
A : ∀ (q₀ : P × G), q₀.1 ∈ s → HasFDerivAt (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (f' q₀.1 q₀.2) q₀
⊢ DifferentiableOn 𝕜 (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ)

pp: case succ.refine_2
𝕜 : Type u𝕜
E : Type uE
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : RCLike 𝕜
inst✝¹¹ : NormedSpace 𝕜 E
G P : Type uP
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : BorelSpace G
inst✝⁷ : NormedSpace 𝕜 G
inst✝⁶ : NormedAddCommGroup P
inst✝⁵ : 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 : NormedAddCommGroup E'] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 E']
    [inst_3 : NormedSpace ℝ F] [inst_4 : NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) {g : P → G → E'},
    (∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) →
      ContDiffOn 𝕜 (↑↑n) (↿g) (s ×ˢ univ) → ContDiffOn 𝕜 (↑↑n) (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ)
E' F : Type uP
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hg :
  DifferentiableOn 𝕜 (↿g) (s ×ˢ univ) ∧
    (↑n = ⊤ → AnalyticOn 𝕜 (↿g) (s ×ˢ univ)) ∧ ContDiffOn 𝕜 (↑n) (fderiv 𝕜 ↿g) (s ×ˢ univ)
f' : P → G → P × G →L[𝕜] F := fun p a ↦ (f ⋆[precompR (P × G) L, μ] fun x ↦ fderiv 𝕜 (uncurry g) (p, x)) a
A : ∀ (q₀ : P × G), q₀.1 ∈ s → HasFDerivAt (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (f' q₀.1 q₀.2) q₀
⊢ ContDiffOn 𝕜 (↑n) (fderiv 𝕜 fun q ↦ (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ)

Tactic:
· rintro ⟨p, x⟩ ⟨hp, -⟩
      exact (A (p, x) hp).differentiableAt.differentiableWithinAt

Goal state after:
case succ.refine_2
𝕜 : Type u𝕜
E : Type uE
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : RCLike 𝕜
inst✝¹¹ : NormedSpace 𝕜 E
G P : Type uP
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : BorelSpace G
inst✝⁷ : NormedSpace 𝕜 G
inst✝⁶ : NormedAddCommGroup P
inst✝⁵ : 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 : NormedAddCommGroup E'] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 E']
    [inst_3 : NormedSpace ℝ F] [inst_4 : NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) {g : P → G → E'},
    (∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) →
      ContDiffOn 𝕜 (↑↑n) (↿g) (s ×ˢ univ) → ContDiffOn 𝕜 (↑↑n) (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ)
E' F : Type uP
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hg :
  DifferentiableOn 𝕜 (↿g) (s ×ˢ univ) ∧
    (↑n = ⊤ → AnalyticOn 𝕜 (↿g) (s ×ˢ univ)) ∧ ContDiffOn 𝕜 (↑n) (fderiv 𝕜 ↿g) (s ×ˢ univ)
f' : P → G → P × G →L[𝕜] F := fun p a ↦ (f ⋆[precompR (P × G) L, μ] fun x ↦ fderiv 𝕜 (uncurry g) (p, x)) a
A : ∀ (q₀ : P × G), q₀.1 ∈ s → HasFDerivAt (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (f' q₀.1 q₀.2) q₀
⊢ ContDiffOn 𝕜 (↑n) (fderiv 𝕜 fun q ↦ (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ)