-- 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.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
⊢ ‖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:
have S₂ : ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4 :=
  calc
    _ ≤ ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ε / 4 / M * ‖z‖ ^ i := by
      gcongr with i hi
      have := hB₁ (i + 1) (by linarith only [(mem_Ico.mp hi).1])
      rw [norm_sub_rev] at this
      exact this.le
    _ = ‖1 - z‖ * (ε / 4 / M) * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖z‖ ^ i := by
      rw [← mul_sum, ← mul_assoc]
    _ ≤ ‖1 - z‖ * (ε / 4 / M) * ∑' i, ‖z‖ ^ i := by
      gcongr
      exact sum_le_tsum _ (fun _ _ ↦ by positivity)
        (summable_geometric_of_lt_one (by positivity) zn)
    _ = ‖1 - z‖ * (ε / 4 / M) / (1 - ‖z‖) := by
      rw [tsum_geometric_of_lt_one (by positivity) zn, ← div_eq_mul_inv]
    _ < M * (1 - ‖z‖) * (ε / 4 / M) / (1 - ‖z‖) := by gcongr; linarith only [zn]
    _ = _ := by
      rw [← mul_rotate, mul_div_cancel_right₀ _ (by linarith only [zn]),
        div_mul_cancel₀ _ (by linarith only [hM])]

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

Proof state:
case 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
i✝ : ℕ
a✝ : i✝ ∈ range B₁
⊢ ‖l - s (i✝ + 1)‖ * ‖z‖ ^ i✝ ≤ ‖l - s (i✝ + 1)‖

Tactic:
nth_rw 3 [← mul_one ‖_‖]

Result:
case 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
i✝ : ℕ
a✝ : i✝ ∈ range B₁
⊢ ‖l - s (i✝ + 1)‖ * ‖z‖ ^ i✝ ≤ ‖l - s (i✝ + 1)‖ * 1

Proof state:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
⊢ Tendsto (fun z => ∑' (n : ℕ), f n * z ^ n) (𝓝[stolzSet M] 1) (𝓝 l)

Tactic:
rcases le_or_lt M 1 with hM | hM

Result:
case inl
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : M ≤ 1
⊢ Tendsto (fun z => ∑' (n : ℕ), f n * z ^ n) (𝓝[stolzSet M] 1) (𝓝 l)

case inr
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
⊢ 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 : ‖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
⊢ M * (1 - ‖z‖) * (ε / 4 / M) / (1 - ‖z‖) = ε / 4

Tactic:
rw [← mul_rotate, mul_div_cancel_right₀ _ (by linarith only [zn]),
  div_mul_cancel₀ _ (by linarith only [hM])]

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
⊢ M ≠ 0

Tactic:
linarith only [hM]

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

Tactic:
simp

Result:
no goals

Proof state:
case inr
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
⊢ Tendsto (fun z => ∑' (n : ℕ), f n * z ^ n) (𝓝[stolzSet M] 1) (𝓝 l)

Tactic:
let s := fun n ↦ ∑ i ∈ range n, f i

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