simpa [iteratedDerivWithin_univ] using
  iteratedDerivWithin_neg' (Set.mem_univ x) uniqueDiffOn_univ (contDiffOn_univ.mpr hf)
𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜'
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : SMulCommClass 𝕜 𝕜' F
i : ℕ
f : 𝕜 → F
x : 𝕜
hf : ContDiff 𝕜 (↑i) f
⊢ iteratedDeriv i (fun x => -f x) x = -iteratedDeriv i f x
no goals