have h6 : ∀ z ∈ sphere c r, deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z := by
  rintro z hz
  have h3 : ∀ z ∈ U, f z = (z - z₀) * g z :=
    λ z _ => by simpa only [smul_eq_mul, hfz₀, sub_zero] using (sub_smul_dslope f z₀ z).symm
  have hz' : z ∈ U := hcr (sphere_subset_closedBall hz)
  have e0 : U ∈ 𝓝 z := hU.mem_nhds hz'
  have h4 : deriv f z = deriv (λ w => (w - z₀) * g w) z :=
    EventuallyEq.deriv_eq (eventually_of_mem e0 h3)
  have e1 : DifferentiableAt ℂ (λ y => y - z₀) z := differentiableAt_id.sub_const z₀
  have e2 : DifferentiableAt ℂ g z := h1.differentiableAt e0
  have h5 : deriv f z = g z + (z - z₀) * deriv g z := by
    have : deriv (fun y => y - z₀) z = 1 := by
      change deriv (fun y => id y - z₀) z = 1
      simp [deriv_sub_const]
    simp [h4, deriv_mul e1 e2, this]
  have e3 : g z ≠ 0 := h2 z (sphere_subset_closedBall hz)
  field_simp [h3 z hz', h5, mul_comm, h10 z hz]
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
⊢ cindex c r f = ((2 * ↑Real.pi * I)⁻¹ * ∮ (z : ℂ) in C(c, r), (z - z₀)⁻¹) + cindex c r g
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
h6 : ∀ z ∈ sphere c r, deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z
⊢ cindex c r f = ((2 * ↑Real.pi * I)⁻¹ * ∮ (z : ℂ) in C(c, r), (z - z₀)⁻¹) + cindex c r g