refine ⟨A, ⟨by norm_num, by norm_num⟩ , C, (by positivity), ?_⟩
A : ℝ := 1 / 2
C : ℝ := A.exp * (5 + 8 * 2)
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C, ∃ (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
A : ℝ := 1 / 2
C : ℝ := A.exp * (5 + 8 * 2)
⊢ ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log