refine ContinuousAt.eventually_ne ?h (hp.iterate_dslope_fslope_ne_zero h)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
n : ℕ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, (swap dslope z₀)^[FormalMultilinearSeries.order p] f z ≠ 0
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
n : ℕ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
⊢ ContinuousAt (fun z => (swap dslope z₀)^[FormalMultilinearSeries.order p] f z) z₀