convert integral_cpow (a := a) (b := b) (r := -s) ?_ using 1
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
ha : a ∈ Ioo 0 b
⊢ ∫ (x : ℝ) in ↑a..↑b, 1 / ↑x ^ s = (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s)
case h.e'_2
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
ha : a ∈ Ioo 0 b
⊢ ∫ (x : ℝ) in ↑a..↑b, 1 / ↑x ^ s = ∫ (x : ℝ) in ↑a..↑b, ↑x ^ (-s)

case h.e'_3
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
ha : a ∈ Ioo 0 b
⊢ (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s) = (↑↑b ^ (-s + 1) - ↑↑a ^ (-s + 1)) / (-s + 1)

a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
ha : a ∈ Ioo 0 b
⊢ -1 < (-s).re ∨ -s ≠ -1 ∧ 0 ∉ [[↑a, ↑b]]