simp only [eventually_nhds_iff_eventually_closed_ball] at e2 e3 e4
case 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
q : FormalMultilinearSeries ℂ ℂ ℂ
hq : HasFPowerSeriesAt (deriv g) q z₀
h26 : q ≠ 0
e1 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
e4 : ∀ᶠ (x : ℂ) in 𝓝 z₀, x ∈ U
e2 : ∀ᶠ (x : ℂ) in 𝓝 z₀, x ≠ z₀ → g x ≠ 0
e3 : ∀ᶠ (x : ℂ) in 𝓝 z₀, x ≠ z₀ → deriv g x ≠ 0
⊢ ∃ r > 0,
    cindex z₀ r g = ↑(FormalMultilinearSeries.order p) ∧
      (∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0) ∧ (∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0) ∧ closedBall z₀ r ⊆ U
case 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
q : FormalMultilinearSeries ℂ ℂ ℂ
hq : HasFPowerSeriesAt (deriv g) q z₀
h26 : q ≠ 0
e1 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
e2 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, ∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0
e3 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, ∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0
e4 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, ∀ z ∈ closedBall z₀ r, z ∈ U
⊢ ∃ r > 0,
    cindex z₀ r g = ↑(FormalMultilinearSeries.order p) ∧
      (∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0) ∧ (∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0) ∧ closedBall z₀ r ⊆ U