obtain ⟨p, hp⟩ := h1
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
h1 : AnalyticAt ℂ f z₀
h2 : f z₀ = 0
h3 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
⊢ ∀ᶠ (r : ℝ) in 𝓝[>] 0, cindex z₀ r f ≠ 0
case intro
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
h2 : f z₀ = 0
h3 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
⊢ ∀ᶠ (r : ℝ) in 𝓝[>] 0, cindex z₀ r f ≠ 0