Theorem: iteratedFDeriv_const_smul_apply' (ForML/Util.lean)

State before:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : Semiring 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : SMulCommClass 𝕜 𝕜' F
inst✝ : ContinuousConstSMul 𝕜' F
i : ℕ
a : 𝕜'
f : E → F
x : E
hf : ContDiff 𝕜 (↑i) f
⊢ iteratedFDeriv 𝕜 i (fun x => a • f x) x = a • iteratedFDeriv 𝕜 i f x
Tactic:
rw [← iteratedFDeriv_const_smul_apply hf]
State after:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : Semiring 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : SMulCommClass 𝕜 𝕜' F
inst✝ : ContinuousConstSMul 𝕜' F
i : ℕ
a : 𝕜'
f : E → F
x : E
hf : ContDiff 𝕜 (↑i) f
⊢ iteratedFDeriv 𝕜 i (fun x => a • f x) x = iteratedFDeriv 𝕜 i (a • f) x

State before:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : Semiring 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : SMulCommClass 𝕜 𝕜' F
inst✝ : ContinuousConstSMul 𝕜' F
i : ℕ
a : 𝕜'
f : E → F
x : E
hf : ContDiff 𝕜 (↑i) f
⊢ iteratedFDeriv 𝕜 i (fun x => a • f x) x = iteratedFDeriv 𝕜 i (a • f) x
Tactic:
rfl
State after:
no goals