simp [σPos]
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ 0 < (↑σ + ↑t * I).re
no goals