simpa [iteratedDeriv_succ'] using ih (f := SchwartzMap.derivCLM ℝ f)
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n✝ n : ℕ
ih : ∀ {f : 𝓢(ℝ, ℂ)}, Integrable (iteratedDeriv n ⇑f) volume
f : 𝓢(ℝ, ℂ)
⊢ Integrable (iteratedDeriv (n + 1) ⇑f) volume
no goals