-- Mathlib/Analysis/Complex/AbelLimit.lean
theorem tendsto_tsum_powerSeries_nhdsWithin_stolzSet
    (h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)) {M : ℝ} :
    Tendsto (fun z ↦ ∑' n, f n * z ^ n) (𝓝[stolzSet M] 1) (𝓝 l)

Proof state:
case right
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i
g : ℂ → ℂ := fun z => ∑' (n : ℕ), f n * z ^ n
hm : ∀ ε > 0, ∃ N, ∀ n ≥ N, ‖∑ i ∈ range n, f i - l‖ < ε
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
F : ℝ := ∑ i ∈ range B₁, ‖l - s (i + 1)‖
z : ℂ
zn : ‖z‖ < 1
zm : ‖1 - z‖ < M * (1 - ‖z‖)
zd : ‖z - 1‖ < ε / 4 / (F + 1)
p :
  Tendsto (fun n => (1 - z) * ∑ i ∈ range n, (l - ∑ j ∈ range (i + 1), f j) * z ^ i) atTop
    (𝓝 (l - ∑' (n : ℕ), f n * z ^ n))
⊢ ‖∑' (n : ℕ), f n * z ^ n - l‖ < ε

Tactic:
simp_rw [Metric.tendsto_atTop, dist_eq_norm, norm_sub_rev] at p

Result:
case right
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i
g : ℂ → ℂ := fun z => ∑' (n : ℕ), f n * z ^ n
hm : ∀ ε > 0, ∃ N, ∀ n ≥ N, ‖∑ i ∈ range n, f i - l‖ < ε
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
F : ℝ := ∑ i ∈ range B₁, ‖l - s (i + 1)‖
z : ℂ
zn : ‖z‖ < 1
zm : ‖1 - z‖ < M * (1 - ‖z‖)
zd : ‖z - 1‖ < ε / 4 / (F + 1)
p :
  ∀ ε > 0,
    ∃ N, ∀ n ≥ N, ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range n, (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε
⊢ ‖∑' (n : ℕ), f n * z ^ n - l‖ < ε

Proof state:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i
g : ℂ → ℂ := fun z => ∑' (n : ℕ), f n * z ^ n
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
F : ℝ := ∑ i ∈ range B₁, ‖l - s (i + 1)‖
z : ℂ
zn : ‖z‖ < 1
zm : ‖1 - z‖ < M * (1 - ‖z‖)
zd : ‖z - 1‖ < ε / 4 / (F + 1)
B₂ : ℕ
hB₂ : ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range (B₁ ⊔ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
this : ‖(1 - z) * ∑ i ∈ range (B₁ ⊔ B₂), (l - s (i + 1)) * z ^ i‖ < ε / 2
⊢ ‖∑' (n : ℕ), f n * z ^ n - l‖ < ε

Tactic:
calc
  _ = ‖l - g z‖ := by rw [norm_sub_rev]
  _ = ‖l - g z - (1 - z) * ∑ i ∈ range (max B₁ B₂), (l - s (i + 1)) * z ^ i +
      (1 - z) * ∑ i ∈ range (max B₁ B₂), (l - s (i + 1)) * z ^ i‖ := by rw [sub_add_cancel _]
  _ ≤ ‖l - g z - (1 - z) * ∑ i ∈ range (max B₁ B₂), (l - s (i + 1)) * z ^ i‖ +
      ‖(1 - z) * ∑ i ∈ range (max B₁ B₂), (l - s (i + 1)) * z ^ i‖ := norm_add_le _ _
  _ < ε / 2 + ε / 2 := add_lt_add hB₂ this
  _ = _ := add_halves ε

Result:
no goals

Proof state:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i
g : ℂ → ℂ := fun z => ∑' (n : ℕ), f n * z ^ n
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
F : ℝ := ∑ i ∈ range B₁, ‖l - s (i + 1)‖
z : ℂ
zn : ‖z‖ < 1
zm : ‖1 - z‖ < M * (1 - ‖z‖)
zd : ‖z - 1‖ < ε / 4 / (F + 1)
B₂ : ℕ
hB₂ : ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range (B₁ ⊔ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
S₁ : ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
⊢ ‖1 - z‖ * (ε / 4 / M) * ∑' (i : ℕ), ‖z‖ ^ i = ‖1 - z‖ * (ε / 4 / M) / (1 - ‖z‖)

Tactic:
rw [tsum_geometric_of_lt_one (by positivity) zn, ← div_eq_mul_inv]

Result:
no goals

Proof state:
case h.h.h
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i
g : ℂ → ℂ := fun z => ∑' (n : ℕ), f n * z ^ n
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
F : ℝ := ∑ i ∈ range B₁, ‖l - s (i + 1)‖
z : ℂ
zn : ‖z‖ < 1
zm : ‖1 - z‖ < M * (1 - ‖z‖)
zd : ‖z - 1‖ < ε / 4 / (F + 1)
B₂ : ℕ
hB₂ : ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range (B₁ ⊔ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
S₁ : ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
i : ℕ
hi : i ∈ Ico B₁ (B₁ ⊔ B₂)
this : ‖l - ∑ i ∈ range (i + 1), f i‖ < ε / 4 / M
⊢ ‖l - s (i + 1)‖ ≤ ε / 4 / M

Tactic:
exact this.le

Result:
no goals