Theorem: HasFPowerSeriesAt.eventually_differentiable_at (RMT4/cindex.lean)

State before:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
f : ℂ → E
z₀ : ℂ
hp : HasFPowerSeriesAt f p z₀
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, DifferentiableAt ℂ f z
Tactic:
obtain ⟨r, hp⟩ := hp
State after:
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
f : ℂ → E
z₀ : ℂ
r : ENNReal
hp : HasFPowerSeriesOnBall f p z₀ r
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, DifferentiableAt ℂ f z

State before:
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
f : ℂ → E
z₀ : ℂ
r : ENNReal
hp : HasFPowerSeriesOnBall f p z₀ r
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, DifferentiableAt ℂ f z
Tactic:
exact hp.differentiableOn.eventually_differentiableAt (EMetric.ball_mem_nhds _ hp.r_pos)
State after:
no goals