ext x
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
key : ∀ (x : ℝ), HasDerivAt ofReal' 1 x
⊢ deriv ofReal' = fun x => 1
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
key : ∀ (x : ℝ), HasDerivAt ofReal' 1 x
x : ℝ
⊢ deriv ofReal' x = 1