gcongr <;> apply sqrt_le_sqrt
case pos.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ 1 / (‖↑σ + ↑t * I‖ * ‖↑σ + ↑t * I + 1‖) ≤ 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
case pos.h.h.h₁.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ 4⁻¹ + t ^ 2 ≤ normSq (↑σ + ↑t * I)

case pos.h.h.h₂.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ 4⁻¹ + t ^ 2 ≤ normSq (↑σ + ↑t * I + 1)