by_cases y_zero : (y : ℂ) = 0
case h.e'_2.h.e'_6.h
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
this : deriv (fun y => -s * (↑y ^ (r + 1) / (r + 1))) x = -s * ↑x ^ r
y : ℝ
⊢ 1 / ↑y ^ s = -s * (↑y ^ (r + 1) / (r + 1))
case pos
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
this : deriv (fun y => -s * (↑y ^ (r + 1) / (r + 1))) x = -s * ↑x ^ r
y : ℝ
y_zero : ↑y = 0
⊢ 1 / ↑y ^ s = -s * (↑y ^ (r + 1) / (r + 1))

case neg
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
this : deriv (fun y => -s * (↑y ^ (r + 1) / (r + 1))) x = -s * ↑x ^ r
y : ℝ
y_zero : ¬↑y = 0
⊢ 1 / ↑y ^ s = -s * (↑y ^ (r + 1) / (r + 1))