Theorem: iteratedDeriv_neg' (ForML/Util.lean)

State before:
𝕜 : 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
Tactic:
simpa [iteratedDerivWithin_univ] using
  iteratedDerivWithin_neg' (Set.mem_univ x) uniqueDiffOn_univ (contDiffOn_univ.mpr hf)
State after:
no goals