apply setIntegral_congr (by simp)
case h
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
u : ℝ
hu : ↑N ≤ u
⊢ ∫ (x : ℝ) in Ioc (↑N) u, Complex.abs (↑⌊x⌋ + 1 / 2 - ↑x) / Complex.abs (↑x ^ (↑σ + ↑t * I + 1)) ∂volume =
    ∫ (x : ℝ) in Ioc (↑N) u, Complex.abs (↑⌊x⌋ + 1 / 2 - ↑x) / Complex.abs (↑x ^ (↑σ + ↑u * I + 1)) ∂volume
case h
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
u : ℝ
hu : ↑N ≤ u
⊢ EqOn (fun x => Complex.abs (↑⌊x⌋ + 1 / 2 - ↑x) / Complex.abs (↑x ^ (↑σ + ↑t * I + 1)))
    (fun x => Complex.abs (↑⌊x⌋ + 1 / 2 - ↑x) / Complex.abs (↑x ^ (↑σ + ↑u * I + 1))) (Ioc (↑N) u)