simp [VerticalIntegral, Real.pi_nonneg]
case h.calc_1
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ ‖VerticalIntegral (f x) σ‖ = ‖∫ (t : ℝ), ↑x ^ (↑σ + ↑t * I) / ((↑σ + ↑t * I) * (↑σ + ↑t * I + 1))‖
no goals