case zero
𝕜 : 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
hs : IsOpen s
⊢ EqOn (iteratedFDerivWithin 𝕜 Nat.zero f s) (iteratedFDeriv 𝕜 Nat.zero f) s

case succ
𝕜 : 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
hs : IsOpen s
n : ℕ
IH : EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s
⊢ EqOn (iteratedFDerivWithin 𝕜 (Nat.succ n) f s) (iteratedFDeriv 𝕜 (Nat.succ n) f) 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
n : ℕ
hs : IsOpen s
⊢ EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s
induction' n with n IH
case zero
𝕜 : 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
hs : IsOpen s
x : E
a✝ : x ∈ s
⊢ iteratedFDerivWithin 𝕜 Nat.zero f s x = iteratedFDeriv 𝕜 Nat.zero f x
case zero
𝕜 : 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
hs : IsOpen s
⊢ EqOn (iteratedFDerivWithin 𝕜 Nat.zero f s) (iteratedFDeriv 𝕜 Nat.zero f) s
intro x _
case zero.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
hs : IsOpen s
x : E
a✝ : x ∈ s
x✝ : Fin Nat.zero → E
⊢ ↑(iteratedFDerivWithin 𝕜 Nat.zero f s x) x✝ = ↑(iteratedFDeriv 𝕜 Nat.zero f x) x✝
case zero
𝕜 : 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
hs : IsOpen s
x : E
a✝ : x ∈ s
⊢ iteratedFDerivWithin 𝕜 Nat.zero f s x = iteratedFDeriv 𝕜 Nat.zero f x
ext1
no goals
case zero.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
hs : IsOpen s
x : E
a✝ : x ∈ s
x✝ : Fin Nat.zero → E
⊢ ↑(iteratedFDerivWithin 𝕜 Nat.zero f s x) x✝ = ↑(iteratedFDeriv 𝕜 Nat.zero f x) x✝
simp only [Nat.zero_eq, iteratedFDerivWithin_zero_apply, iteratedFDeriv_zero_apply]
case succ
𝕜 : 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
hs : IsOpen s
n : ℕ
IH : EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s
x : E
hx : x ∈ s
⊢ iteratedFDerivWithin 𝕜 (Nat.succ n) f s x = iteratedFDeriv 𝕜 (Nat.succ n) f x
case succ
𝕜 : 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
hs : IsOpen s
n : ℕ
IH : EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s
⊢ EqOn (iteratedFDerivWithin 𝕜 (Nat.succ n) f s) (iteratedFDeriv 𝕜 (Nat.succ n) f) s
intro x hx
case succ
𝕜 : 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
hs : IsOpen s
n : ℕ
IH : EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s
x : E
hx : x ∈ s
⊢ (↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F) ∘ fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s) x =
    (↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F) ∘ fderiv 𝕜 (iteratedFDeriv 𝕜 n f)) x
case succ
𝕜 : 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
hs : IsOpen s
n : ℕ
IH : EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s
x : E
hx : x ∈ s
⊢ iteratedFDerivWithin 𝕜 (Nat.succ n) f s x = iteratedFDeriv 𝕜 (Nat.succ n) f x
rw [iteratedFDeriv_succ_eq_comp_left, iteratedFDerivWithin_succ_eq_comp_left]
case succ
𝕜 : 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
hs : IsOpen s
n : ℕ
IH : EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s
x : E
hx : x ∈ s
⊢ ↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F) (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s x) =
    ↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F) (fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x)
case succ
𝕜 : 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
hs : IsOpen s
n : ℕ
IH : EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s
x : E
hx : x ∈ s
⊢ (↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F) ∘ fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s) x =
    (↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F) ∘ fderiv 𝕜 (iteratedFDeriv 𝕜 n f)) x
dsimp
case succ.h.e_6.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
hs : IsOpen s
n : ℕ
IH : EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s
x : E
hx : x ∈ s
⊢ fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s x = fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x
case succ
𝕜 : 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
hs : IsOpen s
n : ℕ
IH : EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s
x : E
hx : x ∈ s
⊢ ↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F) (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s x) =
    ↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F) (fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x)
congr 1
case succ.h.e_6.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
hs : IsOpen s
n : ℕ
IH : EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s
x : E
hx : x ∈ s
⊢ fderiv 𝕜 (iteratedFDerivWithin 𝕜 n f s) x = fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x
case succ.h.e_6.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
hs : IsOpen s
n : ℕ
IH : EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s
x : E
hx : x ∈ s
⊢ fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s x = fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x
rw [fderivWithin_of_open hs hx]
case succ.h.e_6.h.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
hs : IsOpen s
n : ℕ
IH : EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s
x : E
hx : x ∈ s
⊢ iteratedFDerivWithin 𝕜 n f s =ᶠ[𝓝 x] iteratedFDeriv 𝕜 n f
case succ.h.e_6.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
hs : IsOpen s
n : ℕ
IH : EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s
x : E
hx : x ∈ s
⊢ fderiv 𝕜 (iteratedFDerivWithin 𝕜 n f s) x = fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x
apply Filter.EventuallyEq.fderiv_eq
case 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
hs : IsOpen s
n : ℕ
IH : EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s
x : E
hx : x ∈ s
⊢ ∀ (a : E), a ∈ s → iteratedFDerivWithin 𝕜 n f s a = iteratedFDeriv 𝕜 n f a
case succ.h.e_6.h.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
hs : IsOpen s
n : ℕ
IH : EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s
x : E
hx : x ∈ s
⊢ iteratedFDerivWithin 𝕜 n f s =ᶠ[𝓝 x] iteratedFDeriv 𝕜 n f
filter_upwards [hs.mem_nhds hx]
no goals
case 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
hs : IsOpen s
n : ℕ
IH : EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s
x : E
hx : x ∈ s
⊢ ∀ (a : E), a ∈ s → iteratedFDerivWithin 𝕜 n f s a = iteratedFDeriv 𝕜 n f a
exact IH