refine continuousOn_const.div ?_ ?_ |>.intervalIntegrable_of_Icc (le_of_lt a_lt_b)
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ IntervalIntegrable (fun u => 1 / u ^ (s.re + 1)) MeasureTheory.volume a b
case refine_1
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ ContinuousOn (fun u => u ^ (s.re + 1)) (Icc a b)

case refine_2
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ ∀ x ∈ Icc a b, x ^ (s.re + 1) ≠ 0