simp [← hg, hasTemperateGrowth_smul_apply, iteratedPDeriv_eq_iteratedFDeriv,
  iteratedDeriv_eq_iteratedFDeriv]
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
x : ℝ
⊢ x ^ k • iteratedDeriv n (⇑f) x = g x
no goals