have r_ne_neg1 : r ≠ -1 := fun hr ↦ (hr ▸ r_add1_ne_zero) <| by norm_num
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
⊢ 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
⊢ deriv (fun t => 1 / ↑t ^ s) x = (fun x => -s * ↑x ^ (-(s + 1))) x