-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem ContDiffOn.ftaylorSeriesWithin
    (h : ContDiffOn 𝕜 n f s) (hs : UniqueDiffOn 𝕜 s) :
    HasFTaylorSeriesUpToOn n f (ftaylorSeriesWithin 𝕜 f s) s

Proof state:
case cont.h.intro.intro.intro.intro.intro.intro
𝕜 : 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 ℕ∞
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m ≤ n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑m) f p u
o : Set E
o_open : IsOpen o
xo : x ∈ o
ho : s ∩ o ⊆ u
⊢ ∃ t, IsOpen t ∧ x ∈ t ∧ ContinuousOn (fun x => ftaylorSeriesWithin 𝕜 f s x m) (s ∩ t)

Tactic:
refine ⟨o, o_open, xo, ?_⟩

Result:
case cont.h.intro.intro.intro.intro.intro.intro
𝕜 : 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 ℕ∞
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m ≤ n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑m) f p u
o : Set E
o_open : IsOpen o
xo : x ∈ o
ho : s ∩ o ⊆ u
⊢ ContinuousOn (fun x => ftaylorSeriesWithin 𝕜 f s x m) (s ∩ o)

Proof state:
case fderivWithin.intro.intro.intro.intro.intro.intro
𝕜 : 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 ℕ∞
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
this : ↑(m + 1) ≤ n
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(m + 1)) f p u
o : Set E
o_open : IsOpen o
xo : x ∈ o
ho : o ∩ s ⊆ u
⊢ HasFDerivWithinAt (fun x => ftaylorSeriesWithin 𝕜 f s x m) (ftaylorSeriesWithin 𝕜 f s x m.succ).curryLeft s x

Tactic:
rw [inter_comm] at ho

Result:
case fderivWithin.intro.intro.intro.intro.intro.intro
𝕜 : 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 ℕ∞
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
this : ↑(m + 1) ≤ n
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(m + 1)) f p u
o : Set E
o_open : IsOpen o
xo : x ∈ o
ho : s ∩ o ⊆ u
⊢ HasFDerivWithinAt (fun x => ftaylorSeriesWithin 𝕜 f s x m) (ftaylorSeriesWithin 𝕜 f s x m.succ).curryLeft s x

Proof state:
case fderivWithin.intro.intro.intro
𝕜 : 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 ℕ∞
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
this : ↑(m + 1) ≤ n
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(m + 1)) f p u
⊢ HasFDerivWithinAt (fun x => ftaylorSeriesWithin 𝕜 f s x m) (ftaylorSeriesWithin 𝕜 f s x m.succ).curryLeft s x

Tactic:
rw [insert_eq_of_mem hx] at hu

Result:
case fderivWithin.intro.intro.intro
𝕜 : 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 ℕ∞
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
this : ↑(m + 1) ≤ n
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(m + 1)) f p u
⊢ HasFDerivWithinAt (fun x => ftaylorSeriesWithin 𝕜 f s x m) (ftaylorSeriesWithin 𝕜 f s x m.succ).curryLeft s x

Proof state:
case cont.h.intro.intro.intro
𝕜 : 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 ℕ∞
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m ≤ n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑m) f p u
⊢ ∃ t, IsOpen t ∧ x ∈ t ∧ ContinuousOn (fun x => ftaylorSeriesWithin 𝕜 f s x m) (s ∩ t)

Tactic:
rcases mem_nhdsWithin.1 hu with ⟨o, o_open, xo, ho⟩

Result:
case cont.h.intro.intro.intro.intro.intro.intro
𝕜 : 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 ℕ∞
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m ≤ n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑m) f p u
o : Set E
o_open : IsOpen o
xo : x ∈ o
ho : o ∩ insert x s ⊆ u
⊢ ∃ t, IsOpen t ∧ x ∈ t ∧ ContinuousOn (fun x => ftaylorSeriesWithin 𝕜 f s x m) (s ∩ t)

Proof state:
case 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
n : WithTop ℕ∞
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m ≤ n
⊢ ContinuousOn (fun x => ftaylorSeriesWithin 𝕜 f s x m) s

Tactic:
apply continuousOn_of_locally_continuousOn

Result:
case cont.h
𝕜 : 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 ℕ∞
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m ≤ n
⊢ ∀ x ∈ s, ∃ t, IsOpen t ∧ x ∈ t ∧ ContinuousOn (fun x => ftaylorSeriesWithin 𝕜 f s x m) (s ∩ t)

Proof state:
case fderivWithin.intro.intro.intro.intro.intro.intro
𝕜 : 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 ℕ∞
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
this : ↑(m + 1) ≤ n
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(m + 1)) f p u
o : Set E
o_open : IsOpen o
xo : x ∈ o
ho : s ∩ o ⊆ u
⊢ HasFDerivWithinAt (fun x => ftaylorSeriesWithin 𝕜 f s x m) (ftaylorSeriesWithin 𝕜 f s x m.succ).curryLeft s x

Tactic:
have : p x m.succ = ftaylorSeriesWithin 𝕜 f s x m.succ := by
  change p x m.succ = iteratedFDerivWithin 𝕜 m.succ f s x
  rw [← iteratedFDerivWithin_inter_open o_open xo]
  exact (Hp.mono ho).eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl (hs.inter o_open) ⟨hx, xo⟩

Result:
case fderivWithin.intro.intro.intro.intro.intro.intro
𝕜 : 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 ℕ∞
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
this✝ : ↑(m + 1) ≤ n
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(m + 1)) f p u
o : Set E
o_open : IsOpen o
xo : x ∈ o
ho : s ∩ o ⊆ u
this : p x m.succ = ftaylorSeriesWithin 𝕜 f s x m.succ
⊢ HasFDerivWithinAt (fun x => ftaylorSeriesWithin 𝕜 f s x m) (ftaylorSeriesWithin 𝕜 f s x m.succ).curryLeft s x