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) (a ^ 2 * 2) x
Tactic:
simpa using hasDerivAt_id x |>.add_const 1 |>.const_mul 2 |>.const_mul (a ^ 2)
State after:
no goals