awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
k :
  Tendsto
    (fun (n : ℕ) ↦ (1 - z) * ∑ j ∈ range n, HSub.hSub (α := ℂ) (∑ k ∈ range n, f k) (∑ k ∈ range (j + 1), f k) * z ^ j)
    atTop (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
this :
  Tendsto (fun (n : ℕ) ↦ (1 - z) * ∑ i ∈ range n, (l - ∑ k ∈ range (i + 1), f k) * z ^ i) atTop
    (𝓝 ((1 - z) * 0 + (l - ∑' (i : ℕ), f i * z ^ i)))
⊢ Tendsto (fun (n : ℕ) ↦ (1 - z) * ∑ i ∈ range n, (l - ∑ j ∈ range (i + 1), f j) * z ^ i) atTop
    (𝓝 (l - ∑' (n : ℕ), f n * z ^ n))
have rwa : ∀
  (this :
    Tendsto (fun (n : ℕ) ↦ (1 - z) * ∑ i ∈ range n, (l - ∑ k ∈ range (i + 1), f k) * z ^ i) atTop
      (𝓝 (0 + (l - ∑' (i : ℕ), f i * z ^ i)))),
  Tendsto (fun (n : ℕ) ↦ (1 - z) * ∑ i ∈ range n, (l - ∑ j ∈ range (i + 1), f j) * z ^ i) atTop
    (𝓝 (l - ∑' (n : ℕ), f n * z ^ n))
Tactic: rwa [mul_zero, zero_add] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
k :
  Tendsto
    (fun (n : ℕ) ↦ (1 - z) * ∑ j ∈ range n, HSub.hSub (α := ℂ) (∑ k ∈ range n, f k) (∑ k ∈ range (j + 1), f k) * z ^ j)
    atTop (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
this :
  Tendsto (fun (n : ℕ) ↦ (1 - z) * ∑ i ∈ range n, (l - ∑ k ∈ range (i + 1), f k) * z ^ i) atTop
    (𝓝 ((1 - z) * 0 + (l - ∑' (i : ℕ), f i * z ^ i)))
rwa :
  ∀
    (this :
      Tendsto (fun (n : ℕ) ↦ (1 - z) * ∑ i ∈ range n, (l - ∑ k ∈ range (i + 1), f k) * z ^ i) atTop
        (𝓝 (0 + (l - ∑' (i : ℕ), f i * z ^ i)))),
    Tendsto (fun (n : ℕ) ↦ (1 - z) * ∑ i ∈ range n, (l - ∑ j ∈ range (i + 1), f j) * z ^ i) atTop
      (𝓝 (l - ∑' (n : ℕ), f n * z ^ n))
⊢ Tendsto (fun (n : ℕ) ↦ (1 - z) * ∑ i ∈ range n, (l - ∑ j ∈ range (i + 1), f j) * z ^ i) atTop
    (𝓝 (l - ∑' (n : ℕ), f n * z ^ n))
have rwa₁ : ∀
  (this :
    Tendsto (fun (n : ℕ) ↦ (1 - z) * ∑ i ∈ range n, (l - ∑ k ∈ range (i + 1), f k) * z ^ i) atTop
      (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))),
  Tendsto (fun (n : ℕ) ↦ (1 - z) * ∑ i ∈ range n, (l - ∑ j ∈ range (i + 1), f j) * z ^ i) atTop
    (𝓝 (l - ∑' (n : ℕ), f n * z ^ n))
Tactic: rwa [mul_zero, zero_add] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
k :
  Tendsto
    (fun (n : ℕ) ↦ (1 - z) * ∑ j ∈ range n, HSub.hSub (α := ℂ) (∑ k ∈ range n, f k) (∑ k ∈ range (j + 1), f k) * z ^ j)
    atTop (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
⊢ Tendsto (fun (n : ℕ) ↦ (1 - z) * ∑ i ∈ range n, (l - ∑ j ∈ range (i + 1), f j) * z ^ i) atTop
    (𝓝 (l - ∑' (n : ℕ), f n * z ^ n))
have suffices : Tendsto (β := ℂ) (fun (n : ℕ) ↦ (l - s n) * ∑ i ∈ range n, z ^ i) atTop (𝓝 0)
Tactic: suffices Tendsto (fun n ↦ (l - s n) * ∑ i ∈ range n, z ^ i) atTop (𝓝 0) by
    simp_rw [mul_sum] at this
    replace this := (this.const_mul (1 - z)).add k
    conv at this =>
      enter [1, n]
      rw [← mul_add, ← sum_add_distrib]
      enter [2, 2, i]
      rw [← add_mul, sub_add_sub_cancel]
    rwa [mul_zero, zero_add] at this
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
k :
  Tendsto
    (fun (n : ℕ) ↦ (1 - z) * ∑ j ∈ range n, HSub.hSub (α := ℂ) (∑ k ∈ range n, f k) (∑ k ∈ range (j + 1), f k) * z ^ j)
    atTop (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
⊢ Tendsto (β := ℂ) (fun (n : ℕ) ↦ (l - s n) * ∑ i ∈ range n, z ^ i) atTop (𝓝 0)
have rw : Tendsto (fun (n : ℕ) ↦ (l - s n) * ∑ i ∈ range n, z ^ i) atTop (𝓝 (0 * (-1 / (z - 1))))
Tactic: rw [← zero_mul (-1 / (z - 1))]
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
k :
  Tendsto
    (fun (n : ℕ) ↦ (1 - z) * ∑ j ∈ range n, HSub.hSub (α := ℂ) (∑ k ∈ range n, f k) (∑ k ∈ range (j + 1), f k) * z ^ j)
    atTop (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
⊢ Tendsto (fun (n : ℕ) ↦ (l - s n) * ∑ i ∈ range n, z ^ i) atTop (𝓝 (0 * (-1 / (z - 1))))
have hf : Tendsto (β := ℂ) (fun (x : ℕ) ↦ l - s x) atTop (𝓝 0)
Tactic: apply Tendsto.mul
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
k :
  Tendsto
    (fun (n : ℕ) ↦ (1 - z) * ∑ j ∈ range n, HSub.hSub (α := ℂ) (∑ k ∈ range n, f k) (∑ k ∈ range (j + 1), f k) * z ^ j)
    atTop (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
hf : Tendsto (β := ℂ) (fun (x : ℕ) ↦ l - s x) atTop (𝓝 0)
⊢ Tendsto (fun (n : ℕ) ↦ (l - s n) * ∑ i ∈ range n, z ^ i) atTop (𝓝 (0 * (-1 / (z - 1))))
have hg : Tendsto (fun (x : ℕ) ↦ ∑ i ∈ range x, z ^ i) atTop (𝓝 (-1 / (z - 1)))
Tactic: apply Tendsto.mul
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
k :
  Tendsto
    (fun (n : ℕ) ↦ (1 - z) * ∑ j ∈ range n, HSub.hSub (α := ℂ) (∑ k ∈ range n, f k) (∑ k ∈ range (j + 1), f k) * z ^ j)
    atTop (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
| Tendsto (fun (x : ℕ) ↦ ∑ i ∈ range x, z ^ i) atTop (𝓝 (-1 / (z - 1)))
have h₁ : ∀ (n : ℕ), ∑ i ∈ range n, z ^ i
Tactic: enter [1, n]
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
k :
  Tendsto
    (fun (n : ℕ) ↦ (1 - z) * ∑ j ∈ range n, HSub.hSub (α := ℂ) (∑ k ∈ range n, f k) (∑ k ∈ range (j + 1), f k) * z ^ j)
    atTop (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
n : ℕ
⊢ z ≠ 1
have contrapose! : ∀ (hz : z = 1), 1 ≤ ‖z‖
Tactic: contrapose! hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
k :
  Tendsto
    (fun (n : ℕ) ↦ (1 - z) * ∑ j ∈ range n, HSub.hSub (α := ℂ) (∑ k ∈ range n, f k) (∑ k ∈ range (j + 1), f k) * z ^ j)
    atTop (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
n : ℕ
| ∑ i ∈ range n, z ^ i
have h₁ : z ^ n / (z - 1) + -1 / (z - 1)
Tactic: rw [geom_sum_eq (by contrapose! hz; simp [hz]), sub_div, sub_eq_add_neg, ← neg_div]
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
k :
  Tendsto
    (fun (n : ℕ) ↦ (1 - z) * ∑ j ∈ range n, HSub.hSub (α := ℂ) (∑ k ∈ range n, f k) (∑ k ∈ range (j + 1), f k) * z ^ j)
    atTop (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
| Tendsto (fun (x : ℕ) ↦ ∑ i ∈ range x, z ^ i) atTop (𝓝 (-1 / (z - 1)))
have h₁ : ∀ (n : ℕ), z ^ n / (z - 1) + -1 / (z - 1)
Tactic: enter [1, n]
      rw [geom_sum_eq (by contrapose! hz; simp [hz]), sub_div, sub_eq_add_neg, ← neg_div]
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
k :
  Tendsto
    (fun (n : ℕ) ↦ (1 - z) * ∑ j ∈ range n, HSub.hSub (α := ℂ) (∑ k ∈ range n, f k) (∑ k ∈ range (j + 1), f k) * z ^ j)
    atTop (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
⊢ Tendsto (fun (x : ℕ) ↦ ∑ i ∈ range x, z ^ i) atTop (𝓝 (-1 / (z - 1)))
have hg : Tendsto (fun (n : ℕ) ↦ z ^ n / (z - 1) + -1 / (z - 1)) atTop (𝓝 (-1 / (z - 1)))
Tactic: conv =>
      enter [1, n]
      rw [geom_sum_eq (by contrapose! hz; simp [hz]), sub_div, sub_eq_add_neg, ← neg_div]
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
k :
  Tendsto
    (fun (n : ℕ) ↦ (1 - z) * ∑ j ∈ range n, HSub.hSub (α := ℂ) (∑ k ∈ range n, f k) (∑ k ∈ range (j + 1), f k) * z ^ j)
    atTop (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
⊢ Tendsto (fun (n : ℕ) ↦ z ^ n / (z - 1) + -1 / (z - 1)) atTop (𝓝 (-1 / (z - 1)))
have hg : Tendsto (fun (n : ℕ) ↦ z ^ n / (z - 1) + (0 / (z - 1) + -1 / (z - 1))) atTop (𝓝 (0 / (z - 1) + -1 / (z - 1)))
Tactic: rw [← zero_add (-1 / (z - 1)), ← zero_div (z - 1)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
k :
  Tendsto
    (fun (n : ℕ) ↦ (1 - z) * ∑ j ∈ range n, HSub.hSub (α := ℂ) (∑ k ∈ range n, f k) (∑ k ∈ range (j + 1), f k) * z ^ j)
    atTop (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
⊢ Tendsto (fun (n : ℕ) ↦ z ^ n / (z - 1) + (0 / (z - 1) + -1 / (z - 1))) atTop (𝓝 (0 / (z - 1) + -1 / (z - 1)))
have hg : Tendsto (fun (x : ℕ) ↦ 0 / (z - 1) + -1 / (z - 1)) atTop (𝓝 (-1 / (z - 1)))
Tactic: apply Tendsto.add (Tendsto.div_const (tendsto_pow_atTop_nhds_zero_of_norm_lt_one hz) (z - 1))
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
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)
have inl : ∀ (hM : M ≤ 1), Tendsto (fun (z : ℂ) ↦ ∑' (n : ℕ), f n * z ^ n) (𝓝[stolzSet M] 1) (𝓝 l)
Tactic: rcases le_or_gt M 1 with hM | hM
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
inl : ∀ (hM : M ≤ 1), Tendsto (fun (z : ℂ) ↦ ∑' (n : ℕ), f n * z ^ n) (𝓝[stolzSet M] 1) (𝓝 l)
⊢ Tendsto (fun (z : ℂ) ↦ ∑' (n : ℕ), f n * z ^ n) (𝓝[stolzSet M] 1) (𝓝 l)
have inr : ∀ (hM : 1 < M), Tendsto (fun (z : ℂ) ↦ ∑' (n : ℕ), f n * z ^ n) (𝓝[stolzSet M] 1) (𝓝 l)
Tactic: rcases le_or_gt M 1 with hM | hM
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
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)
have inl : Tendsto (fun (z : ℂ) ↦ ∑' (n : ℕ), f n * z ^ n) (𝓝[∅] 1) (𝓝 l)
Tactic: simp_rw [stolzSet_empty hM, nhdsWithin_empty, tendsto_bot]
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : M ≤ 1
inl : Tendsto (fun (z : ℂ) ↦ ∑' (n : ℕ), f n * z ^ n) (𝓝[∅] 1) (𝓝 l)
⊢ Tendsto (fun (z : ℂ) ↦ ∑' (n : ℕ), f n * z ^ n) (𝓝[stolzSet M] 1) (𝓝 l)
have inl₁ : Tendsto (fun (z : ℂ) ↦ ∑' (n : ℕ), f n * z ^ n) ⊥ (𝓝 l)
Tactic: simp_rw [stolzSet_empty hM, nhdsWithin_empty, tendsto_bot]
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (hypothesis)
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
⊢ Tendsto (fun (z : ℂ) ↦ ∑' (n : ℕ), f n * z ^ n) (𝓝[stolzSet M] 1) (𝓝 l)
have hm : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, dist (∑ i ∈ range n, f i) l < ε
Tactic: have hm := Metric.tendsto_atTop.mp h
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
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
hm : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, dist (∑ i ∈ range n, f i) l < ε
⊢ Tendsto (fun (z : ℂ) ↦ ∑' (n : ℕ), f n * z ^ n) (𝓝[stolzSet M] 1) (𝓝 l)
have inr : ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : ℂ⦄, x ∈ stolzSet M → dist x 1 < δ → dist (∑' (n : ℕ), f n * x ^ n) l < ε
Tactic: rw [Metric.tendsto_nhdsWithin_nhds]
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
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
hm : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, dist (∑ i ∈ range n, f i) l < ε
⊢ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : ℂ⦄, x ∈ stolzSet M → dist x 1 < δ → dist (∑' (n : ℕ), f n * x ^ n) l < ε
have inr : ∀ (hm : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, ‖∑ i ∈ range n, f i - l‖ < ε),
  ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : ℂ⦄, x ∈ stolzSet M → ‖x - 1‖ < δ → ‖∑' (n : ℕ), f n * x ^ n - l‖ < ε
Tactic: simp only [dist_eq_norm] at hm ⊢
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
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
hm : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, ‖∑ i ∈ range n, f i - l‖ < ε
ε : ℝ
εpos : ε > 0
⊢ ∃ δ > 0, ∀ ⦃x : ℂ⦄, x ∈ stolzSet M → ‖x - 1‖ < δ → ‖∑' (n : ℕ), f n * x ^ n - l‖ < ε
have inr : ∀ (B₁ : ℕ) (hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M),
  ∃ δ > 0, ∀ ⦃x : ℂ⦄, x ∈ stolzSet M → ‖x - 1‖ < δ → ‖∑' (n : ℕ), f n * x ^ n - l‖ < ε
Tactic: obtain ⟨B₁, hB₁⟩ := hm (ε / 4 / M) (by positivity)
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
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
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)‖
⊢ ∃ δ > 0, ∀ ⦃x : ℂ⦄, x ∈ stolzSet M → ‖x - 1‖ < δ → ‖∑' (n : ℕ), f n * x ^ n - l‖ < ε
have right : ∀ ⦃x : ℂ⦄, x ∈ stolzSet M → ‖x - 1‖ < ε / 4 / (F + 1) → ‖∑' (n : ℕ), f n * x ^ n - l‖ < ε
Tactic: use ε / 4 / (F + 1), by positivity
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
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
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 : ℂ
⊢ z ∈ stolzSet M → ‖z - 1‖ < ε / 4 / (F + 1) → ‖∑' (n : ℕ), f n * z ^ n - l‖ < ε
have right : ∀ (zn : ‖z‖ < 1) (zm : ‖1 - z‖ < M * (1 - ‖z‖)), ‖z - 1‖ < ε / 4 / (F + 1) → ‖∑' (n : ℕ), f n * z ^ n - l‖ < ε
Tactic: ⟨zn, zm⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (hypothesis)
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
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)
⊢ ‖∑' (n : ℕ), f n * z ^ n - l‖ < ε
have 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))
Tactic: have p := abel_aux h zn
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (hypothesis)
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
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‖ < ε
have 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‖ < ε
Tactic: simp_rw [Metric.tendsto_atTop, dist_eq_norm, norm_sub_rev] at p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
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
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‖ < ε
have right : ∀ (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: obtain ⟨B₂, hB₂⟩ := p (ε / 2) (by positivity)
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (hypothesis)
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₂ : ∀ 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‖ < ε
have hB₃ : ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
Tactic: replace hB₂ := hB₂ (max B₁ B₂) (by simp)
Cleared hypotheses: hB₂
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
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
this : ‖(1 - z) * ∑ i ∈ range (max B₁ B₂), (l - s (i + 1)) * z ^ i‖ < ε / 2
⊢ ‖∑' (n : ℕ), f n * z ^ n - l‖ = ‖l - g z‖
have rw : ‖l - ∑' (n : ℕ), f n * z ^ n‖ = ‖l - g z‖
Tactic: rw [norm_sub_rev]
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
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
this : ‖(1 - z) * ∑ i ∈ range (max B₁ B₂), (l - s (i + 1)) * z ^ i‖ < ε / 2
⊢ ‖l - g z‖ =
    ‖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‖
have rw : ‖l - g z‖ = ‖l - g z‖
Tactic: rw [sub_add_cancel _]
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
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
this : ‖(1 - z) * ∑ i ∈ range (max B₁ B₂), (l - s (i + 1)) * z ^ i‖ < ε / 2
⊢ ‖∑' (n : ℕ), f n * z ^ n - l‖ < ε
have _ : ‖∑' (n : ℕ), f n * z ^ n - l‖ = ‖l - g z‖
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 ε
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
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
this : ‖(1 - z) * ∑ i ∈ range (max B₁ B₂), (l - s (i + 1)) * z ^ i‖ < ε / 2
_ : ‖∑' (n : ℕ), f n * z ^ n - l‖ = ‖l - g z‖
⊢ ‖∑' (n : ℕ), f n * z ^ n - l‖ < ε
have _₁ : ‖l - g z‖ =
  ‖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‖
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 ε
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
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
⊢ ‖∑' (n : ℕ), f n * z ^ n - l‖ < ε
have right : ‖(1 - z) * ∑ i ∈ range (max B₁ B₂), (l - s (i + 1)) * z ^ i‖ < ε / 2
Tactic: suffices ‖(1 - z) * ∑ i ∈ range (max B₁ B₂), (l - s (i + 1)) * z ^ i‖ < ε / 2 by
    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 ε