simp only [← hasTemperateGrowth_smul_apply (Function.hasTemperateGrowth_id')]
case hsuc
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
n : ℕ
IH : ∀ (f : 𝓢(ℝ, F)), ContDiff ℝ ↑n fun ξ => 𝓕 (fun x => f x) ξ
f : 𝓢(ℝ, F)
⊢ ContDiff ℝ ↑n fun ξ => 𝓕 (fun x => x • f x) ξ
case hsuc
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
n : ℕ
IH : ∀ (f : 𝓢(ℝ, F)), ContDiff ℝ ↑n fun ξ => 𝓕 (fun x => f x) ξ
f : 𝓢(ℝ, F)
⊢ ContDiff ℝ ↑n fun ξ => 𝓕 (fun x => ((hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x)) f) x) ξ