-- 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 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
y : E
hy : y ∈ s
yo : y ∈ o
⊢ p y m = iteratedFDerivWithin 𝕜 m f s y

Tactic:
rw [← iteratedFDerivWithin_inter_open o_open yo]

Result:
case 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
y : E
hy : y ∈ s
yo : y ∈ o
⊢ p y m = iteratedFDerivWithin 𝕜 m f (s ∩ o) y

Proof state:
case 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
y : E
hy : y ∈ s
yo : y ∈ o
⊢ p y m = iteratedFDerivWithin 𝕜 m f s y

Tactic:
rw [← iteratedFDerivWithin_inter_open o_open yo]

Result:
case 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
y : E
hy : y ∈ s
yo : y ∈ o
⊢ p y m = iteratedFDerivWithin 𝕜 m f (s ∩ o) y

Proof state:
case 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
y : E
hy : y ∈ s
yo : y ∈ o
⊢ p y m = iteratedFDerivWithin 𝕜 m f (s ∩ o) y

Tactic:
exact
  (Hp.mono ho).eq_iteratedFDerivWithin_of_uniqueDiffOn (mod_cast Nat.le_succ m)
    (hs.inter o_open) ⟨hy, yo⟩

Result:
no goals

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 : o ∩ insert x s ⊆ u
⊢ ∃ t, IsOpen t ∧ x ∈ t ∧ ContinuousOn (fun x => ftaylorSeriesWithin 𝕜 f s x m) (s ∩ t)

Tactic:
rw [insert_eq_of_mem hx] at 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 ∩ s ⊆ u
⊢ ∃ t, IsOpen t ∧ x ∈ t ∧ ContinuousOn (fun x => ftaylorSeriesWithin 𝕜 f s x m) (s ∩ t)

Proof state:
case fderivWithin
𝕜 : 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 : ℕ),
    ↑m < n →
      ∀ x ∈ s,
        HasFDerivWithinAt (fun x => ftaylorSeriesWithin 𝕜 f s x m) (ftaylorSeriesWithin 𝕜 f s x m.succ).curryLeft s x

Tactic:
intro m hm x hx

Result:
case fderivWithin
𝕜 : 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
⊢ HasFDerivWithinAt (fun x => ftaylorSeriesWithin 𝕜 f s x m) (ftaylorSeriesWithin 𝕜 f s x m.succ).curryLeft s x

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 ℕ∞
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
⊢ ∀ y ∈ s ∩ o, p y m = ftaylorSeriesWithin 𝕜 f s y m

Tactic:
rintro y ⟨hy, yo⟩

Result:
case 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
y : E
hy : y ∈ s
yo : y ∈ o
⊢ p y m = ftaylorSeriesWithin 𝕜 f s y m