Power series of analytic function

Stream: Is there code for X?

[Michail Karatarakis]

I have a function that is AnalyticAt ℂ . How do I define the power series for it and which lemma shows that that series converges to the function? Do I need to define it myself or is it already there?

[Yakov Pechersky]

It is the property of AnalyticAt 𝕜 f x = ∃ (p : FormalMultilinearSeries 𝕜 E F), HasFPowerSeriesAt f p x.
So you could do, for h : AnalyticAt K f x, h.choose for the power series, and h.choose_spec for the convergence proof.