-- 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 mpr.intro.intro.cont.succ
𝕜 : 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
m : ℕ
hm : ↑(m + 1) ≤ ↑n.succ
⊢ ↑m ≤ ↑n

Tactic:
rw [Nat.cast_le] at hm ⊢

Result:
case mpr.intro.intro.cont.succ
𝕜 : 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
m : ℕ
hm : m + 1 ≤ n.succ
⊢ m ≤ n

Proof state:
case mpr.intro.intro.cont.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
hm : ↑0 ≤ ↑n.succ
⊢ ContinuousOn (fun x => p x 0) s

Tactic:
have : DifferentiableOn 𝕜 (fun x => p x 0) s := fun x hx =>
  (Hfderiv_zero x hx).differentiableWithinAt

Result:
case mpr.intro.intro.cont.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
hm : ↑0 ≤ ↑n.succ
this : DifferentiableOn 𝕜 (fun x => p x 0) s
⊢ ContinuousOn (fun x => p x 0) s

Proof state:
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

Tactic:
change
  (p x (Nat.succ (Nat.succ m))) (cons y v) =
    (p x m.succ.succ) (snoc (cons y (init v)) (v (last _)))

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.succ.succ) (cons y v) = (p x m.succ.succ) (snoc (cons y (init v)) (v (last m)))

Proof state:
case mpr.intro.intro.cont
𝕜 : 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
⊢ ∀ (m : ℕ), ↑m ≤ ↑(n + 1) → ContinuousOn (fun x => p x m) s

Tactic:
intro m (hm : (m : WithTop ℕ∞) ≤ n.succ)

Result:
case mpr.intro.intro.cont
𝕜 : 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
m : ℕ
hm : ↑m ≤ ↑n.succ
⊢ ContinuousOn (fun x => p x m) s