-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
protected lemma AnalyticOn.hasFTaylorSeriesUpToOn {n : WithTop ℕ∞}
    (h : AnalyticOn 𝕜 f s) (hu : UniqueDiffOn 𝕜 s) :
    HasFTaylorSeriesUpToOn n f (ftaylorSeriesWithin 𝕜 f s) s

Proof state:
case refine_1
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
n : WithTop ℕ∞
h : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
m : ℕ
_hm : ↑m < n
x : E
hx : x ∈ s
⊢ HasFDerivWithinAt (fun x => ftaylorSeriesWithin 𝕜 f s x m) (ftaylorSeriesWithin 𝕜 f s x m.succ).curryLeft s x

Tactic:
have := (h.iteratedFDerivWithin hu m x hx).differentiableWithinAt.hasFDerivWithinAt

Result:
case refine_1
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
n : WithTop ℕ∞
h : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
m : ℕ
_hm : ↑m < n
x : E
hx : x ∈ s
this :
  HasFDerivWithinAt (iteratedFDerivWithin 𝕜 m f s) (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 m f s) (insert x s) x)
    (insert x s) x
⊢ HasFDerivWithinAt (fun x => ftaylorSeriesWithin 𝕜 f s x m) (ftaylorSeriesWithin 𝕜 f s x m.succ).curryLeft s x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
n : WithTop ℕ∞
h : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
⊢ HasFTaylorSeriesUpToOn n f (ftaylorSeriesWithin 𝕜 f s) s

Tactic:
refine ⟨fun x _hx ↦ rfl, fun m _hm x hx ↦ ?_, fun m _hm x hx ↦ ?_⟩

Result:
case refine_1
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
n : WithTop ℕ∞
h : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
m : ℕ
_hm : ↑m < n
x : E
hx : x ∈ s
⊢ HasFDerivWithinAt (fun x => ftaylorSeriesWithin 𝕜 f s x m) (ftaylorSeriesWithin 𝕜 f s x m.succ).curryLeft s x

case refine_2
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
n : WithTop ℕ∞
h : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
m : ℕ
_hm : ↑m ≤ n
x : E
hx : x ∈ s
⊢ ContinuousWithinAt (fun x => ftaylorSeriesWithin 𝕜 f s x m) s x

Proof state:
case refine_2
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
n : WithTop ℕ∞
h : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
m : ℕ
_hm : ↑m ≤ n
x : E
hx : x ∈ s
⊢ ContinuousWithinAt (fun x => ftaylorSeriesWithin 𝕜 f s x m) s x

Tactic:
exact (h.iteratedFDerivWithin hu m x hx).continuousWithinAt

Result:
no goals

Proof state:
case refine_1
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
n : WithTop ℕ∞
h : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
m : ℕ
_hm : ↑m < n
x : E
hx : x ∈ s
this :
  HasFDerivWithinAt (iteratedFDerivWithin 𝕜 m f s) (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 m f s) (insert x s) x)
    (insert x s) x
⊢ HasFDerivWithinAt (fun x => ftaylorSeriesWithin 𝕜 f s x m) (ftaylorSeriesWithin 𝕜 f s x m.succ).curryLeft s x

Tactic:
rwa [insert_eq_of_mem hx] at this

Result:
no goals