-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinOnBall f p s x r
f' : E →L[𝕜] F
y : E
hy : (↑‖y‖₊ : ℝ≥0∞) < r
h'y : x + y ∈ insert x s
hf' : HasFDerivWithinAt f f' (insert x s) (x + y)
hu : UniqueDiffOn 𝕜 (insert x s)
F' : Type v := UniformSpace.Completion F
a : F →L[𝕜] F' := UniformSpace.Completion.toComplL
b : (E →L[𝕜] F) →ₗᵢ[𝕜] E →L[𝕜] F' := LinearIsometry.postcomp UniformSpace.Completion.toComplₗᵢ
this_1 :
  HasFPowerSeriesWithinOnBall.{u_1, u, v} (𝕜 := 𝕜) (F := F') ((⇑a : (a : F) → F') ∘ f) (a.compFormalMultilinearSeries p)
    s x r
Z :
  HasSum
    (fun (n : ℕ) ↦
      (FormalMultilinearSeries.derivSeries (a.compFormalMultilinearSeries p) n : (a : (i : Fin n) → E) → E →L[𝕜] F')
        fun (x : Fin n) ↦ y)
    (a ∘SL f')
this : fderivWithin 𝕜 ((⇑a : (a : F) → F') ∘ f) (insert x s) (x + y) = a ∘SL f'
n : ℕ
v : E
h₁ :
  Eq.{v + 1} (α := F')
    (∑ c : { s : Finset (Fin (1 + n)) // s.card = n },
      ((b : (a : E →L[𝕜] F) → E →L[𝕜] F')
            ((continuousMultilinearCurryFin1 𝕜 E F :
                (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
              ((p.changeOriginSeriesTerm 1 n (↑c : Finset (Fin (1 + n))) ⋯ :
                  (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
                fun (x : Fin n) ↦ y)) :
          (a : E) → F')
        v)
    (∑ c : { s : Finset (Fin (1 + n)) // s.card = n },
      ((continuousMultilinearCurryFin1 𝕜 E F' : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F') → E →L[𝕜] F')
            ((FormalMultilinearSeries.changeOriginSeriesTerm (a.compFormalMultilinearSeries p) 1 n
                  (↑c : Finset (Fin (1 + n))) ⋯ :
                (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F')
              fun (x : Fin n) ↦ y) :
          (a : E) → F')
        v)
⊢ Eq.{v + 1} (α := F')
    (((Function.comp (β := E →L[𝕜] F) (⇑b : (a : E →L[𝕜] F) → E →L[𝕜] F')
              (fun (n : ℕ) ↦ (p.derivSeries n : (a : (i : Fin n) → E) → E →L[𝕜] F) fun (x : Fin n) ↦ y) n :
            E →L[𝕜] F') :
          (a : E) → F')
        v :
      F')
    (((FormalMultilinearSeries.derivSeries (a.compFormalMultilinearSeries p) n : (a : (i : Fin n) → E) → E →L[𝕜] F')
            fun (x : Fin n) ↦ y :
          (a : E) → F')
        v :
      F')

Tactic:
simp only [FormalMultilinearSeries.derivSeries, ContinuousLinearMap.coe_sum', Finset.sum_apply,
    ContinuousLinearMap.compFormalMultilinearSeries_apply,
    FormalMultilinearSeries.changeOriginSeries,
    ContinuousLinearMap.compContinuousMultilinearMap_coe, ContinuousLinearEquiv.coe_coe,
    LinearIsometryEquiv.coe_coe, Function.comp_apply, ContinuousMultilinearMap.sum_apply, map_sum]

Premises used: FormalMultilinearSeries.derivSeries, Finset.sum_apply, FormalMultilinearSeries.changeOriginSeries, ContinuousMultilinearMap.sum_apply, ContinuousLinearMap.compFormalMultilinearSeries_apply, LinearIsometryEquiv.coe_coe, map_sum, ContinuousLinearMap.compContinuousMultilinearMap_coe, ContinuousLinearMap.coe_sum', Function.comp_apply, ContinuousLinearEquiv.coe_coe