congr with t
case h.calc_2
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ ∫ (t : ℝ), ‖↑x ^ (↑σ + ↑t * I) / ((↑σ + ↑t * I) * (↑σ + ↑t * I + 1))‖ =
    ∫ (t : ℝ), x ^ σ / ‖(↑σ + ↑t * I) * (↑σ + ↑t * I + 1)‖
case h.calc_2.e_f.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
t : ℝ
⊢ ‖↑x ^ (↑σ + ↑t * I) / ((↑σ + ↑t * I) * (↑σ + ↑t * I + 1))‖ = x ^ σ / ‖(↑σ + ↑t * I) * (↑σ + ↑t * I + 1)‖