any_goals apply norm_nonneg
case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I * 2)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I * 2)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + ↑t * I * 2)‖ ^ (1 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I)‖
case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I * 2)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + ↑t * I * 2)‖ ^ (1 / 4)