simp [cindex, circle_integral_eq_zero h2 hr h3 (((f_hol.mono h1).deriv h2).div (f_hol.mono h1) h4)]
case intro.intro.intro.intro
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
hcr : closedBall c r ⊆ U
f_hol : DifferentiableOn ℂ f U
hf : ∀ z ∈ closedBall c r, f z ≠ 0
V : Set ℂ
h1 : V ⊆ U
h2 : IsOpen V
h3 : closedBall c r ⊆ V
h4 : ∀ z ∈ V, f z ≠ 0
⊢ cindex c r f = 0
no goals