obtain ⟨R, hR, hf⟩ := Metric.eventually_nhds_iff.mp (hp.locally_zero_iff.mpr rfl)
f g : ℂ → ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f 0 z₀
⊢ ∃ R > 0, ∀ r ∈ Set.Ioo 0 R, cindex z₀ r f = ↑(FormalMultilinearSeries.order 0)
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 > 0, ∀ r ∈ Set.Ioo 0 R, cindex z₀ r f = ↑(FormalMultilinearSeries.order 0)