awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
g : (z : ℂ) → ℂ := 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 (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
h₁ : norm (E := ℂ) (∑ i ∈ range B₁, (l - s (i + 1)) * z ^ i) ≤ ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i
h₂ :
  norm (E := ℂ) (∑ i ∈ Ico B₁ (max B₁ B₂), (l - s (i + 1)) * z ^ i) ≤
    ∑ i ∈ Ico B₁ (max B₁ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i
⊢ ‖1 - z‖ * norm (E := ℂ) (∑ i ∈ range B₁, (l - s (i + 1)) * z ^ i) +
      ‖1 - z‖ * norm (E := ℂ) (∑ i ∈ Ico B₁ (max B₁ B₂), (l - s (i + 1)) * z ^ i) ≤
    ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i + ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
g : (z : ℂ) → ℂ := 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 (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
h₁ : norm (E := ℂ) (∑ i ∈ range B₁, (l - s (i + 1)) * z ^ i) ≤ ∑ x ∈ range B₁, ‖l - s (x + 1)‖ * ‖z ^ x‖
h₂ : norm (E := ℂ) (∑ i ∈ range B₁, (l - s (i + 1)) * z ^ i) ≤ ∑ x ∈ range B₁, ‖(l - s (x + 1)) * z ^ x‖
⊢ norm (E := ℂ) (∑ i ∈ range B₁, (l - s (i + 1)) * z ^ i) ≤ ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i

Tactic:
simp_rw [← norm_pow, ← norm_mul, norm_sum_le]

Premises used: norm_pow, norm_mul, norm_sum_le
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
g : (z : ℂ) → ℂ := 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 (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
h₂ :
  norm (E := ℂ) (∑ i ∈ Ico B₁ (max B₁ B₂), (l - s (i + 1)) * z ^ i) ≤
    ∑ x ∈ Ico B₁ (max B₁ B₂), ‖l - s (x + 1)‖ * ‖z ^ x‖
h₃ :
  norm (E := ℂ) (∑ i ∈ Ico B₁ (max B₁ B₂), (l - s (i + 1)) * z ^ i) ≤
    ∑ x ∈ Ico B₁ (max B₁ B₂), ‖(l - s (x + 1)) * z ^ x‖
⊢ norm (E := ℂ) (∑ i ∈ Ico B₁ (max B₁ B₂), (l - s (i + 1)) * z ^ i) ≤
    ∑ i ∈ Ico B₁ (max B₁ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i

Tactic:
simp_rw [← norm_pow, ← norm_mul, norm_sum_le]

Premises used: norm_pow, norm_mul, norm_sum_le
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
g : (z : ℂ) → ℂ := 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 (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
right :
  ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i + ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i <
    ε / 2
⊢ ‖(1 - z) * ∑ i ∈ range (max B₁ B₂), (l - s (i + 1)) * z ^ i‖ < ε / 2

Tactic:
calc
    _ = ‖(1 - z) * ∑ i ∈ range B₁, (l - s (i + 1)) * z ^ i +
        (1 - z) * ∑ i ∈ Ico B₁ (max B₁ B₂), (l - s (i + 1)) * z ^ i‖ := by
      rw [← mul_add, sum_range_add_sum_Ico _ (le_max_left B₁ B₂)]
    _ ≤ ‖(1 - z) * ∑ i ∈ range B₁, (l - s (i + 1)) * z ^ i‖ +
        ‖(1 - z) * ∑ i ∈ Ico B₁ (max B₁ B₂), (l - s (i + 1)) * z ^ i‖ := norm_add_le _ _
    _ = ‖1 - z‖ * ‖∑ i ∈ range B₁, (l - s (i + 1)) * z ^ i‖ +
        ‖1 - z‖ * ‖∑ i ∈ Ico B₁ (max B₁ B₂), (l - s (i + 1)) * z ^ i‖ := by
      rw [norm_mul, norm_mul]
    _ ≤ ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i +
        ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i := by
      gcongr <;> simp_rw [← norm_pow, ← norm_mul, norm_sum_le]

Premises used: HSub.hSub, norm_add_le, Finset.Ico, Finset.range, Max.max, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
g : (z : ℂ) → ℂ := 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 (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
hbc : ∀ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i ≤ ‖l - s (i + 1)‖
⊢ ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i ≤ ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
g : (z : ℂ) → ℂ := 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 (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
i : ℕ
h_1 : i ∈ range B₁
hbc : ‖l - s (i + 1)‖ * ‖z‖ ^ i ≤ ‖l - s (i + 1)‖ * 1
⊢ ‖l - s (i + 1)‖ * ‖z‖ ^ i ≤ ‖l - s (i + 1)‖

Tactic:
nth_rw 3 [← mul_one ‖_‖]

Premises used: Norm.norm, mul_one
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
g : (z : ℂ) → ℂ := 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 (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
i : ℕ
h_1 : i ∈ range B₁
hbc : ‖z‖ ^ i ≤ 1
⊢ ‖l - s (i + 1)‖ * ‖z‖ ^ i ≤ ‖l - s (i + 1)‖ * 1

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
g : (z : ℂ) → ℂ := 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 (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
i : ℕ
h_1 : i ∈ range B₁
⊢ ‖z‖ ^ i ≤ 1

Tactic:
pow_le_one₀ (norm_nonneg _) zn.le

Premises used: LT.lt.le, norm_nonneg, pow_le_one₀
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
g : (z : ℂ) → ℂ := 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 (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
i : ℕ
h_1 : i ∈ range B₁
⊢ ‖z‖ ^ i ≤ 1

Tactic:
exact pow_le_one₀ (norm_nonneg _) zn.le

Premises used: LT.lt.le, norm_nonneg, pow_le_one₀
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
g : (z : ℂ) → ℂ := 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 (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
hbc : ∑ i ∈ range B₁, ‖l - s (i + 1)‖ ≤ F + 1
⊢ ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ ≤ ‖1 - z‖ * (F + 1)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
g : (z : ℂ) → ℂ := 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 (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
linarith : F + 1 < ∑ i ∈ range B₁, ‖l - s (i + 1)‖ → -1 + (F + 1 - ∑ i ∈ range B₁, ‖l - s (i + 1)‖) = 0
⊢ ∑ i ∈ range B₁, ‖l - s (i + 1)‖ ≤ F + 1

Tactic:
linarith only
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
g : (z : ℂ) → ℂ := 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 (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
⊢ 0 < F + 1

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
g : (z : ℂ) → ℂ := 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 (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
rwa :
  ∀ (zd : ‖1 - z‖ < ε / 4 / (F + 1)) (B₂ : ℕ)
    (hB₂ :
      ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ <
        ε / 2),
    ‖1 - z‖ * (F + 1) < ε / 4
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (zd : ‖1 - z‖ * (F + 1) < ε / 4) (B₂ : ℕ)
    (hB₂ :
      ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ <
        ε / 2),
    ‖1 - z‖ * (F + 1) < ε / 4
⊢ ‖1 - z‖ * (F + 1) < ε / 4

Tactic:
rwa [norm_sub_rev, lt_div_iff₀ (by positivity)] at zd

Premises used: lt_div_iff₀, norm_sub_rev
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
g : (z : ℂ) → ℂ := 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 (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
⊢ ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4

Tactic:
have S₁ : ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4 :=
    calc
      _ ≤ ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ := by
        gcongr; nth_rw 3 [← mul_one ‖_‖]
        gcongr; exact pow_le_one₀ (norm_nonneg _) zn.le
      _ ≤ ‖1 - z‖ * (F + 1) := by gcongr; linarith only
      _ < _ := by rwa [norm_sub_rev, lt_div_iff₀ (by positivity)] at zd
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
g : (z : ℂ) → ℂ := 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 (max 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
hbc : ∀ (i : ℕ) (hi : i ∈ Ico B₁ (max B₁ B₂)), ‖l - s (i + 1)‖ ≤ ε / 4 / M
⊢ ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i ≤
    ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ε / 4 / M * ‖z‖ ^ i

Tactic:
gcongr with i hi
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
g : (z : ℂ) → ℂ := 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 (max 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₁ (max B₁ B₂)
linarith :
  i + 1 < B₁ →
    HMul.hMul (α := ℤ) 2 (-1) + (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1 + 1 - (↑B₁ : ℤ)) +
        HSub.hSub (α := ℤ) (↑B₁ : ℤ) (↑i : ℤ) =
      0
linarith₁ : i + 1 < B₁ → GT.gt (α := ℤ) 2 0
⊢ i + 1 ≥ B₁

Tactic:
linarith only [(mem_Ico.mp hi).1]

Premises used: And.left, Iff.mp, Finset.mem_Ico
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
g : (z : ℂ) → ℂ := 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 (max 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₁ (max B₁ B₂)
⊢ ‖∑ i ∈ range (i + 1), f i - l‖ < ε / 4 / M

Tactic:
have := hB₁ (i + 1) (by linarith only [(mem_Ico.mp hi).1])
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
g : (z : ℂ) → ℂ := 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 (max 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₁ (max B₁ B₂)
this : ‖∑ i ∈ range (i + 1), f i - l‖ < ε / 4 / M
⊢ ‖l - ∑ i ∈ range (i + 1), f i‖ < ε / 4 / M

Tactic:
rw [norm_sub_rev] at this

Premises used: norm_sub_rev
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
g : (z : ℂ) → ℂ := 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 (max 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₁ (max B₁ B₂)
this : ‖l - ∑ i ∈ range (i + 1), f i‖ < ε / 4 / M
⊢ ‖l - s (i + 1)‖ ≤ ε / 4 / M

Tactic:
this.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
g : (z : ℂ) → ℂ := 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 (max 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₁ (max B₁ B₂)
this : ‖l - ∑ i ∈ range (i + 1), f i‖ < ε / 4 / M
⊢ ‖l - s (i + 1)‖ ≤ ε / 4 / M

Tactic:
exact this.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
g : (z : ℂ) → ℂ := 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 (max 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
rw :
  ‖1 - z‖ * (ε / 4 / M * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖z‖ ^ i) = ‖1 - z‖ * (ε / 4 / M) * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖z‖ ^ i
rw₁ rw₂ :
  ‖1 - z‖ * (ε / 4 / M) * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖z‖ ^ i = ‖1 - z‖ * (ε / 4 / M) * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖z‖ ^ i
⊢ ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ε / 4 / M * ‖z‖ ^ i = ‖1 - z‖ * (ε / 4 / M) * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖z‖ ^ i

Tactic:
rw [← mul_sum, ← mul_assoc]

Premises used: Finset.mul_sum, mul_assoc
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
g : (z : ℂ) → ℂ := 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 (max 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
hbc : LE.le (α := ℝ) (∑ i ∈ Ico B₁ (max B₁ B₂), ‖z‖ ^ i) (∑' (i : ℕ), ‖z‖ ^ i)
⊢ ‖1 - z‖ * (ε / 4 / M) * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖z‖ ^ i ≤ ‖1 - z‖ * (ε / 4 / M) * ∑' (i : ℕ), ‖z‖ ^ i

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
g : (z : ℂ) → ℂ := 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 (max 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
x : ℕ
h_1 : x ∉ Ico B₁ (max B₁ B₂)
⊢ 0 ≤ ‖z‖ ^ x

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
g : (z : ℂ) → ℂ := 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 (max 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
⊢ 0 ≤ ‖z‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
g : (z : ℂ) → ℂ := 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 (max 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
⊢ LE.le (α := ℝ) (∑ i ∈ Ico B₁ (max B₁ B₂), ‖z‖ ^ i) (∑' (i : ℕ), ‖z‖ ^ i)

Tactic:
exact Summable.sum_le_tsum _ (fun _ _ ↦ by positivity)
          (summable_geometric_of_lt_one (by positivity) zn)

Premises used: Summable.sum_le_tsum, summable_geometric_of_lt_one
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
g : (z : ℂ) → ℂ := 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 (max 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
rw : ‖1 - z‖ * (ε / 4 / M) * (1 - ‖z‖)⁻¹ = ‖1 - z‖ * (ε / 4 / M) / (1 - ‖z‖)
rw₁ rw₂ : ‖1 - z‖ * (ε / 4 / M) / (1 - ‖z‖) = ‖1 - z‖ * (ε / 4 / M) / (1 - ‖z‖)
⊢ ‖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]

Premises used: tsum_geometric_of_lt_one, div_eq_mul_inv
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
g : (z : ℂ) → ℂ := 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 (max 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
hc : 0 < 1 - ‖z‖
h₁ : 0 < ε / 4 / M
⊢ ‖1 - z‖ * (ε / 4 / M) / (1 - ‖z‖) < M * (1 - ‖z‖) * (ε / 4 / M) / (1 - ‖z‖)

Tactic:
gcongr