no goals
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.469661
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → F
p pf pg : FormalMultilinearSeries 𝕜 E F
x : E
r r' : ℝ≥0∞
hf : HasFPowerSeriesOnBall f 0 x r
⊢ ∀ᶠ (z : E) in 𝓝 x, f z = 0
filter_upwards [hf.eventually_hasSum_sub] with z hz using hz.unique hasSum_zero