simp [circleIntegral]
case intro.intro
f g : ℂ → ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f 0 z₀
R : ℝ
hR : R > 0
hf : ∀ ⦃y : ℂ⦄, dist y z₀ < R → f y = 0
r : ℝ
hr : r ∈ Set.Ioo 0 R
this : Set.EqOn (fun z => deriv f z / f z) 0 (sphere z₀ r)
⊢ (∮ (z : ℂ) in C(z₀, r), 0 z) = 0
no goals