-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem hasFTaylorSeriesUpToOn_succ_nat_iff_right {n : ℕ} :
    HasFTaylorSeriesUpToOn (n + 1 : ℕ) f p s ↔
      (∀ x ∈ s, (p x 0).curry0 = f x) ∧
        (∀ x ∈ s, HasFDerivWithinAt (fun y => p y 0) (p x 1).curryLeft s x) ∧
          HasFTaylorSeriesUpToOn n (fun x => continuousMultilinearCurryFin1 𝕜 E F (p x 1))
            (fun x => (p x).shift) s

Proof state:
case h.e'_12.h.h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ x ∈ s, (p x 0).curry0 = f x
Hfderiv_zero : ∀ x ∈ s, HasFDerivWithinAt (fun y => p y 0) (p x 1).curryLeft s x
Htaylor : HasFTaylorSeriesUpToOn (↑n) (fun x => (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x => (p x).shift) s
x : E
hx : x ∈ s
m : ℕ
hm : ↑(m + 1) < ↑n.succ
A : ↑m < ↑n
this :
  HasFDerivWithinAt (fun x => p x m.succ)
    ((↑{ toLinearEquiv := (continuousMultilinearCurryRightEquiv' 𝕜 m E F).symm.toLinearEquiv, continuous_toFun := ⋯,
            continuous_invFun := ⋯ }).comp
      ((p x).shift m.succ).curryLeft)
    s x
e_8✝ : ContinuousMultilinearMap.instAddCommGroup = SeminormedAddCommGroup.toAddCommGroup
he✝ : ContinuousMultilinearMap.instModule = NormedSpace.toModule
e_10✝ : ContinuousMultilinearMap.instTopologicalSpace = UniformSpace.toTopologicalSpace
⊢ (p x (m + 1).succ).curryLeft =
    (↑{ toLinearEquiv := (continuousMultilinearCurryRightEquiv' 𝕜 m E F).symm.toLinearEquiv, continuous_toFun := ⋯,
            continuous_invFun := ⋯ }).comp
      ((p x).shift m.succ).curryLeft

Tactic:
ext y v

Result:
case h.e'_12.h.h.h.H
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ x ∈ s, (p x 0).curry0 = f x
Hfderiv_zero : ∀ x ∈ s, HasFDerivWithinAt (fun y => p y 0) (p x 1).curryLeft s x
Htaylor : HasFTaylorSeriesUpToOn (↑n) (fun x => (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x => (p x).shift) s
x : E
hx : x ∈ s
m : ℕ
hm : ↑(m + 1) < ↑n.succ
A : ↑m < ↑n
this :
  HasFDerivWithinAt (fun x => p x m.succ)
    ((↑{ toLinearEquiv := (continuousMultilinearCurryRightEquiv' 𝕜 m E F).symm.toLinearEquiv, continuous_toFun := ⋯,
            continuous_invFun := ⋯ }).comp
      ((p x).shift m.succ).curryLeft)
    s x
e_8✝ : ContinuousMultilinearMap.instAddCommGroup = SeminormedAddCommGroup.toAddCommGroup
he✝ : ContinuousMultilinearMap.instModule = NormedSpace.toModule
e_10✝ : ContinuousMultilinearMap.instTopologicalSpace = UniformSpace.toTopologicalSpace
y : E
v : Fin (m + 1) → E
⊢ ((p x (m + 1).succ).curryLeft y) v =
    (((↑{ toLinearEquiv := (continuousMultilinearCurryRightEquiv' 𝕜 m E F).symm.toLinearEquiv, continuous_toFun := ⋯,
                continuous_invFun := ⋯ }).comp
          ((p x).shift m.succ).curryLeft)
        y)
      v

Proof state:
case mpr.intro.intro.fderivWithin.zero
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ x ∈ s, (p x 0).curry0 = f x
Hfderiv_zero : ∀ x ∈ s, HasFDerivWithinAt (fun y => p y 0) (p x 1).curryLeft s x
Htaylor : HasFTaylorSeriesUpToOn (↑n) (fun x => (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x => (p x).shift) s
x : E
hx : x ∈ s
hm : ↑0 < ↑n.succ
⊢ HasFDerivWithinAt (fun x => p x 0) (p x (Nat.succ 0)).curryLeft s x

Tactic:
exact Hfderiv_zero x hx

Result:
no goals