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)
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))
h₁ : ∀ (n : ℕ), z ^ n / (z - 1) + -1 / (z - 1)
| Tendsto (fun (x : ℕ) ↦ ∑ i ∈ range x, z ^ i) atTop (𝓝 (-1 / (z - 1)))

Tactic:
enter [1, n]
      rw [geom_sum_eq (by contrapose! hz; simp [hz]), sub_div, sub_eq_add_neg, ← neg_div]

Premises used: neg_div, sub_eq_add_neg, geom_sum_eq, sub_div
-- Module: Mathlib.Analysis.Complex.AbelLimit
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))
hg : Tendsto (fun (n : ℕ) ↦ z ^ n / (z - 1) + -1 / (z - 1)) atTop (𝓝 (-1 / (z - 1)))
⊢ Tendsto (fun (x : ℕ) ↦ ∑ i ∈ range x, z ^ i) 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]

Premises used: neg_div, sub_eq_add_neg, geom_sum_eq, sub_div
-- Module: Mathlib.Analysis.Complex.AbelLimit
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))
hg : Tendsto (fun (n : ℕ) ↦ z ^ n / (z - 1) + (0 / (z - 1) + -1 / (z - 1))) atTop (𝓝 (0 / (z - 1) + -1 / (z - 1)))
⊢ Tendsto (fun (n : ℕ) ↦ z ^ n / (z - 1) + -1 / (z - 1)) atTop (𝓝 (-1 / (z - 1)))

Tactic:
rw [← zero_add (-1 / (z - 1)), ← zero_div (z - 1)]

Premises used: HSub.hSub, zero_div, HDiv.hDiv, zero_add, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.Complex.AbelLimit
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))
hg : Tendsto (fun (x : ℕ) ↦ 0 / (z - 1) + -1 / (z - 1)) atTop (𝓝 (-1 / (z - 1)))
⊢ Tendsto (fun (n : ℕ) ↦ z ^ n / (z - 1) + (0 / (z - 1) + -1 / (z - 1))) atTop (𝓝 (0 / (z - 1) + -1 / (z - 1)))

Tactic:
apply Tendsto.add (Tendsto.div_const (tendsto_pow_atTop_nhds_zero_of_norm_lt_one hz) (z - 1))

Premises used: HSub.hSub, Filter.Tendsto.div_const, Filter.Tendsto.add, OfNat.ofNat, tendsto_pow_atTop_nhds_zero_of_norm_lt_one
-- Module: Mathlib.Analysis.Complex.AbelLimit
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 : ℕ) ↦ 0 / (z - 1) + -1 / (z - 1)) atTop (𝓝 (-1 / (z - 1)))

Tactic:
simp only [zero_div, zero_add, tendsto_const_nhds_iff]

