have contourPull₃ (σ' σ'' : ℝ) (hσ' : σ' ≤ -3/2) (hσ'' : σ'' ≤ -3/2) :
    VerticalIntegral' f σ' = VerticalIntegral' f σ'' :=
  contourPull3 x_gt_one hσ' hσ''
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 + (-1 / ↑x + VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-3 / 2)) = 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))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
⊢ 1 + (-1 / ↑x + VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-3 / 2)) = 1 - 1 / ↑x