-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
i_1 : ℕ
a : 𝕜
i : ℕ
hi :
  ∀ (hf : ContDiff 𝕜 (↑i : ℕ∞ω) f),
    Eq (α := E → ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDeriv 𝕜 i fun (z : E) ↦ f (a • z)) fun (x : E) ↦
      HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (a ^ i)
        (iteratedFDeriv 𝕜 i f (a • x))
hf : ContDiff 𝕜 (↑(i + 1) : ℕ∞ω) f
v : E
x : (i : Fin (i + 1)) → E
⊢ Eq.{uF + 1} (α := F)
    ((comp (β := E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
            (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (i + 1)) ↦ E) F) :
                  (E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) ≃ₗᵢ[𝕜]
                    ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (x : Fin (i + 1)) ↦ E) F) :
              (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F) →
                ContinuousMultilinearMap 𝕜 (fun (x : Fin (i + 1)) ↦ E) F)
            (fderiv 𝕜 (iteratedFDeriv 𝕜 i fun (z : E) ↦ f (a • z))) v :
          (a : (i : Fin (i + 1)) → E) → F)
        x :
      F)
    ((HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin (i + 1)) ↦ E) F) (a ^ (i + 1))
            (comp (β := E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
              (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (i + 1)) ↦ E) F) :
                    (E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) ≃ₗᵢ[𝕜]
                      ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (x : Fin (i + 1)) ↦ E) F) :
                (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F) →
                  ContinuousMultilinearMap 𝕜 (fun (x : Fin (i + 1)) ↦ E) F)
              (fderiv 𝕜 (iteratedFDeriv 𝕜 i f)) (a • v)) :
          (a : (i : Fin (i + 1)) → E) → F)
        x :
      F)
have succ : (((fderiv 𝕜
              (fun (x : E) ↦
                HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (a ^ i)
                  (iteratedFDeriv 𝕜 i f (a • x)))
              v :
            (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
          (x 0) :
        ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
      (a : (i : Fin i) → E) → F)
    (tail (α := fun (x : Fin (i + 1)) ↦ E) x) =
  HSMul.hSMul (β := F) (a ^ (i + 1))
    ((((fderiv 𝕜 (iteratedFDeriv 𝕜 i f) (a • v) : (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F) (x 0) :
            ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (x : Fin (i + 1)) ↦ E) x) :
      F)
Tactic: simp only [Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one, self_le_add_right, hf.of_le, hi,
      comp_apply, continuousMultilinearCurryLeftEquiv_symm_apply,
      ContinuousMultilinearMap.smul_apply]