case zero_eq
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
⊢ ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (ftaylorSeriesWithin 𝕜 f s x 0) = f x

case fderivWithin
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
⊢ ∀ (m : ℕ),
    ↑m < n →
      ∀ (x : E),
        x ∈ s →
          HasFDerivWithinAt (fun x => ftaylorSeriesWithin 𝕜 f s x m)
            (ContinuousMultilinearMap.curryLeft (ftaylorSeriesWithin 𝕜 f s x (Nat.succ m))) s x

case cont
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
⊢ ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => ftaylorSeriesWithin 𝕜 f s x m) s
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
⊢ HasFTaylorSeriesUpToOn n f (ftaylorSeriesWithin 𝕜 f s) s
constructor
case zero_eq
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
x : E
a✝ : x ∈ s
⊢ ContinuousMultilinearMap.uncurry0 (ftaylorSeriesWithin 𝕜 f s x 0) = f x
case zero_eq
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
⊢ ∀ (x : E), x ∈ s → ContinuousMultilinearMap.uncurry0 (ftaylorSeriesWithin 𝕜 f s x 0) = f x
intro x _
no goals
case zero_eq
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
x : E
a✝ : x ∈ s
⊢ ContinuousMultilinearMap.uncurry0 (ftaylorSeriesWithin 𝕜 f s x 0) = f x
simp only [ftaylorSeriesWithin, ContinuousMultilinearMap.uncurry0_apply,
  iteratedFDerivWithin_zero_apply]
case fderivWithin
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
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)
    (ContinuousMultilinearMap.curryLeft (ftaylorSeriesWithin 𝕜 f s x (Nat.succ m))) s x
case fderivWithin
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
⊢ ∀ (m : ℕ),
    ↑m < n →
      ∀ (x : E),
        x ∈ s →
          HasFDerivWithinAt (fun x => ftaylorSeriesWithin 𝕜 f s x m)
            (ContinuousMultilinearMap.curryLeft (ftaylorSeriesWithin 𝕜 f s x (Nat.succ m))) s x
intro m hm x hx
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
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
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 (↑(Nat.succ m)) f p u
⊢ HasFDerivWithinAt (fun x => ftaylorSeriesWithin 𝕜 f s x m)
    (ContinuousMultilinearMap.curryLeft (ftaylorSeriesWithin 𝕜 f s x (Nat.succ m))) s x
case fderivWithin
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
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)
    (ContinuousMultilinearMap.curryLeft (ftaylorSeriesWithin 𝕜 f s x (Nat.succ m))) s x
rcases(h x hx) m.succ (ENat.add_one_le_of_lt hm) with ⟨u, hu, p, Hp⟩
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
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(Nat.succ m)) f p u
⊢ HasFDerivWithinAt (fun x => ftaylorSeriesWithin 𝕜 f s x m)
    (ContinuousMultilinearMap.curryLeft (ftaylorSeriesWithin 𝕜 f s x (Nat.succ m))) s x
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
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
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 (↑(Nat.succ m)) f p u
⊢ HasFDerivWithinAt (fun x => ftaylorSeriesWithin 𝕜 f s x m)
    (ContinuousMultilinearMap.curryLeft (ftaylorSeriesWithin 𝕜 f s x (Nat.succ m))) s x
rw [insert_eq_of_mem hx] at hu
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
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(Nat.succ m)) 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)
    (ContinuousMultilinearMap.curryLeft (ftaylorSeriesWithin 𝕜 f s x (Nat.succ m))) s x
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
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(Nat.succ m)) f p u
⊢ HasFDerivWithinAt (fun x => ftaylorSeriesWithin 𝕜 f s x m)
    (ContinuousMultilinearMap.curryLeft (ftaylorSeriesWithin 𝕜 f s x (Nat.succ m))) s x
rcases mem_nhdsWithin.1 hu with ⟨o, o_open, xo, ho⟩
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
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(Nat.succ m)) 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)
    (ContinuousMultilinearMap.curryLeft (ftaylorSeriesWithin 𝕜 f s x (Nat.succ m))) s x
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
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(Nat.succ m)) 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)
    (ContinuousMultilinearMap.curryLeft (ftaylorSeriesWithin 𝕜 f s x (Nat.succ m))) s x
