rw [add_right_comm, ← ofReal_one, ← ofReal_add, normSq_add_mul_I, add_le_add_iff_right]
case pos.h.h.h₂.h
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ 2 + t ^ 2 ≤ normSq (↑σ + ↑t * I + 1)
case pos.h.h.h₂.h
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_gt_one : 1 < σ
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ 2 ≤ (σ + 1) ^ 2