-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
u : F
i : ℕ
ih :
  ∀ (hi : (↑i : ℕ∞ω) ≤ n) {x : E} (hx : x ∈ s) {m : Fin i → E},
    Eq.{u_4 + 1} (α := G)
      ((iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s x : (a : (i : Fin i) → E) → G) m : G)
      ((((iteratedFDerivWithin 𝕜 i c s x : (a : (i : Fin i) → E) → F →L[𝕜] G) m : F →L[𝕜] G) : (a : F) → G) u : G)
x : E
hx : x ∈ s
m : Fin (i + 1) → E
hi : (↑i : ℕ∞ω) < n
h_deriv_apply :
  DifferentiableOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s) s
h_deriv :
  DifferentiableOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G)) (iteratedFDerivWithin 𝕜 i c s)
    s
succ :
  Eq.{u_4 + 1} (α := G)
    ((HAdd.hAdd (α := E →L[𝕜] G) (β := E →L[𝕜] G)
            (ContinuousLinearMap.comp.{u_1, u_1, u_1, u_2, u_3, u_4} (σ₂₃ := RingHom.id 𝕜) (M₂ := F)
              ((iteratedFDerivWithin 𝕜 i c s x : (a : (i : Fin i) → E) → F →L[𝕜] G)
                (Fin.tail (α := fun (i : Fin (i + 1)) ↦ E) m))
              (fderivWithin 𝕜 (fun (x : E) ↦ u) s x))
            ((ContinuousLinearMap.flip
                    (fderivWithin 𝕜
                      (fun (y : E) ↦
                        (iteratedFDerivWithin 𝕜 i c s y : (a : (i : Fin i) → E) → F →L[𝕜] G)
                          (Fin.tail (α := fun (i : Fin (i + 1)) ↦ E) m))
                      s x) :
                  (a : F) → E →L[𝕜] G)
                u :
              E →L[𝕜] G) :
          (a : E) → G)
        (m 0) :
      G)
    ((((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i c s) s x :
                      (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G))
                    (m 0) :
                  ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G)) :
                (a : (i : Fin i) → E) → F →L[𝕜] G)
              (Fin.tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
            F →L[𝕜] G) :
          (a : F) → G)
        u :
      G)
⊢ Eq.{u_4 + 1} (α := G)
    ((fderivWithin 𝕜
            (fun (x : E) ↦
              (((iteratedFDerivWithin 𝕜 i c s x : (a : (i : Fin i) → E) → F →L[𝕜] G)
                      (Fin.tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
                    F →L[𝕜] G) :
                  (a : F) → G)
                u)
            s x :
          (a : E) → G)
        (m 0) :
      G)
    ((((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i c s) s x :
                      (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G))
                    (m 0) :
                  ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G)) :
                (a : (i : Fin i) → E) → F →L[𝕜] G)
              (Fin.tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
            F →L[𝕜] G) :
          (a : F) → G)
        u :
      G)

Tactic:
rw [fderivWithin_clm_apply (hs x hx) (h_deriv.continuousMultilinear_apply_const _ x hx)
      (differentiableWithinAt_const u)]

Premises used: DifferentiableOn.continuousMultilinear_apply_const, differentiableWithinAt_const, fderivWithin_clm_apply