rw [(by simp [pi_nonneg] : ‖1 / (2 * ↑π * I)‖ = 1 / (2 * π)), mul_assoc]
case h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ ‖1 / (2 * ↑π * I)‖ * ‖VerticalIntegral (f x) σ‖ ≤
    1 / (2 * π) * ‖∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))‖ * x ^ σ
case h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ 1 / (2 * π) * ‖VerticalIntegral (f x) σ‖ ≤
    1 / (2 * π) * (‖∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))‖ * x ^ σ)