have e7 : (∮ z in C(z₀, r), c / (z - z₀)) = 2 * π * I * c := by
  simpa [div_eq_mul_inv, mul_comm _ _⁻¹] using circle_integral_sub_center_inv_smul hr
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
e5 :
  (∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z) =
    (∮ (z : ℂ) in C(z₀, r), c / (z - z₀)) + ∮ (z : ℂ) in C(z₀, r), deriv g z / g z
e6 : (∮ (z : ℂ) in C(z₀, r), deriv g z / g z) = 0
⊢ cindex z₀ r f = c
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
e5 :
  (∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z) =
    (∮ (z : ℂ) in C(z₀, r), c / (z - z₀)) + ∮ (z : ℂ) in C(z₀, r), deriv g z / g z
e6 : (∮ (z : ℂ) in C(z₀, r), deriv g z / g z) = 0
e7 : (∮ (z : ℂ) in C(z₀, r), c / (z - z₀)) = 2 * ↑π * I * c
⊢ cindex z₀ r f = c