rw [hgz₀, zero_add] at hgz
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c : ℂ
r✝ : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
p : FormalMultilinearSeries ℂ ℂ ℂ
h17 : p ≠ 0
h6 : 2 ≤ FormalMultilinearSeries.order p
r : ℝ
h7 : r > 0
h18 : ∀ (ε : ℂ), DifferentiableOn ℂ (fun z => g z + ε) U
h19 : TendstoLocallyUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
h24 : FormalMultilinearSeries.order p ≠ 0
ε : ℂ
hε : ε ∈ {0}ᶜ
z : ℂ
hgz : g z + ε = 0
hz₀ : z ∈ U
hgz₀ : g z = 0
hp : HasFPowerSeriesAt g p z
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z, g z ≠ 0
h✝ : deriv g z = 0
h8 : cindex z r g = ↑(FormalMultilinearSeries.order p)
h14 : ∀ z_1 ∈ closedBall z r, z_1 ≠ z → deriv g z_1 ≠ 0
h21 : ∀ z_1 ∈ closedBall z r, z_1 ≠ z → g z_1 ≠ 0
h20 : closedBall z r ⊆ U
h22 : ∀ z_1 ∈ sphere z r, g z_1 ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → ∃ z_1 ∈ ball z r, g z_1 + x = 0
h : ε ∈ {0}ᶜ → ∃ z_1 ∈ ball z r, g z_1 + ε = 0
hz : z ∈ ball z r
⊢ False
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c : ℂ
r✝ : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
p : FormalMultilinearSeries ℂ ℂ ℂ
h17 : p ≠ 0
h6 : 2 ≤ FormalMultilinearSeries.order p
r : ℝ
h7 : r > 0
h18 : ∀ (ε : ℂ), DifferentiableOn ℂ (fun z => g z + ε) U
h19 : TendstoLocallyUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
h24 : FormalMultilinearSeries.order p ≠ 0
ε : ℂ
hε : ε ∈ {0}ᶜ
z : ℂ
hgz : ε = 0
hz₀ : z ∈ U
hgz₀ : g z = 0
hp : HasFPowerSeriesAt g p z
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z, g z ≠ 0
h✝ : deriv g z = 0
h8 : cindex z r g = ↑(FormalMultilinearSeries.order p)
h14 : ∀ z_1 ∈ closedBall z r, z_1 ≠ z → deriv g z_1 ≠ 0
h21 : ∀ z_1 ∈ closedBall z r, z_1 ≠ z → g z_1 ≠ 0
h20 : closedBall z r ⊆ U
h22 : ∀ z_1 ∈ sphere z r, g z_1 ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → ∃ z_1 ∈ ball z r, g z_1 + x = 0
h : ε ∈ {0}ᶜ → ∃ z_1 ∈ ball z r, g z_1 + ε = 0
hz : z ∈ ball z r
⊢ False