have h6 : 2 ≤ p.order := two_le_order_of_deriv_eq_zero hp h17 hgz₀ h
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
⊢ False
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
⊢ False