have := integrableOn_Ioi_rpow_iff (s := r / 2 - 1) (t := N) (by simp [Npos]) |>.mpr
  (by linarith [rneg])
case hg
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ IntegrableAtFilter (fun x => x ^ (r / 2 - 1)) atTop volume
case hg
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
this : IntegrableOn (fun x => x ^ (r / 2 - 1)) (Ioi ↑N) volume
⊢ IntegrableAtFilter (fun x => x ^ (r / 2 - 1)) atTop volume