-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
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
⊢ 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} (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ :=
              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))
              0)
            ((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)
have succ : Eq.{u_4 + 1} (α := G)
  ((((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 : E) → F →L[𝕜] G)
            (m 0) :
          F →L[𝕜] G) :
        (a : F) → G)
      u :
    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: simp only [ContinuousLinearMap.flip_apply, ContinuousLinearMap.comp_zero, zero_add]