simp_rw [ge_iff_le, norm_mul, norm_pow, ofReal_sub, ofReal_one, add_sub_cancel, ← Real.rpow_natCast] at this
σ t : ℝ
σ_gt : 1 < σ
this : ‖ζ (1 + ↑(σ - 1)) ^ 3 * ζ (1 + ↑(σ - 1) + I * ↑t) ^ 4 * ζ (1 + ↑(σ - 1) + 2 * I * ↑t)‖ ≥ 1
⊢ 1 ≤ ‖ζ ↑σ‖ ^ 3 * ‖ζ (↑σ + ↑t * I)‖ ^ 4 * ‖ζ (↑σ + 2 * ↑t * I)‖

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

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

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

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

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

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

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

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

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

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

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

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