rw [VerticalIntegral', ← smul_sub, hε.2, ← RectangleIntegral', neg_div, one_div, ← ofReal_inv]
case h.intro.intro.intro.intro
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})
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0,
    RectangleIntegral' (f x) (-↑x_1 - ↑x_1 * I - 1) (↑x_1 + ↑x_1 * I - 1) = -↑x⁻¹ ∧
      VerticalIntegral (f x) (-1 / 2) - VerticalIntegral (f x) (-3 / 2) =
        RectangleIntegral (f x) (-↑x_1 - ↑x_1 * I + -1) (↑x_1 + ↑x_1 * I + -1)
c : Set ℝ
hcf : c ∈ 𝓝[>] 0
hc :
  ∀ y ∈ c,
    RectangleIntegral' (f x) (-↑y - ↑y * I - 1) (↑y + ↑y * I - 1) = -↑x⁻¹ ∧
      VerticalIntegral (f x) (-1 / 2) - VerticalIntegral (f x) (-3 / 2) =
        RectangleIntegral (f x) (-↑y - ↑y * I + -1) (↑y + ↑y * I + -1)
ε : ℝ
hεc : Metric.ball 0 ε ∩ Ioi 0 ⊆ c
hε :
  RectangleIntegral' (f x) (-↑(ε / 2) - ↑(ε / 2) * I - 1) (↑(ε / 2) + ↑(ε / 2) * I - 1) = -↑x⁻¹ ∧
    VerticalIntegral (f x) (-1 / 2) - VerticalIntegral (f x) (-3 / 2) =
      RectangleIntegral (f x) (-↑(ε / 2) - ↑(ε / 2) * I + -1) (↑(ε / 2) + ↑(ε / 2) * I + -1)
⊢ VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-1 / 2) -
      VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-3 / 2) =
    -1 / ↑x
case h.intro.intro.intro.intro
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})
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0,
    RectangleIntegral' (f x) (-↑x_1 - ↑x_1 * I - 1) (↑x_1 + ↑x_1 * I - 1) = -↑x⁻¹ ∧
      VerticalIntegral (f x) (-1 / 2) - VerticalIntegral (f x) (-3 / 2) =
        RectangleIntegral (f x) (-↑x_1 - ↑x_1 * I + -1) (↑x_1 + ↑x_1 * I + -1)
c : Set ℝ
hcf : c ∈ 𝓝[>] 0
hc :
  ∀ y ∈ c,
    RectangleIntegral' (f x) (-↑y - ↑y * I - 1) (↑y + ↑y * I - 1) = -↑x⁻¹ ∧
      VerticalIntegral (f x) (-1 / 2) - VerticalIntegral (f x) (-3 / 2) =
        RectangleIntegral (f x) (-↑y - ↑y * I + -1) (↑y + ↑y * I + -1)
ε : ℝ
hεc : Metric.ball 0 ε ∩ Ioi 0 ⊆ c
hε :
  RectangleIntegral' (f x) (-↑(ε / 2) - ↑(ε / 2) * I - 1) (↑(ε / 2) + ↑(ε / 2) * I - 1) = -↑x⁻¹ ∧
    VerticalIntegral (f x) (-1 / 2) - VerticalIntegral (f x) (-3 / 2) =
      RectangleIntegral (f x) (-↑(ε / 2) - ↑(ε / 2) * I + -1) (↑(ε / 2) + ↑(ε / 2) * I + -1)
⊢ RectangleIntegral' (f x) (-↑(ε / 2) - ↑(ε / 2) * I + -1) (↑(ε / 2) + ↑(ε / 2) * I + -1) = -↑x⁻¹