simp only [← hasTemperateGrowth_smul_apply (Function.hasTemperateGrowth_pow n)]
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ‖𝓕 (fun x => x ^ n • f x) ξ‖ * |ξ| ^ k * (2 * π) ^ k = ‖𝓕 (fun x => iteratedDeriv k (fun y => y ^ n • f y) x) ξ‖
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ‖𝓕 (fun x => ((hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ n)) f) x) ξ‖ * |ξ| ^ k *
      (2 * π) ^ k =
    ‖𝓕
        (fun x =>
          iteratedDeriv k (fun x => ((hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ n)) f) x) x)
        ξ‖