-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
E : Type uE
inst : NormedAddCommGroup E
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
G E' F P : Type uP
inst_3 : NormedAddCommGroup E'
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
μ : Measure G
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedAddCommGroup P
inst_13 : NormedSpace 𝕜 P
f : G → E
n : ℕ∞
L : ContinuousLinearMap.{u𝕜, u𝕜, uE, uP} (RingHom.id 𝕜) E (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)
zero :
  ∀ {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 𝕜 (↑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)
succ :
  ∀ (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_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.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)
top :
  ∀
    (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_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 𝕜 (↑⊤ : 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)
⊢ 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:
induction n using ENat.nat_induction generalizing g E' F with
  | zero =>
    rw [WithTop.coe_zero, contDiffOn_zero] at hg ⊢
    exact continuousOn_convolution_right_with_param L hk hgs hf hg
  | succ n ih =>
    simp only [Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one, WithTop.coe_add,
      WithTop.coe_natCast, WithTop.coe_one] at hg ⊢
    let f' : P → G → P × G →L[𝕜] F := fun p a =>
      (f ⋆[L.precompR (P × G), μ] fun x : G => fderiv 𝕜 (uncurry g) (p, x)) a
    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
    rw [contDiffOn_succ_iff_fderiv_of_isOpen (hs.prod (@isOpen_univ G _))] at hg ⊢
    refine ⟨?_, by simp, ?_⟩
    · rintro ⟨p, x⟩ ⟨hp, -⟩
      exact (A (p, x) hp).differentiableAt.differentiableWithinAt
    · suffices H : ContDiffOn 𝕜 n ↿f' (s ×ˢ univ) by
        apply H.congr
        rintro ⟨p, x⟩ ⟨hp, -⟩
        exact (A (p, x) hp).fderiv
      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
      apply ih (L.precompR (P × G) :) B
      convert! hg.2.2
  | top ih =>
    rw [contDiffOn_infty] at hg ⊢
    exact fun n ↦ ih n L hgs (hg n)

Premises used: Nat.succ_eq_add_one, contDiffOn_infty, contDiffOn_succ_iff_fderiv_of_isOpen, ContinuousLinearMap.zero, WithTop.coe_zero, contDiffOn_zero, WithTop.coe_one, isOpen_univ, Nat.cast_add, WithTop.coe_natCast, WithTop.coe_add, Nat.cast_one, IsOpen.prod