case pos =>
  subst_vars
  obtain ⟨R, hR, hf⟩ := Metric.eventually_nhds_iff.mp (hp.locally_zero_iff.mpr rfl)
  refine ⟨R, hR, λ r hr => ?_⟩
  simp [cindex, Real.pi_ne_zero, Complex.I_ne_zero]
  have : Set.EqOn (λ z => deriv f z / f z) 0 (sphere z₀ r) := by
    intro z hz
    simp
    right
    apply hf
    rw [hz.symm.symm]
    exact hr.2
  rw [circleIntegral.integral_congr hr.1.le this]
  simp [circleIntegral]
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p = 0
⊢ ∃ R > 0, ∀ r ∈ Set.Ioo 0 R, cindex z₀ r f = ↑(FormalMultilinearSeries.order p)
no goals