-- Mathlib/Analysis/Analytic/Basic.lean
theorem hasFPowerSeriesAt_iff :
    HasFPowerSeriesAt f p z₀ ↔ ∀ᶠ z in 𝓝 0, HasSum (fun n => z ^ n • p.coeff n) (f (z₀ + z))

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
⊢ HasFPowerSeriesAt f p z₀ ↔ ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • p.coeff n) (f (z₀ + z))

Tactic:
refine ⟨fun ⟨r, _, r_pos, h⟩ =>
  eventually_of_mem (EMetric.ball_mem_nhds 0 r_pos) fun _ => by simpa using h, ?_⟩

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
⊢ (∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • p.coeff n) (f (z₀ + z))) → HasFPowerSeriesAt f p z₀

Proof state:
case intro.intro.refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
h : ∀ ⦃y : 𝕜⦄, dist y 0 < r → HasSum (fun n => y ^ n • p.coeff n) (f (z₀ + y))
⊢ 0 < p.radius

Tactic:
obtain ⟨z, z_pos, le_z⟩ := NormedField.exists_norm_lt 𝕜 r_pos.lt

Result:
case intro.intro.refine_1.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
h : ∀ ⦃y : 𝕜⦄, dist y 0 < r → HasSum (fun n => y ^ n • p.coeff n) (f (z₀ + y))
z : 𝕜
z_pos : 0 < ‖z‖
le_z : ‖z‖ < r
⊢ 0 < p.radius

Proof state:
case intro.intro.refine_1.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
h : ∀ ⦃y : 𝕜⦄, dist y 0 < r → HasSum (fun n => y ^ n • p.coeff n) (f (z₀ + y))
z : 𝕜
z_pos : 0 < ‖z‖
le_z : ‖z‖ < r
this : ↑‖z‖₊ ≤ p.radius
⊢ 0 < ‖z‖₊

Tactic:
exact zero_lt_iff.mpr (nnnorm_ne_zero_iff.mpr (norm_pos_iff.mp z_pos))

Result:
no goals

Proof state:
case intro.intro.refine_1.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
h : ∀ ⦃y : 𝕜⦄, dist y 0 < r → HasSum (fun n => y ^ n • p.coeff n) (f (z₀ + y))
z : 𝕜
z_pos : 0 < ‖z‖
le_z : ‖z‖ < r
⊢ 0 < p.radius

Tactic:
have : (‖z‖₊ : ENNReal) ≤ p.radius := by
  simp only [dist_zero_right] at h
  apply FormalMultilinearSeries.le_radius_of_tendsto
  convert tendsto_norm.comp (h le_z).summable.tendsto_atTop_zero
  simp [norm_smul, mul_comm]

Result:
case intro.intro.refine_1.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
h : ∀ ⦃y : 𝕜⦄, dist y 0 < r → HasSum (fun n => y ^ n • p.coeff n) (f (z₀ + y))
z : 𝕜
z_pos : 0 < ‖z‖
le_z : ‖z‖ < r
this : ↑‖z‖₊ ≤ p.radius
⊢ 0 < p.radius

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
h : ∀ ⦃y : 𝕜⦄, dist y 0 < r → HasSum (fun n => y ^ n • p.coeff n) (f (z₀ + y))
⊢ HasFPowerSeriesAt f p z₀

Tactic:
refine ⟨p.radius ⊓ r.toNNReal, by simp, ?_, ?_⟩

Result:
case intro.intro.refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
h : ∀ ⦃y : 𝕜⦄, dist y 0 < r → HasSum (fun n => y ^ n • p.coeff n) (f (z₀ + y))
⊢ 0 < p.radius ⊓ ↑r.toNNReal

case intro.intro.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
h : ∀ ⦃y : 𝕜⦄, dist y 0 < r → HasSum (fun n => y ^ n • p.coeff n) (f (z₀ + y))
⊢ ∀ {y : 𝕜}, y ∈ EMetric.ball 0 (p.radius ⊓ ↑r.toNNReal) → HasSum (fun n => (p n) fun x => y) (f (z₀ + y))

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
z : 𝕜
z_pos : 0 < ‖z‖
le_z : ‖z‖ < r
h : ∀ ⦃y : 𝕜⦄, ‖y‖ < r → HasSum (fun n => y ^ n • p.coeff n) (f (z₀ + y))
⊢ ↑‖z‖₊ ≤ p.radius

Tactic:
apply FormalMultilinearSeries.le_radius_of_tendsto

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
z : 𝕜
z_pos : 0 < ‖z‖
le_z : ‖z‖ < r
h : ∀ ⦃y : 𝕜⦄, ‖y‖ < r → HasSum (fun n => y ^ n • p.coeff n) (f (z₀ + y))
⊢ Tendsto (fun n => ‖p n‖ * ↑‖z‖₊ ^ n) atTop (𝓝 ?l)

case l
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
z : 𝕜
z_pos : 0 < ‖z‖
le_z : ‖z‖ < r
h : ∀ ⦃y : 𝕜⦄, ‖y‖ < r → HasSum (fun n => y ^ n • p.coeff n) (f (z₀ + y))
⊢ ℝ

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
h : ∀ ⦃y : 𝕜⦄, dist y 0 < r → HasSum (fun n => y ^ n • p.coeff n) (f (z₀ + y))
⊢ p.radius ⊓ ↑r.toNNReal ≤ p.radius

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro.refine_1.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
h : ∀ ⦃y : 𝕜⦄, dist y 0 < r → HasSum (fun n => y ^ n • p.coeff n) (f (z₀ + y))
z : 𝕜
z_pos : 0 < ‖z‖
le_z : ‖z‖ < r
this : ↑‖z‖₊ ≤ p.radius
⊢ 0 < ↑‖z‖₊

Tactic:
simp only [ENNReal.coe_pos]

Result:
case intro.intro.refine_1.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
h : ∀ ⦃y : 𝕜⦄, dist y 0 < r → HasSum (fun n => y ^ n • p.coeff n) (f (z₀ + y))
z : 𝕜
z_pos : 0 < ‖z‖
le_z : ‖z‖ < r
this : ↑‖z‖₊ ≤ p.radius
⊢ 0 < ‖z‖₊