induction n generalizing f with
| zero => exact f.integrable
| succ n ih => simpa [iteratedDeriv_succ'] using ih (f := SchwartzMap.derivCLM ℝ f)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f : 𝓢(ℝ, ℂ)
⊢ Integrable (iteratedDeriv n ⇑f) volume
no goals