obtain ⟨Npos, _, _, _, σPos, neOne⟩ := UpperBnd_aux ⟨by norm_num, by norm_num⟩ t_gt σ_ge
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
case intro.intro.intro.intro.intro
A : ℝ := 1 / 2
C : ℝ := A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
left✝² : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log