-- 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
h :
  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 →
    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 →
      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 →
        ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin (m + 1).succ) ↦ E) (p x (m + 1).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))
⊢ HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (m + 1)) ↦ E) F)
    (fun (x : E) ↦ p x (m + 1))
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin (m + 1).succ) ↦ E) (p x (m + 1).succ)) s x

Tactic:
convert! this