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

Proof state:
case mp.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 : HasFTaylorSeriesUpToOn n f p univ
⊢ ∀ (x : E), (p x 0).curry0 = f x

Tactic:
exact fun x => H.zero_eq x (mem_univ x)

Result:
no goals

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

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

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
⊢ Continuous fun x => p x m

Tactic:
rw [continuous_iff_continuousOn_univ]

Result:
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

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 : ℕ), ↑m ≤ n → Continuous fun x => p x m

Tactic:
intro m hm

Result:
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
⊢ 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 : ℕ
hm : ↑m ≤ n
⊢ Continuous fun x => p x m

Tactic:
exact H.cont m hm

Result:
no goals

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
⊢ HasFTaylorSeriesUpTo n f p → HasFTaylorSeriesUpToOn n f p univ

Tactic:
intro H

Result:
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

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
⊢ HasFDerivWithinAt (fun y => p y m) (p x m.succ).curryLeft univ x

Tactic:
exact H.fderivWithin m hm x (mem_univ x)

Result:
no goals

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

Tactic:
constructor

Result:
case mp.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 : HasFTaylorSeriesUpToOn n f p univ
⊢ ∀ (x : E), (p x 0).curry0 = f x

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

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 : ℕ), ↑m ≤ n → Continuous fun x => p x m

Proof state:
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 : ℕ
hm : ↑m < n
x : E
a✝ : x ∈ univ
⊢ HasFDerivAt (fun x => p x m) (p x m.succ).curryLeft x

Tactic:
exact H.fderiv m hm x

Result:
no goals

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

Tactic:
intro m hm x _

Result:
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 : ℕ
hm : ↑m < n
x : E
a✝ : x ∈ univ
⊢ HasFDerivWithinAt (fun x => p x m) (p x m.succ).curryLeft univ x

Proof state:
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 : ℕ
hm : ↑m < n
x : E
a✝ : x ∈ univ
⊢ HasFDerivWithinAt (fun x => p x m) (p x m.succ).curryLeft univ x

Tactic:
rw [hasFDerivWithinAt_univ]

Result:
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 : ℕ
hm : ↑m < n
x : E
a✝ : x ∈ univ
⊢ HasFDerivAt (fun x => p x m) (p x m.succ).curryLeft x