Theorem: cindex_pos (RMT4/hurwitz.lean)

State before:
ι : 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
Tactic:
obtain ⟨p, hp⟩ := h1
State after:
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

State before:
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
Tactic:
filter_upwards [cindex_eventually_eq_order hp] with r h4
State after:
case h
ι : 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 : ℝ
h4 : cindex z₀ r f = ↑(FormalMultilinearSeries.order p)
⊢ cindex z₀ r f ≠ 0

State before:
case h
ι : 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 : ℝ
h4 : cindex z₀ r f = ↑(FormalMultilinearSeries.order p)
⊢ cindex z₀ r f ≠ 0
Tactic:
simpa [h4, order_eq_zero_iff hp h2] using h3.frequently.filter_mono nhdsWithin_le_nhds
State after:
no goals