exact contDiff_top.mpr fun n ↦ IH n f
case htop
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
IH : ∀ (n : ℕ) (f : 𝓢(ℝ, F)), ContDiff ℝ ↑n fun ξ => 𝓕 (fun x => f x) ξ
f : 𝓢(ℝ, F)
⊢ ContDiff ℝ ⊤ fun ξ => 𝓕 (fun x => f x) ξ
no goals