Premises used: zero_div, zero_add, tendsto_const_nhds_iff
-- Module: Mathlib.Analysis.Complex.AbelLimit
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)
inr : ∀ (hM : 1 < M), Tendsto (fun (z : ℂ) ↦ ∑' (n : ℕ), f n * z ^ n) (𝓝[stolzSet M] 1) (𝓝 l)
⊢ Tendsto (fun (z : ℂ) ↦ ∑' (n : ℕ), f n * z ^ n) (𝓝[stolzSet M] 1) (𝓝 l)

Tactic:
rcases le_or_gt M 1 with hM | hM

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.AbelLimit
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)
inl₁ : Tendsto (fun (z : ℂ) ↦ ∑' (n : ℕ), f n * z ^ n) ⊥ (𝓝 l)
⊢ Tendsto (fun (z : ℂ) ↦ ∑' (n : ℕ), f n * z ^ n) (𝓝[stolzSet M] 1) (𝓝 l)

Tactic:
simp_rw [stolzSet_empty hM, nhdsWithin_empty, tendsto_bot]

Premises used: Filter.tendsto_bot, nhdsWithin_empty, Complex.stolzSet_empty
-- 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
⊢ ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, dist (∑ i ∈ range n, f i) l < ε

Tactic:
have hm := Metric.tendsto_atTop.mp h
-- 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
hm : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, dist (∑ i ∈ range n, f i) l < ε
inr : ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : ℂ⦄, x ∈ stolzSet M → dist x 1 < δ → dist (∑' (n : ℕ), f n * x ^ n) l < ε
⊢ Tendsto (fun (z : ℂ) ↦ ∑' (n : ℕ), f n * z ^ n) (𝓝[stolzSet M] 1) (𝓝 l)

Tactic:
rw [Metric.tendsto_nhdsWithin_nhds]

Premises used: Metric.tendsto_nhdsWithin_nhds
-- 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
hm : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, dist (∑ i ∈ range n, f i) l < ε
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‖ < ε
⊢ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : ℂ⦄, x ∈ stolzSet M → dist x 1 < δ → dist (∑' (n : ℕ), f n * x ^ n) l < ε

Tactic:
simp only [dist_eq_norm] at hm ⊢

Premises used: dist_eq_norm
-- 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
hm : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, ‖∑ i ∈ range n, f i - l‖ < ε
ε : ℝ
εpos : ε > 0
⊢ ε / 4 / M > 0

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
hm : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, ‖∑ i ∈ range n, f i - l‖ < ε
ε : ℝ
εpos : ε > 0
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‖ < ε
⊢ ∃ δ > 0, ∀ ⦃x : ℂ⦄, x ∈ stolzSet M → ‖x - 1‖ < δ → ‖∑' (n : ℕ), f n * x ^ n - l‖ < ε

Tactic:
obtain ⟨B₁, hB₁⟩ := hm (ε / 4 / M) (by positivity)

Premises used: HDiv.hDiv, 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
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)‖
⊢ ε / 4 / (F + 1) > 0

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
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)‖
right : ∀ ⦃x : ℂ⦄, x ∈ stolzSet M → ‖x - 1‖ < ε / 4 / (F + 1) → ‖∑' (n : ℕ), f n * x ^ n - l‖ < ε
⊢ ∃ δ > 0, ∀ ⦃x : ℂ⦄, x ∈ stolzSet M → ‖x - 1‖ < δ → ‖∑' (n : ℕ), f n * x ^ n - l‖ < ε

Tactic:
use ε / 4 / (F + 1), by positivity

Premises used: HAdd.hAdd, 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
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 : ℂ
right : ∀ (zn : ‖z‖ < 1) (zm : ‖1 - z‖ < M * (1 - ‖z‖)), ‖z - 1‖ < ε / 4 / (F + 1) → ‖∑' (n : ℕ), f n * z ^ n - l‖ < ε
⊢ z ∈ stolzSet M → ‖z - 1‖ < ε / 4 / (F + 1) → ‖∑' (n : ℕ), f n * z ^ n - l‖ < ε

Tactic:
⟨zn, zm⟩
-- 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
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)
⊢ 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
-- 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
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))
⊢ ∀ ε > 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

Premises used: Metric.tendsto_atTop, dist_eq_norm, 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
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‖ < ε
⊢ ε / 2 > 0

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

Tactic:
obtain ⟨B₂, hB₂⟩ := p (ε / 2) (by positivity)

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

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

Tactic:
rw [norm_sub_rev]

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
this : ‖(1 - z) * ∑ i ∈ range (max B₁ B₂), (l - s (i + 1)) * z ^ i‖ < ε / 2
rw rw₁ : ‖l - g z‖ = ‖l - g z‖
⊢ ‖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:
rw [sub_add_cancel _]

Premises used: sub_add_cancel
-- 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
this : ‖(1 - z) * ∑ i ∈ range (max B₁ B₂), (l - s (i + 1)) * z ^ i‖ < ε / 2
⊢ ‖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‖ ≤
    ‖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:
norm_add_le _ _

Premises used: norm_add_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
this : ‖(1 - z) * ∑ i ∈ range (max B₁ B₂), (l - s (i + 1)) * z ^ i‖ < ε / 2
⊢ ‖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‖ <
    ε / 2 + ε / 2

Tactic:
add_lt_add hB₂ this

Premises used: add_lt_add
-- 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
this : ‖(1 - z) * ∑ i ∈ range (max B₁ B₂), (l - s (i + 1)) * z ^ i‖ < ε / 2
⊢ ε / 2 + ε / 2 = ε

Tactic:
add_halves ε

Premises used: add_halves
-- 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
this : ‖(1 - z) * ∑ i ∈ range (max B₁ B₂), (l - s (i + 1)) * z ^ i‖ < ε / 2
_ : ‖∑' (n : ℕ), f n * z ^ n - l‖ = ‖l - g z‖
_₁ :
  ‖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‖
⊢ ‖∑' (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 ε

Premises used: add_halves, HSub.hSub, norm_add_le, Finset.range, add_lt_add, 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
right : ‖(1 - z) * ∑ i ∈ range (max B₁ B₂), (l - s (i + 1)) * z ^ i‖ < ε / 2
⊢ ‖∑' (n : ℕ), f n * z ^ n - l‖ < ε

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 ε
-- 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
rw :
  ‖(1 - z) * ∑ i ∈ range (max B₁ B₂), (l - s (i + 1)) * z ^ i‖ =
    ‖(1 - z) *
        HAdd.hAdd (α := ℂ) (∑ i ∈ range B₁, (l - s (i + 1)) * z ^ i)
          (∑ i ∈ Ico B₁ (max B₁ B₂), (l - s (i + 1)) * z ^ i)‖
rw₁ rw₂ :
  ‖(1 - z) * ∑ i ∈ range (max B₁ B₂), (l - s (i + 1)) * z ^ i‖ =
    ‖(1 - z) * ∑ k ∈ range (max B₁ B₂), (l - s (k + 1)) * z ^ k‖
⊢ ‖(1 - z) * ∑ i ∈ range (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:
rw [← mul_add, sum_range_add_sum_Ico _ (le_max_left B₁ B₂)]

Premises used: Finset.sum_range_add_sum_Ico, mul_add, le_max_left
-- 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 + (1 - z) * ∑ 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:
norm_add_le _ _

Premises used: norm_add_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
rw :
  ‖1 - z‖ * norm (E := ℂ) (∑ i ∈ range B₁, (l - s (i + 1)) * z ^ i) +
      ‖(1 - z) * ∑ 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)
rw₁ rw₂ :
  ‖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‖ * 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‖ =
    ‖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)

Tactic:
rw [norm_mul, norm_mul]

Premises used: norm_mul