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)
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
⊢ ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ε / 4 / M * ‖z‖ ^ i = ‖1 - z‖ * (ε / 4 / M) * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖z‖ ^ i
have 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
Tactic: rw [← mul_sum, ← mul_assoc]
-- 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
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
⊢ ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ε / 4 / M * ‖z‖ ^ i = ‖1 - z‖ * (ε / 4 / M) * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖z‖ ^ i
have 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
Tactic: rw [← mul_sum, ← mul_assoc]
-- 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
S₁ : ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
⊢ ‖1 - z‖ * (ε / 4 / M) * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖z‖ ^ i ≤ ‖1 - z‖ * (ε / 4 / M) * ∑' (i : ℕ), ‖z‖ ^ i
have hbc : LE.le (α := ℝ) (∑ i ∈ Ico B₁ (max B₁ B₂), ‖z‖ ^ i) (∑' (i : ℕ), ‖z‖ ^ i)
Tactic: gcongr
-- 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
S₁ : ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
⊢ ‖1 - z‖ * (ε / 4 / M) * ∑' (i : ℕ), ‖z‖ ^ i = ‖1 - z‖ * (ε / 4 / M) / (1 - ‖z‖)
have rw : ‖1 - z‖ * (ε / 4 / M) * (1 - ‖z‖)⁻¹ = ‖1 - z‖ * (ε / 4 / M) / (1 - ‖z‖)
Tactic: rw [tsum_geometric_of_lt_one (by positivity) zn, ← div_eq_mul_inv]
-- 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
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‖)
⊢ ‖1 - z‖ * (ε / 4 / M) * ∑' (i : ℕ), ‖z‖ ^ i = ‖1 - z‖ * (ε / 4 / M) / (1 - ‖z‖)
have rw₁ : ‖1 - z‖ * (ε / 4 / M) / (1 - ‖z‖) = ‖1 - z‖ * (ε / 4 / M) / (1 - ‖z‖)
Tactic: rw [tsum_geometric_of_lt_one (by positivity) zn, ← div_eq_mul_inv]
-- 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
S₁ : ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
⊢ ‖1 - z‖ * (ε / 4 / M) / (1 - ‖z‖) < M * (1 - ‖z‖) * (ε / 4 / M) / (1 - ‖z‖)
have hc : 0 < 1 - ‖z‖
Tactic: gcongr
-- 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
S₁ : ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
hc : 0 < 1 - ‖z‖
⊢ ‖1 - z‖ * (ε / 4 / M) / (1 - ‖z‖) < M * (1 - ‖z‖) * (ε / 4 / M) / (1 - ‖z‖)
have h₁ : 0 < ε / 4 / M
Tactic: gcongr
-- 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
S₁ : ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
⊢ 1 - ‖z‖ ≠ 0
have linarith : 1 - ‖z‖ = 0 → 1 - ‖z‖ - 0 + (‖z‖ - 1) = 0
Tactic: linarith only [zn]
-- 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
S₁ : ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
⊢ M ≠ 0
have linarith : M = 0 → -1 + (M - 0) + (1 - M) = 0
Tactic: linarith only [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
ε : ℝ
ε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
⊢ M * (1 - ‖z‖) * (ε / 4 / M) / (1 - ‖z‖) = ε / 4
have rw : ε / 4 / M * M * (1 - ‖z‖) / (1 - ‖z‖) = ε / 4
Tactic: rw [← mul_rotate, mul_div_cancel_right₀ _ (by linarith only [zn]),
          div_mul_cancel₀ _ (by linarith only [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
ε : ℝ
ε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 : ε / 4 / M * M * (1 - ‖z‖) / (1 - ‖z‖) = ε / 4
⊢ M * (1 - ‖z‖) * (ε / 4 / M) / (1 - ‖z‖) = ε / 4
have rw₁ : ε / 4 / M * M = ε / 4
Tactic: rw [← mul_rotate, mul_div_cancel_right₀ _ (by linarith only [zn]),
          div_mul_cancel₀ _ (by linarith only [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
ε : ℝ
ε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 : ε / 4 / M * M * (1 - ‖z‖) / (1 - ‖z‖) = ε / 4
rw₁ : ε / 4 / M * M = ε / 4
⊢ M * (1 - ‖z‖) * (ε / 4 / M) / (1 - ‖z‖) = ε / 4
have rw₂ : ε / 4 = ε / 4
Tactic: rw [← mul_rotate, mul_div_cancel_right₀ _ (by linarith only [zn]),
          div_mul_cancel₀ _ (by linarith only [hM])]
-- 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₂ : ‖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
⊢ ‖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
have S₂ : ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
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 Summable.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
      _ = _ := by
        rw [← mul_rotate, mul_div_cancel_right₀ _ (by linarith only [zn]),
          div_mul_cancel₀ _ (by linarith only [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
ε : ℝ
ε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
S₂ : ‖1 - z‖ * ∑ i ∈ Ico B₁ (max 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₁ (max B₁ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i <
    ε / 2
have h₁ : ε / 2 = ε / 4 + ε / 4
Tactic: convert! add_lt_add S₁ S₂ using 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 : ℝ
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
S₂ : ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
⊢ ε / 2 = ε / 4 + ε / 4
have linarith : ε / 2 < ε / 4 + ε / 4 → 2 / 2 = 1
Tactic: linarith only
-- 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
S₁ : ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
S₂ : ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
linarith : ε / 2 < ε / 4 + ε / 4 → 2 / 2 = 1
⊢ ε / 2 = ε / 4 + ε / 4
have linarith₁ : ε / 2 < ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 2 2 = 4
Tactic: linarith only
-- 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
S₁ : ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
S₂ : ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
linarith : ε / 2 < ε / 4 + ε / 4 → 2 / 2 = 1
linarith₁ : ε / 2 < ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 2 2 = 4
⊢ ε / 2 = ε / 4 + ε / 4
have linarith₂ : ε / 2 < ε / 4 + ε / 4 → 4 / 4 = 1
Tactic: linarith only
-- 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
S₁ : ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
S₂ : ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
linarith : ε / 2 < ε / 4 + ε / 4 → 2 / 2 = 1
linarith₁ : ε / 2 < ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 2 2 = 4
linarith₂ : ε / 2 < ε / 4 + ε / 4 → 4 / 4 = 1
⊢ ε / 2 = ε / 4 + ε / 4
have linarith₃ : ε / 2 < ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 1 4 = 4
Tactic: linarith only
-- 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
S₁ : ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
S₂ : ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
linarith : ε / 2 < ε / 4 + ε / 4 → 2 / 2 = 1
linarith₁ : ε / 2 < ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 2 2 = 4
linarith₂ : ε / 2 < ε / 4 + ε / 4 → 4 / 4 = 1
linarith₃ : ε / 2 < ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₄ : ε / 2 < ε / 4 + ε / 4 → 4 / 4 = 1
linarith₅ : ε / 2 < ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 1 4 = 4
⊢ ε / 2 = ε / 4 + ε / 4
have linarith₆ : ε / 2 < ε / 4 + ε / 4 → GT.gt (α := ℝ) 4 0
Tactic: linarith only
-- 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
S₁ : ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
S₂ : ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
linarith : ε / 2 < ε / 4 + ε / 4 → 2 / 2 = 1
linarith₁ : ε / 2 < ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 2 2 = 4
linarith₂ : ε / 2 < ε / 4 + ε / 4 → 4 / 4 = 1
linarith₃ : ε / 2 < ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₄ : ε / 2 < ε / 4 + ε / 4 → 4 / 4 = 1
linarith₅ : ε / 2 < ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₆ : ε / 2 < ε / 4 + ε / 4 → GT.gt (α := ℝ) 4 0
⊢ ε / 2 = ε / 4 + ε / 4
have linarith₇ : ε / 2 < ε / 4 + ε / 4 → 2 * ε - (1 * ε + 1 * ε) = 0
Tactic: linarith only
-- 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
S₁ : ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
S₂ : ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
linarith : ε / 2 < ε / 4 + ε / 4 → 2 / 2 = 1
linarith₁ : ε / 2 < ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 2 2 = 4
linarith₂ : ε / 2 < ε / 4 + ε / 4 → 4 / 4 = 1
linarith₃ : ε / 2 < ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₄ : ε / 2 < ε / 4 + ε / 4 → 4 / 4 = 1
linarith₅ : ε / 2 < ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₆ : ε / 2 < ε / 4 + ε / 4 → GT.gt (α := ℝ) 4 0
linarith₇ : ε / 2 < ε / 4 + ε / 4 → 2 * ε - (1 * ε + 1 * ε) = 0
⊢ ε / 2 = ε / 4 + ε / 4
have linarith₈ : ε / 4 + ε / 4 < ε / 2 → 4 / 4 = 1
Tactic: linarith only
-- 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
S₁ : ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
S₂ : ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
linarith : ε / 2 < ε / 4 + ε / 4 → 2 / 2 = 1
linarith₁ : ε / 2 < ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 2 2 = 4
linarith₂ : ε / 2 < ε / 4 + ε / 4 → 4 / 4 = 1
linarith₃ : ε / 2 < ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₄ : ε / 2 < ε / 4 + ε / 4 → 4 / 4 = 1
linarith₅ : ε / 2 < ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₆ : ε / 2 < ε / 4 + ε / 4 → GT.gt (α := ℝ) 4 0
linarith₇ : ε / 2 < ε / 4 + ε / 4 → 2 * ε - (1 * ε + 1 * ε) = 0
linarith₈ : ε / 4 + ε / 4 < ε / 2 → 4 / 4 = 1
⊢ ε / 2 = ε / 4 + ε / 4
have linarith₉ : ε / 4 + ε / 4 < ε / 2 → HMul.hMul (α := ℝ) 1 4 = 4
Tactic: linarith only
-- 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
S₁ : ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
S₂ : ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
linarith : ε / 2 < ε / 4 + ε / 4 → 2 / 2 = 1
linarith₁ : ε / 2 < ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 2 2 = 4
linarith₂ : ε / 2 < ε / 4 + ε / 4 → 4 / 4 = 1
linarith₃ : ε / 2 < ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₄ : ε / 2 < ε / 4 + ε / 4 → 4 / 4 = 1
linarith₅ : ε / 2 < ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₆ : ε / 2 < ε / 4 + ε / 4 → GT.gt (α := ℝ) 4 0
linarith₇ : ε / 2 < ε / 4 + ε / 4 → 2 * ε - (1 * ε + 1 * ε) = 0
linarith₈ : ε / 4 + ε / 4 < ε / 2 → 4 / 4 = 1
linarith₉ : ε / 4 + ε / 4 < ε / 2 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₁₀ : ε / 4 + ε / 4 < ε / 2 → 4 / 4 = 1
linarith₁₁ : ε / 4 + ε / 4 < ε / 2 → HMul.hMul (α := ℝ) 1 4 = 4
⊢ ε / 2 = ε / 4 + ε / 4
have linarith₁₂ : ε / 4 + ε / 4 < ε / 2 → 2 / 2 = 1
Tactic: linarith only