have key' : deriv ofReal' = fun _ => 1 := by ext x ; exact (key x).deriv
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
key : ∀ (x : ℝ), HasDerivAt ofReal' 1 x
⊢ ContDiff ℝ ⊤ ofReal'
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
key : ∀ (x : ℝ), HasDerivAt ofReal' 1 x
key' : deriv ofReal' = fun x => 1
⊢ ContDiff ℝ ⊤ ofReal'