Theorem: ZetaSum_aux1φDiff (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
s : ℂ
x : ℝ
xpos : 0 < x
⊢ HasDerivAt (fun t => 1 / ↑t ^ s) (deriv (fun t => 1 / ↑t ^ s) x) x
Tactic:
apply hasDerivAt_deriv_iff.mpr <| DifferentiableAt.div (differentiableAt_const _) ?_ ?_
State after:
s : ℂ
x : ℝ
xpos : 0 < x
⊢ DifferentiableAt ℝ (fun x => ↑x ^ s) x

s : ℂ
x : ℝ
xpos : 0 < x
⊢ ↑x ^ s ≠ 0

State before:
s : ℂ
x : ℝ
xpos : 0 < x
⊢ DifferentiableAt ℝ (fun x => ↑x ^ s) x
Tactic:
exact Real.differentiableAt_cpow_const_of_ne s xpos
State after:
no goals

State before:
s : ℂ
x : ℝ
xpos : 0 < x
⊢ ↑x ^ s ≠ 0
Tactic:
simp [cpow_eq_zero_iff, xpos.ne']
State after:
no goals