rw [residuePull1 x_gt_one σ_pos]
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
⊢ VerticalIntegral' f σ = 1 - 1 / ↑x
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
⊢ 1 + VerticalIntegral' (Perron.f x) (-1 / 2) = 1 - 1 / ↑x