rw [inter_comm] at ho
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
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(Nat.succ m)) f p u
o : Set E
o_open : IsOpen o
xo : x ∈ o
ho : s ∩ o ⊆ u
this : p x (Nat.succ m) = ftaylorSeriesWithin 𝕜 f s x (Nat.succ m)
⊢ HasFDerivWithinAt (fun x => ftaylorSeriesWithin 𝕜 f s x m)
    (ContinuousMultilinearMap.curryLeft (ftaylorSeriesWithin 𝕜 f s x (Nat.succ m))) s x
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
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(Nat.succ m)) 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)
    (ContinuousMultilinearMap.curryLeft (ftaylorSeriesWithin 𝕜 f s x (Nat.succ m))) s x
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_ftaylor_series_of_uniqueDiffOn le_rfl (hs.inter o_open) ⟨hx, xo⟩
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
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(Nat.succ m)) f p u
o : Set E
o_open : IsOpen o
xo : x ∈ o
ho : s ∩ o ⊆ u
this : p x (Nat.succ m) = ftaylorSeriesWithin 𝕜 f s x (Nat.succ m)
⊢ HasFDerivWithinAt (fun x => ftaylorSeriesWithin 𝕜 f s x m) (ContinuousMultilinearMap.curryLeft (p x (Nat.succ m)))
    (s ∩ o) x
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
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(Nat.succ m)) f p u
o : Set E
o_open : IsOpen o
xo : x ∈ o
ho : s ∩ o ⊆ u
this : p x (Nat.succ m) = ftaylorSeriesWithin 𝕜 f s x (Nat.succ m)
⊢ HasFDerivWithinAt (fun x => ftaylorSeriesWithin 𝕜 f s x m)
    (ContinuousMultilinearMap.curryLeft (ftaylorSeriesWithin 𝕜 f s x (Nat.succ m))) s x
rw [← this, ← hasFDerivWithinAt_inter (IsOpen.mem_nhds o_open xo)]
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
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(Nat.succ m)) f p u
o : Set E
o_open : IsOpen o
xo : x ∈ o
ho : s ∩ o ⊆ u
this : p x (Nat.succ m) = ftaylorSeriesWithin 𝕜 f s x (Nat.succ m)
A : ∀ (y : E), y ∈ s ∩ o → p y m = ftaylorSeriesWithin 𝕜 f s y m
⊢ HasFDerivWithinAt (fun x => ftaylorSeriesWithin 𝕜 f s x m) (ContinuousMultilinearMap.curryLeft (p x (Nat.succ m)))
    (s ∩ o) x
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
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(Nat.succ m)) f p u
o : Set E
o_open : IsOpen o
xo : x ∈ o
ho : s ∩ o ⊆ u
this : p x (Nat.succ m) = ftaylorSeriesWithin 𝕜 f s x (Nat.succ m)
⊢ HasFDerivWithinAt (fun x => ftaylorSeriesWithin 𝕜 f s x m) (ContinuousMultilinearMap.curryLeft (p x (Nat.succ m)))
    (s ∩ o) x
have A : ∀ y ∈ s ∩ o, p y m = ftaylorSeriesWithin 𝕜 f s y m := by
  rintro y ⟨hy, yo⟩
  change p y m = iteratedFDerivWithin 𝕜 m f s y
  rw [← iteratedFDerivWithin_inter_open o_open yo]
  exact
    (Hp.mono ho).eq_ftaylor_series_of_uniqueDiffOn (WithTop.coe_le_coe.2 (Nat.le_succ m))
      (hs.inter o_open) ⟨hy, yo⟩
no goals
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
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(Nat.succ m)) f p u
o : Set E
o_open : IsOpen o
xo : x ∈ o
ho : s ∩ o ⊆ u
this : p x (Nat.succ m) = ftaylorSeriesWithin 𝕜 f s x (Nat.succ m)
A : ∀ (y : E), y ∈ s ∩ o → p y m = ftaylorSeriesWithin 𝕜 f s y m
⊢ HasFDerivWithinAt (fun x => ftaylorSeriesWithin 𝕜 f s x m) (ContinuousMultilinearMap.curryLeft (p x (Nat.succ m)))
    (s ∩ o) x
