simp
case h.e'_8.h
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)
x✝ : ℝ
⊢ 1 / (↑x✝ - 1) = ((fun x => 1 / ↑x) ∘ fun y => y - 1) x✝
no goals