swap
case pos
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ ∫ (t : ℝ), 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖) ≤ ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))

case neg
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : ¬Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ ∫ (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))
case neg
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : ¬Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ ∫ (t : ℝ), 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖) ≤ ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))

case pos
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
⊢ ∫ (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))