-- 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.fderivWithin
𝕜 : 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) → ∀ x ∈ s, HasFDerivWithinAt (fun x => p x m) (p x m.succ).curryLeft s x

Tactic:
intro m (hm : (m : WithTop ℕ∞) < n.succ) x (hx : x ∈ s)

Result:
case mpr.intro.intro.fderivWithin
𝕜 : 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
x : E
hx : x ∈ s
⊢ HasFDerivWithinAt (fun x => p x m) (p x m.succ).curryLeft s x

Proof state:
case mpr.intro.intro.fderivWithin.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
x : E
hx : x ∈ s
m : ℕ
hm : ↑(m + 1) < ↑n.succ
⊢ HasFDerivWithinAt (fun x => p x (m + 1)) (p x (m + 1).succ).curryLeft s x

Tactic:
have A : (m : WithTop ℕ∞) < n := by
  rw [Nat.cast_lt] at hm ⊢
  exact Nat.lt_of_succ_lt_succ hm

Result:
case mpr.intro.intro.fderivWithin.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
x : E
hx : x ∈ s
m : ℕ
hm : ↑(m + 1) < ↑n.succ
A : ↑m < ↑n
⊢ HasFDerivWithinAt (fun x => p x (m + 1)) (p x (m + 1).succ).curryLeft s x

Proof state:
𝕜 : 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
⊢ ↑m < ↑n

Tactic:
rw [Nat.cast_lt] at hm ⊢

Result:
𝕜 : 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
⊢ m < n

Proof state:
case mpr.intro.intro.zero_eq
𝕜 : 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 ∈ s, (p x 0).curry0 = f x

Tactic:
exact Hzero_eq

Result:
no goals

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

Tactic:
rcases m with - | m

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
⊢ ContinuousOn (fun x => p x 0) s

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
⊢ ContinuousOn (fun x => p x (m + 1)) s

Proof state:
case mp
𝕜 : 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 : ℕ
⊢ 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

Tactic:
intro H

Result:
case mp
𝕜 : 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 : ℕ
H : 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