-- 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 h.e'_4
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
S₂ : ‖1 - z‖ * ∑ i ∈ Ico B₁ (B₁ ⊔ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
⊢ ε / 2 = ε / 4 + ε / 4

Tactic:
linarith only

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
⊢ ‖(1 - z) * ∑ i ∈ range (B₁ ⊔ B₂), (l - s (i + 1)) * z ^ i‖ =
    ‖(1 - z) * ∑ i ∈ range B₁, (l - s (i + 1)) * z ^ i + (1 - z) * ∑ i ∈ Ico B₁ (B₁ ⊔ B₂), (l - s (i + 1)) * z ^ i‖

Tactic:
rw [← mul_add, sum_range_add_sum_Ico _ (le_max_left B₁ B₂)]

Result:
no goals

Proof state:
case right.intro.calc.step
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
S₂ : ‖1 - z‖ * ∑ i ∈ Ico B₁ (B₁ ⊔ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
⊢ ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i + ‖1 - z‖ * ∑ i ∈ Ico B₁ (B₁ ⊔ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i <
    ε / 2

Tactic:
convert add_lt_add S₁ S₂ using 1

Result:
case h.e'_4
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
S₂ : ‖1 - z‖ * ∑ i ∈ Ico B₁ (B₁ ⊔ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
⊢ ε / 2 = ε / 4 + ε / 4

Proof state:
case inr
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
⊢ Tendsto (fun z => ∑' (n : ℕ), f n * z ^ n) (𝓝[stolzSet M] 1) (𝓝 l)

Tactic:
let g := fun z ↦ ∑' n, f n * z ^ n

Result:
case inr
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
⊢ Tendsto (fun z => ∑' (n : ℕ), f n * z ^ n) (𝓝[stolzSet M] 1) (𝓝 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 : ‖1 - z‖ < ε / 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
⊢ 0 < F + 1

Tactic:
positivity

Result:
no goals

Proof state:
case right.intro
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₂ : ∀ n ≥ B₂, ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range n, (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
⊢ ‖∑' (n : ℕ), f n * z ^ n - l‖ < ε

Tactic:
replace hB₂ := hB₂ (max B₁ B₂) (by simp)

Result:
case right.intro
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
⊢ ‖∑' (n : ℕ), f n * z ^ n - l‖ < ε

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 : ‖∑ i ∈ range (i + 1), f i - l‖ < ε / 4 / M
⊢ ‖l - s (i + 1)‖ ≤ ε / 4 / M

Tactic:
rw [norm_sub_rev] at this

Result:
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