have hf : HolomorphicOn (f x) (Icc (-3 / 2) (-1 / 2) ×ℂ univ \ {-1}) :=
  (isHolomorphicOn xpos).mono fun s ⟨⟨⟨_, _⟩, _⟩, hs1⟩ hc ↦ hc.casesOn
    (fun hc ↦ by linarith [show s.re = 0 from congrArg _ hc]) (fun hc ↦ hs1 hc)
case 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
xpos : 0 < x
⊢ VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-1 / 2) -
      VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-3 / 2) =
    -1 / ↑x
case 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
xpos : 0 < x
hf : HolomorphicOn (f x) (Icc (-3 / 2) (-1 / 2) ×ℂ univ \ {-1})
⊢ VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-1 / 2) -
      VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-3 / 2) =
    -1 / ↑x