-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ x ∈ s, ContinuousMultilinearMap.curry0 (p x 0) = f x
Hfderiv_zero :
  ∀ x ∈ s,
    HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (fun (y : E) ↦ p y 0)
      (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin 1) ↦ E) (p x 1)) s x
Htaylor :
  HasFTaylorSeriesUpToOn (𝕜 := 𝕜) (F := E →L[𝕜] F) (↑n : ℕ∞ω)
    (fun (x : E) ↦
      (continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
        (p x 1))
    (fun (x : E) ↦ (p x).shift) s
x : E
hx : x ∈ s
m : ℕ
hm : LT.lt (α := ℕ∞ω) (↑(m + 1) : ℕ∞ω) (↑n.succ : ℕ∞ω)
A : LT.lt (α := ℕ∞ω) (↑m : ℕ∞ω) (↑n : ℕ∞ω)
this :
  HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m.succ) ↦ E) F)
    (fun (x : E) ↦ p x m.succ)
    (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜)
      (↑(↑(LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 m E F)) :
            ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (E →L[𝕜] F) ≃L[𝕜]
              ContinuousMultilinearMap 𝕜 (fun (i : Fin m.succ) ↦ E) F) :
        ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (E →L[𝕜] F) →L[𝕜]
          ContinuousMultilinearMap 𝕜 (fun (i : Fin m.succ) ↦ E) F)
      (ContinuousMultilinearMap.curryLeft (𝕜 := 𝕜) (Ei := fun (i : Fin m.succ) ↦ E) (G := E →L[𝕜] F)
        ((p x).shift m.succ)))
    s x
e_8 :
  Eq (α := AddCommGroup (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (m + 1)) ↦ E) F))
    (ContinuousMultilinearMap.instAddCommGroup (M₁ := fun (i : Fin (m + 1)) ↦ E)) NormedAddCommGroup.toAddCommGroup
e_9 :
  HEq (α := Module 𝕜 (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (m + 1)) ↦ E) F))
    (ContinuousMultilinearMap.instModule (M₁ := fun (i : Fin (m + 1)) ↦ E)) (β :=
    Module 𝕜 (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (m + 1)) ↦ E) F)) NormedSpace.toModule
e_10 :
  Eq (α := TopologicalSpace (ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (m + 1)) ↦ E) F))
    (ContinuousMultilinearMap.instTopologicalSpace (E := fun (i : Fin (m + 1)) ↦ E)) UniformSpace.toTopologicalSpace
y : E
v : (i : Fin (m + 1)) → E
h :
  Eq.{uF + 1} (α := F)
    ((p x m.succ.succ : (a : (i : Fin m.succ.succ) → E) → F) (cons (α := fun (i : Fin m.succ.succ) ↦ E) y v) : F)
    ((p x m.succ.succ : (a : (i : Fin m.succ.succ) → E) → F)
        (cons (α := fun (x : Fin (m.succ + 1)) ↦ E) y
          (snoc (α := fun (i : Fin m.succ) ↦ (fun (x : Fin (m.succ + 1)) ↦ E) i.succ)
            (init (α := fun (i : Fin (m + 1)) ↦ E) v) (v (last m)))) :
      F)
h₁ h₂ :
  Eq.{uF + 1} (α := F)
    ((p x m.succ.succ : (a : (i : Fin m.succ.succ) → E) → F) (cons (α := fun (i : Fin m.succ.succ) ↦ E) y v) : F)
    ((p x m.succ.succ : (a : (i : Fin m.succ.succ) → E) → F) (cons (α := fun (x : Fin (m.succ + 1)) ↦ E) y v) : F)
⊢ Eq.{uF + 1} (α := F)
    ((p x m.succ.succ : (a : (i : Fin m.succ.succ) → E) → F) (cons (α := fun (i : Fin m.succ.succ) ↦ E) y v) : F)
    ((p x m.succ.succ : (a : (i : Fin m.succ.succ) → E) → F)
        (snoc (α := fun (i : Fin m.succ.succ) ↦ E)
          (cons (α := fun (i : Fin (m + 1)) ↦ E) y (init (α := fun (i : Fin (m + 1)) ↦ E) v)) (v (last m))) :
      F)

Tactic:
rw [← cons_snoc_eq_snoc_cons, snoc_init_self]

Premises used: Fin.cons_snoc_eq_snoc_cons, Fin.snoc_init_self