rw [hp.coeff_zero, hz₀]
case H
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
hz₀ : f z₀ = 0
h : ¬p = 0
x✝ : Fin 0 → ℂ
⊢ (p 0) x✝ = 0 x✝
case H
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
hz₀ : f z₀ = 0
h : ¬p = 0
x✝ : Fin 0 → ℂ
⊢ 0 = 0 x✝