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

Tactic:
ext y v