rw [iteratedDerivWithin, iteratedDeriv, iteratedFDerivWithin_nhds hu]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
u : Set 𝕜
x : 𝕜
f : 𝕜 → F
n : ℕ
hu : u ∈ 𝓝 x
⊢ iteratedDerivWithin n f u x = iteratedDeriv n f x
no goals