-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
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)
⊢ 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)

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]

Premises used: Nat.succ_eq_add_one, self_le_add_right, Nat.cast_add, ContDiff.of_le, ContinuousMultilinearMap.smul_apply, Function.comp_apply, continuousMultilinearCurryLeftEquiv_symm_apply, Nat.cast_one