apply IntegrableOn.congr_fun this ?_ (by simp)
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
this : IntegrableOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (Ioi ↑N) volume
⊢ Integrable (fun a => Complex.abs (↑a ^ (-s - 1)) * |a.log|) (volume.restrict (Ioi ↑N))
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
this : IntegrableOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (Ioi ↑N) volume
⊢ EqOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (fun a => Complex.abs (↑a ^ (-s - 1)) * |a.log|) (Ioi ↑N)