simpa only [hg] using hgp.coeff_zero x
case H
ι : 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
h1 : FormalMultilinearSeries.coeff p 1 = 0
x : Fin 0 → ℂ
⊢ (p 0) x = 0 x
no goals