have hasDeriv := hasDerivAt_ofReal_cpow xpos.ne' r_ne_neg1
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
⊢ deriv (fun t => 1 / ↑t ^ s) x = (fun x => -s * ↑x ^ (-(s + 1))) x
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
hasDeriv : HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
⊢ deriv (fun t => 1 / ↑t ^ s) x = (fun x => -s * ↑x ^ (-(s + 1))) x