calc
  _ = ‖∫ (t : ℝ), x ^ (σ + t * I) / ((σ + t * I) * (σ + t * I + 1))‖ := ?_
  _ ≤ ∫ (t : ℝ), ‖x ^ (σ + t * I) / ((σ + t * I) * (σ + t * I + 1))‖ :=
      norm_integral_le_integral_norm _
  _ = ∫ (t : ℝ), x ^ σ / ‖((σ + t * I) * (σ + t * I + 1))‖ := ?_
  _ = x ^ σ * ∫ (t : ℝ), 1 / (‖σ + t * I‖ * ‖σ + t * I + 1‖) := ?_
  _ ≤ x ^ σ * ∫ (t : ℝ), 1 / ((1 + t ^ 2).sqrt * (2 + t ^ 2).sqrt) :=
      mul_le_mul_of_nonneg_left ?_ (rpow_nonneg xpos.le _)
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ ‖VerticalIntegral (f x) σ‖ ≤ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))
case calc_1
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ ‖VerticalIntegral (f x) σ‖ = ‖∫ (t : ℝ), ↑x ^ (↑σ + ↑t * I) / ((↑σ + ↑t * I) * (↑σ + ↑t * I + 1))‖

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)‖

case calc_3
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ ∫ (t : ℝ), x ^ σ / ‖(↑σ + ↑t * I) * (↑σ + ↑t * I + 1)‖ = x ^ σ * ∫ (t : ℝ), 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖)

case calc_4
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ ∫ (t : ℝ), 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖) ≤ ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))

case calc.step
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
⊢ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2)) ≤ x ^ σ * ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))