Theorem: iteratedDeriv_neg_apply (ForML/Trigonometric.lean)

State before:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
n : ℕ
f : 𝕜 → F
⊢ iteratedDeriv n (fun x => -f x) x = -iteratedDeriv n f x
Tactic:
change iteratedDeriv n (-f) x = _
State after:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
n : ℕ
f : 𝕜 → F
⊢ iteratedDeriv n (-f) x = -iteratedDeriv n f x

State before:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
n : ℕ
f : 𝕜 → F
⊢ iteratedDeriv n (-f) x = -iteratedDeriv n f x
Tactic:
simp only [iteratedDeriv_eq_iteratedFDeriv]
State after:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
n : ℕ
f : 𝕜 → F
⊢ ((iteratedFDeriv 𝕜 n (-f) x) fun x => 1) = -(iteratedFDeriv 𝕜 n f x) fun x => 1

State before:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
n : ℕ
f : 𝕜 → F
⊢ ((iteratedFDeriv 𝕜 n (-f) x) fun x => 1) = -(iteratedFDeriv 𝕜 n f x) fun x => 1
Tactic:
simp [iteratedFDeriv_neg_apply]
State after:
no goals