simp [hs]
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
s : ℂ
hs : s = 1
⊢ s.re ≤ 1
no goals