-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
inst_6 : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N : WithTop ℕ∞) (f i)
hv : ∀ (k : ℕ), (↑k : ℕ∞) ≤ N → Summable (v k)
h'f :
  ∀ (k : ℕ) (i : α) (x : E),
    (↑k : ℕ∞) ≤ N →
      norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F) (iteratedFDeriv 𝕜 k (f i) x) ≤
        v k i
k : ℕ
IH :
  ∀ (hk : (↑k : ℕ∞) ≤ N),
    Eq (α := E → ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
      (iteratedFDeriv 𝕜 k fun (y : E) ↦ ∑' (n : α), f n y) fun (x : E) ↦ ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x
hk : (↑(k + 1) : ℕ∞) ≤ N
h'k : (↑k : ℕ∞) < N
A :
  Summable (α := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F) fun (n : α) ↦
    iteratedFDeriv 𝕜 k (f n) 0
⊢ Eq (α := E → ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin (k + 1)) ↦ E) F)
    (comp (β := E →L[𝕜] ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
      (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (k + 1)) ↦ E) F) :
            (E →L[𝕜] ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F) ≃ₗᵢ[𝕜]
              ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (x : Fin (k + 1)) ↦ E) F) :
        (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F) →
          ContinuousMultilinearMap 𝕜 (fun (x : Fin (k + 1)) ↦ E) F)
      (fderiv 𝕜 fun (x : E) ↦ ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x))
    fun (x : E) ↦
    ∑' (n : α),
      comp (β := E →L[𝕜] ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
        (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (k + 1)) ↦ E) F) :
              (E →L[𝕜] ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F) ≃ₗᵢ[𝕜]
                ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (x : Fin (k + 1)) ↦ E) F) :
          (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F) →
            ContinuousMultilinearMap 𝕜 (fun (x : Fin (k + 1)) ↦ E) F)
        (fderiv 𝕜 (iteratedFDeriv 𝕜 k (f n))) x
have succ : Eq (α := E → ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin (k + 1)) ↦ E) F)
  (comp (β := E →L[𝕜] ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
    (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (k + 1)) ↦ E) F) :
          (E →L[𝕜] ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F) ≃ₗᵢ[𝕜]
            ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (x : Fin (k + 1)) ↦ E) F) :
      (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F) →
        ContinuousMultilinearMap 𝕜 (fun (x : Fin (k + 1)) ↦ E) F)
    fun (x : E) ↦ ∑' (n : α), fderiv 𝕜 (fun (x : E) ↦ iteratedFDeriv 𝕜 k (f n) x) x)
  fun (x : E) ↦
  ∑' (n : α),
    comp (β := E →L[𝕜] ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
      (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (k + 1)) ↦ E) F) :
            (E →L[𝕜] ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F) ≃ₗᵢ[𝕜]
              ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (x : Fin (k + 1)) ↦ E) F) :
        (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F) →
          ContinuousMultilinearMap 𝕜 (fun (x : Fin (k + 1)) ↦ E) F)
      (fderiv 𝕜 (iteratedFDeriv 𝕜 k (f n))) x
Tactic: rw [fderiv_tsum (hv _ hk) (fun n => (hf n).differentiable_iteratedFDeriv
        (mod_cast h'k)) _ A]