classical
have h1 : p.coeff 1 = 0 := by simpa only [hg'] using hgp.deriv.symm
have h2 : p 0 = 0 := by ext1 x; simpa only [hg] using hgp.coeff_zero x
have h3 : p 1 = 0 := by ext1; simp [h1]
rw [FormalMultilinearSeries.order_eq_find' hp, Nat.le_find_iff]
intro n hn
cases n
case zero => simp [h2]
case succ n =>
  cases n
  case zero => simpa using h3
  case succ => linarith
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hgp : HasFPowerSeriesAt g p z₀
hp : p ≠ 0
hg : g z₀ = 0
hg' : deriv g z₀ = 0
⊢ 2 ≤ FormalMultilinearSeries.order p
no goals