Theorem: HasDerivAt_neg_cpow_over2 (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
N : ℕ
Npos : 0 < N
s : ℂ
⊢ HasDerivAt (fun x => -↑N ^ (-x) / 2) (-(-↑(↑N).log * ↑N ^ (-s)) / 2) s
Tactic:
convert hasDerivAt_neg' s |>.const_cpow (c := N) (by aesop) |>.neg |>.div_const _ using 1
State after:
case h.e'_7
N : ℕ
Npos : 0 < N
s : ℂ
⊢ -(-↑(↑N).log * ↑N ^ (-s)) / 2 = -(↑N ^ (-s) * (↑N).log * -1) / 2

State before:
case h.e'_7
N : ℕ
Npos : 0 < N
s : ℂ
⊢ -(-↑(↑N).log * ↑N ^ (-s)) / 2 = -(↑N ^ (-s) * (↑N).log * -1) / 2
Tactic:
simp [mul_comm]
State after:
no goals

State before:
N : ℕ
Npos : 0 < N
s : ℂ
⊢ ↑N ≠ 0 ∨ -s ≠ 0
Tactic:
aesop
State after:
no goals