simp [Complex.abs_cpow_eq_rpow_re_of_pos xpos]
case calc_2
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ ∫ (t : ℝ), ‖↑x ^ (↑σ + ↑t * I) / ((↑σ + ↑t * I) * (↑σ + ↑t * I + 1))‖ =
    ∫ (t : ℝ), x ^ σ / ‖(↑σ + ↑t * I) * (↑σ + ↑t * I + 1)‖
no goals