-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem hasFTaylorSeriesUpToOn_succ_iff_right :
    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:
𝕜 : 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
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
⊢ 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:
match n with
| ⊤ => exact hasFTaylorSeriesUpToOn_top_iff_right (by simp)
| (⊤ : ℕ∞) => exact hasFTaylorSeriesUpToOn_top_iff_right (by simp)
| (n : ℕ) => exact hasFTaylorSeriesUpToOn_succ_nat_iff_right

Result:
no goals

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
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
⊢ ∞ ≤ ∞ + 1

Tactic:
simp

Result:
no goals

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
n✝ : WithTop ℕ∞
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:
exact hasFTaylorSeriesUpToOn_succ_nat_iff_right

Result:
no goals

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
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
⊢ HasFTaylorSeriesUpToOn (∞ + 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 ∞ (fun x => (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x => (p x).shift) s

Tactic:
exact hasFTaylorSeriesUpToOn_top_iff_right (by simp)

Result:
no goals

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
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
⊢ ∞ ≤ ω + 1

Tactic:
simp

Result:
no goals

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
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
⊢ HasFTaylorSeriesUpToOn (ω + 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 ω (fun x => (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x => (p x).shift) s

Tactic:
exact hasFTaylorSeriesUpToOn_top_iff_right (by simp)

Result:
no goals