rw [eventually_nhdsWithin_iff, Metric.eventually_nhds_iff]
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f p z₀
⊢ ∀ᶠ (r : ℝ) in 𝓝[>] 0, cindex z₀ r f = ↑(FormalMultilinearSeries.order p)
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f p z₀
⊢ ∃ ε > 0, ∀ ⦃y : ℝ⦄, dist y 0 < ε → y ∈ Set.Ioi 0 → cindex z₀ y f = ↑(FormalMultilinearSeries.order p)