simpa [key'] using contDiff_const
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
key : ∀ (x : ℝ), HasDerivAt ofReal' 1 x
key' : deriv ofReal' = fun x => 1
⊢ ContDiff ℝ ⊤ (deriv ofReal')
no goals