no goals
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ HasFTaylorSeriesUpTo (↑(n + 1)) f p ↔
    (∀ (x : E), ContinuousMultilinearMap.uncurry0 (p x 0) = f x) ∧
      (∀ (x : E), HasFDerivAt (fun y => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) x) ∧
        HasFTaylorSeriesUpTo (↑n) (fun x => ↑(continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) fun x =>
          FormalMultilinearSeries.shift (p x)
simp only [hasFTaylorSeriesUpToOn_succ_iff_right, ← hasFTaylorSeriesUpToOn_univ_iff, mem_univ,
  forall_true_left, hasFDerivWithinAt_univ]