intro σ t t_gt ⟨σ_ge, σ_le⟩
A : ℝ := 1 / 2
C : ℝ := A.exp * (5 + 8 * 2)
⊢ ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
A : ℝ := 1 / 2
C : ℝ := A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
⊢ ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log