Theorem: deriv_ofReal (PrimeNumberTheoremAnd/Fourier.lean)

State before:
⊢ deriv ofReal' = fun x => 1
Tactic:
ext x
State after:
case h
x : ℝ
⊢ deriv ofReal' x = 1

State before:
case h
x : ℝ
⊢ deriv ofReal' x = 1
Tactic:
exact ((hasDerivAt_id x).ofReal_comp).deriv
State after:
no goals