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

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