exact
  ((Hp.mono ho).fderivWithin m (WithTop.coe_lt_coe.2 (lt_add_one m)) x ⟨hx, xo⟩).congr
    (fun y hy => (A y hy).symm) (A x ⟨hx, xo⟩).symm
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(Nat.succ m)) f p u
o : Set E
o_open : IsOpen o
xo : x ∈ o
ho : s ∩ o ⊆ u
⊢ p x (Nat.succ m) = iteratedFDerivWithin 𝕜 (Nat.succ m) f s x
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(Nat.succ m)) f p u
o : Set E
o_open : IsOpen o
xo : x ∈ o
ho : s ∩ o ⊆ u
⊢ p x (Nat.succ m) = ftaylorSeriesWithin 𝕜 f s x (Nat.succ m)
change p x m.succ = iteratedFDerivWithin 𝕜 m.succ f s x
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(Nat.succ m)) f p u
o : Set E
o_open : IsOpen o
xo : x ∈ o
ho : s ∩ o ⊆ u
⊢ p x (Nat.succ m) = iteratedFDerivWithin 𝕜 (Nat.succ m) f (s ∩ o) x
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(Nat.succ m)) f p u
o : Set E
o_open : IsOpen o
xo : x ∈ o
ho : s ∩ o ⊆ u
⊢ p x (Nat.succ m) = iteratedFDerivWithin 𝕜 (Nat.succ m) f s x
rw [← iteratedFDerivWithin_inter_open o_open xo]
no goals
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(Nat.succ m)) f p u
o : Set E
o_open : IsOpen o
xo : x ∈ o
ho : s ∩ o ⊆ u
⊢ p x (Nat.succ m) = iteratedFDerivWithin 𝕜 (Nat.succ m) f (s ∩ o) x
exact (Hp.mono ho).eq_ftaylor_series_of_uniqueDiffOn le_rfl (hs.inter o_open) ⟨hx, xo⟩
case intro
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(Nat.succ m)) f p u
o : Set E
o_open : IsOpen o
xo : x ∈ o
ho : s ∩ o ⊆ u
this : p x (Nat.succ m) = ftaylorSeriesWithin 𝕜 f s x (Nat.succ m)
y : E
hy : y ∈ s
yo : y ∈ o
⊢ p y m = ftaylorSeriesWithin 𝕜 f s y m
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(Nat.succ m)) f p u
o : Set E
o_open : IsOpen o
xo : x ∈ o
ho : s ∩ o ⊆ u
this : p x (Nat.succ m) = ftaylorSeriesWithin 𝕜 f s x (Nat.succ m)
⊢ ∀ (y : E), y ∈ s ∩ o → p y m = ftaylorSeriesWithin 𝕜 f s y m
rintro y ⟨hy, yo⟩
case intro
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(Nat.succ m)) f p u
o : Set E
o_open : IsOpen o
xo : x ∈ o
ho : s ∩ o ⊆ u
this : p x (Nat.succ m) = ftaylorSeriesWithin 𝕜 f s x (Nat.succ m)
y : E
hy : y ∈ s
yo : y ∈ o
⊢ p y m = iteratedFDerivWithin 𝕜 m f s y
case intro
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(Nat.succ m)) f p u
o : Set E
o_open : IsOpen o
xo : x ∈ o
ho : s ∩ o ⊆ u
this : p x (Nat.succ m) = ftaylorSeriesWithin 𝕜 f s x (Nat.succ m)
y : E
hy : y ∈ s
yo : y ∈ o
⊢ p y m = ftaylorSeriesWithin 𝕜 f s y m
change p y m = iteratedFDerivWithin 𝕜 m f s y
case intro
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(Nat.succ m)) f p u
o : Set E
o_open : IsOpen o
xo : x ∈ o
ho : s ∩ o ⊆ u
this : p x (Nat.succ m) = ftaylorSeriesWithin 𝕜 f s x (Nat.succ m)
y : E
hy : y ∈ s
yo : y ∈ o
⊢ p y m = iteratedFDerivWithin 𝕜 m f (s ∩ o) y
case intro
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(Nat.succ m)) f p u
o : Set E
o_open : IsOpen o
xo : x ∈ o
ho : s ∩ o ⊆ u
this : p x (Nat.succ m) = ftaylorSeriesWithin 𝕜 f s x (Nat.succ m)
y : E
hy : y ∈ s
yo : y ∈ o
⊢ p y m = iteratedFDerivWithin 𝕜 m f s y
rw [← iteratedFDerivWithin_inter_open o_open yo]
no goals
case intro
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(Nat.succ m)) f p u
o : Set E
o_open : IsOpen o
xo : x ∈ o
ho : s ∩ o ⊆ u
this : p x (Nat.succ m) = ftaylorSeriesWithin 𝕜 f s x (Nat.succ m)
y : E
hy : y ∈ s
yo : y ∈ o
⊢ p y m = iteratedFDerivWithin 𝕜 m f (s ∩ o) y
exact
  (Hp.mono ho).eq_ftaylor_series_of_uniqueDiffOn (WithTop.coe_le_coe.2 (Nat.le_succ m))
    (hs.inter o_open) ⟨hy, yo⟩
