have := riemannZeta_isBigO_near_one_horizontal.comp_tendsto this
this : Tendsto (fun y => y - 1) (𝓝[>] 1) (𝓝[>] 0)
⊢ (fun σ => ζ ↑σ) =O[𝓝[>] 1] fun σ => 1 / (↑σ - 1)
this✝ : Tendsto (fun y => y - 1) (𝓝[>] 1) (𝓝[>] 0)
this : ((fun x => ζ (1 + ↑x)) ∘ fun y => y - 1) =O[𝓝[>] 1] ((fun x => 1 / ↑x) ∘ fun y => y - 1)
⊢ (fun σ => ζ ↑σ) =O[𝓝[>] 1] fun σ => 1 / (↑σ - 1)