simp only [add_right_neg, ← sub_eq_add_neg] at this
this : Tendsto (fun y => y + -1) (𝓝[>] 1) (𝓝[>] (1 + -1))
⊢ (fun σ => ζ ↑σ) =O[𝓝[>] 1] fun σ => 1 / (↑σ - 1)
this : Tendsto (fun y => y - 1) (𝓝[>] 1) (𝓝[>] 0)
⊢ (fun σ => ζ ↑σ) =O[𝓝[>] 1] fun σ => 1 / (↑σ - 1)