case cont
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m✝ n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m ≤ n
⊢ ContinuousOn (fun x => ftaylorSeriesWithin 𝕜 f s x m) s
case cont
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
⊢ ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => ftaylorSeriesWithin 𝕜 f s x m) s
intro m hm
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
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m✝ n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m ≤ n
⊢ ∀ (x : E), x ∈ s → ∃ t, IsOpen t ∧ x ∈ t ∧ ContinuousOn (fun x => ftaylorSeriesWithin 𝕜 f s x m) (s ∩ t)
case cont
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m✝ n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m ≤ n
⊢ ContinuousOn (fun x => ftaylorSeriesWithin 𝕜 f s x m) s
apply continuousOn_of_locally_continuousOn
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
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m ≤ n
x : E
hx : x ∈ s
⊢ ∃ t, IsOpen t ∧ x ∈ t ∧ ContinuousOn (fun x => ftaylorSeriesWithin 𝕜 f s x m) (s ∩ t)
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
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m✝ n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m ≤ n
⊢ ∀ (x : E), x ∈ s → ∃ t, IsOpen t ∧ x ∈ t ∧ ContinuousOn (fun x => ftaylorSeriesWithin 𝕜 f s x m) (s ∩ t)
intro x hx
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
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
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)
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
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m ≤ n
x : E
hx : x ∈ s
⊢ ∃ t, IsOpen t ∧ x ∈ t ∧ ContinuousOn (fun x => ftaylorSeriesWithin 𝕜 f s x m) (s ∩ t)
rcases h x hx m hm with ⟨u, hu, p, Hp⟩
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
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
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)
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
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
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)
rcases mem_nhdsWithin.1 hu with ⟨o, o_open, xo, ho⟩
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
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
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)
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
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
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)
rw [insert_eq_of_mem hx] at ho
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
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
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)
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
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
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)
rw [inter_comm] at ho
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
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
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)
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
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
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)
refine' ⟨o, o_open, xo, _⟩
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
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
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
A : ∀ (y : E), y ∈ s ∩ o → p y m = ftaylorSeriesWithin 𝕜 f s y m
⊢ ContinuousOn (fun x => ftaylorSeriesWithin 𝕜 f s x m) (s ∩ o)
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
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
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)
have A : ∀ y ∈ s ∩ o, p y m = ftaylorSeriesWithin 𝕜 f s y m := by
  rintro y ⟨hy, yo⟩
  change p y m = iteratedFDerivWithin 𝕜 m f s y
  rw [← iteratedFDerivWithin_inter_open o_open yo]
  exact (Hp.mono ho).eq_ftaylor_series_of_uniqueDiffOn le_rfl (hs.inter o_open) ⟨hy, yo⟩
no goals
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
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
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
A : ∀ (y : E), y ∈ s ∩ o → p y m = ftaylorSeriesWithin 𝕜 f s y m
⊢ ContinuousOn (fun x => ftaylorSeriesWithin 𝕜 f s x m) (s ∩ o)
exact ((Hp.mono ho).cont m le_rfl).congr fun y hy => (A y hy).symm
case intro
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
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 = ftaylorSeriesWithin 𝕜 f s y m
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
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), y ∈ s ∩ o → p y m = ftaylorSeriesWithin 𝕜 f s y m
rintro y ⟨hy, yo⟩
case intro
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
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
case intro
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
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 = ftaylorSeriesWithin 𝕜 f s y m
change p y m = iteratedFDerivWithin 𝕜 m f s y
case intro
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
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
case intro
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
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
rw [← iteratedFDerivWithin_inter_open o_open yo]
no goals
case intro
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
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
exact (Hp.mono ho).eq_ftaylor_series_of_uniqueDiffOn le_rfl (hs.inter o_open) ⟨hy, yo⟩