-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem hasFTaylorSeriesUpToOn_univ_iff :
    HasFTaylorSeriesUpToOn n f p univ ↔ HasFTaylorSeriesUpTo n f p

Proof state:
case mpr
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpTo n f p
⊢ HasFTaylorSeriesUpToOn n f p univ

Tactic:
constructor

Result:
case mpr.zero_eq
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpTo n f p
⊢ ∀ x ∈ univ, (p x 0).curry0 = f x

case mpr.fderivWithin
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpTo n f p
⊢ ∀ (m : ℕ), ↑m < n → ∀ x ∈ univ, HasFDerivWithinAt (fun x => p x m) (p x m.succ).curryLeft univ x

case mpr.cont
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpTo n f p
⊢ ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => p x m) univ

Proof state:
case mp.fderiv
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn n f p univ
m : ℕ
hm : ↑m < n
x : E
⊢ HasFDerivAt (fun y => p y m) (p x m.succ).curryLeft x

Tactic:
rw [← hasFDerivWithinAt_univ]

Result:
case mp.fderiv
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn n f p univ
m : ℕ
hm : ↑m < n
x : E
⊢ HasFDerivWithinAt (fun y => p y m) (p x m.succ).curryLeft univ x

Proof state:
case mpr.cont
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpTo n f p
m : ℕ
hm : ↑m ≤ n
⊢ ContinuousOn (fun x => p x m) univ

Tactic:
rw [← continuous_iff_continuousOn_univ]

Result:
case mpr.cont
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpTo n f p
m : ℕ
hm : ↑m ≤ n
⊢ Continuous fun x => p x m

Proof state:
case mpr.cont
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpTo n f p
⊢ ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => p x m) univ

Tactic:
intro m hm

Result:
case mpr.cont
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpTo n f p
m : ℕ
hm : ↑m ≤ n
⊢ ContinuousOn (fun x => p x m) univ

Proof state:
case mpr.zero_eq
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpTo n f p
⊢ ∀ x ∈ univ, (p x 0).curry0 = f x

Tactic:
exact fun x _ => H.zero_eq x

Result:
no goals

Proof state:
case mp.fderiv
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn n f p univ
⊢ ∀ (m : ℕ), ↑m < n → ∀ (x : E), HasFDerivAt (fun y => p y m) (p x m.succ).curryLeft x

Tactic:
intro m hm x

Result:
case mp.fderiv
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn n f p univ
m : ℕ
hm : ↑m < n
x : E
⊢ HasFDerivAt (fun y => p y m) (p x m.succ).curryLeft x

Proof state:
case mp.cont
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn n f p univ
m : ℕ
hm : ↑m ≤ n
⊢ ContinuousOn (fun x => p x m) univ

Tactic:
exact H.cont m hm

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
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
⊢ HasFTaylorSeriesUpToOn n f p univ ↔ HasFTaylorSeriesUpTo n f p

Tactic:
constructor

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
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
⊢ HasFTaylorSeriesUpToOn n f p univ → HasFTaylorSeriesUpTo n f p

case mpr
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
⊢ HasFTaylorSeriesUpTo n f p → HasFTaylorSeriesUpToOn n f p univ