rw [← iteratedFDerivWithin_univ, ← univ_inter u, iteratedFDerivWithin_inter 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 E
x : E
f : E → F
n : ℕ
hu : u ∈ 𝓝 x
⊢ iteratedFDerivWithin 𝕜 n f u x = iteratedFDeriv 𝕜 n f x
no goals