have h9 : ∀ᶠ ε in 𝓝[≠] 0, cindex z₀ r (λ z => g z + ε) = 1 := by
  have h24 : p.order ≠ 0 := by linarith
  have := hurwitz2 hU (eventually_of_forall h18) h19 h7 h20 h22 (by simp [h8, h24])
  simp only [eventually_nhdsWithin_iff] at this ⊢
  filter_upwards [this] with ε h hε
  obtain ⟨z, hz, hgz⟩ := h hε
  have e1 : z ≠ z₀ := by rintro rfl; rw [hgz₀, zero_add] at hgz; exact hε hgz
  have e2 : deriv (λ z => g z + ε) z ≠ 0 := by simpa using h14 z (ball_subset_closedBall hz) e1
  refine crucial hU h20 hz (h18 ε) hgz e2 (λ w hw hwz => ?_)
  contrapose! hwz
  exact hi (h20 hw) ((ball_subset_closedBall.trans h20) hz) (add_right_cancel (hwz.trans hgz.symm))
case intro.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r✝ : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
r : ℝ
h7 : r > 0
h8 : cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
h14 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0
h21 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0
h20 : closedBall z₀ r ⊆ U
h22 : ∀ z ∈ sphere z₀ r, g z ≠ 0
h18 : ∀ (ε : ℂ), DifferentiableOn ℂ (fun z => g z + ε) U
h19 : TendstoLocallyUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
⊢ False
case intro.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r✝ : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
r : ℝ
h7 : r > 0
h8 : cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
h14 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0
h21 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0
h20 : closedBall z₀ r ⊆ U
h22 : ∀ z ∈ sphere z₀ r, g z ≠ 0
h18 : ∀ (ε : ℂ), DifferentiableOn ℂ (fun z => g z + ε) U
h19 : TendstoLocallyUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
h9 : ∀ᶠ (ε : ℂ) in 𝓝[≠] 0, (cindex z₀ r fun z => g z + ε) = 1
⊢ False