have RectSub : Square 0 c \ {0} ⊆ {0, -1}ᶜ := by
  refine fun s ⟨hs, hs0⟩ ↦ not_or.mpr ⟨hs0, ?_⟩
  rw [Square, mem_Rect (by simpa using by linarith) (by simp [cpos.le])] at hs
  replace hs : -c ≤ s.re ∧ s.re ≤ c ∧ -c ≤ s.im ∧ s.im ≤ c := by simpa using hs
  simpa [Complex.ext_iff] using fun h ↦ by linarith
case h.intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
xpos : 0 < x
c : ℝ
bddAbove : BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s) '' (Square 0 c \ {0}))
cpos : 0 < c
right✝ : c < 1 / 2
⊢ RectangleIntegral' (f x) (-↑c - ↑c * I) (↑c + ↑c * I) = 1
case h.intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
xpos : 0 < x
c : ℝ
bddAbove : BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s) '' (Square 0 c \ {0}))
cpos : 0 < c
right✝ : c < 1 / 2
RectSub : Square 0 c \ {0} ⊆ {0, -1}ᶜ
⊢ RectangleIntegral' (f x) (-↑c - ↑c * I) (↑c + ↑c * I) = 1