Theorem: pp_deriv (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a x : ℝ
⊢ HasDerivAt (pp a) (pp' a x) x
Tactic:
simpa using hasDerivAt_id x |>.add_const 1 |>.pow 2 |>.const_mul _ |>.add_const _
State after:
no goals