awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
H : √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2) ≤ 1 - x / 2
calc : √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ≤ √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) (s * x) 2)
⊢ √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) <
    (2 * √(1 + HPow.hPow (β := ℕ) s 2) + 1) * (1 - √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2))
have calc₁ : √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) (s * x) 2) = √((1 + HPow.hPow (β := ℕ) s 2) * HPow.hPow (β := ℕ) x 2)
Tactic: calc √(x ^ 2 + y ^ 2)
    _ ≤ √(x ^ 2 + (s * x) ^ 2) := by rw [← sq_abs y]; gcongr
    _ = √((1 + s ^ 2) * x ^ 2) := by congr; ring
    _ = √(1 + s ^ 2) * x := by rw [sqrt_mul' _ (sq_nonneg x), sqrt_sq hx₀.le]
    _ = 2 * √(1 + s ^ 2) * (x / 2) := by ring
    _ < (2 * √(1 + s ^ 2) + 1) * (x / 2) := by gcongr; exact lt_add_one _
    _ ≤ _ := by gcongr; exact le_sub_comm.mpr H
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
H : √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2) ≤ 1 - x / 2
calc : √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ≤ √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) (s * x) 2)
calc₁ :
  √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) (s * x) 2) = √((1 + HPow.hPow (β := ℕ) s 2) * HPow.hPow (β := ℕ) x 2)
⊢ √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) <
    (2 * √(1 + HPow.hPow (β := ℕ) s 2) + 1) * (1 - √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2))
have calc₂ : √((1 + HPow.hPow (β := ℕ) s 2) * HPow.hPow (β := ℕ) x 2) = √(1 + HPow.hPow (β := ℕ) s 2) * x
Tactic: calc √(x ^ 2 + y ^ 2)
    _ ≤ √(x ^ 2 + (s * x) ^ 2) := by rw [← sq_abs y]; gcongr
    _ = √((1 + s ^ 2) * x ^ 2) := by congr; ring
    _ = √(1 + s ^ 2) * x := by rw [sqrt_mul' _ (sq_nonneg x), sqrt_sq hx₀.le]
    _ = 2 * √(1 + s ^ 2) * (x / 2) := by ring
    _ < (2 * √(1 + s ^ 2) + 1) * (x / 2) := by gcongr; exact lt_add_one _
    _ ≤ _ := by gcongr; exact le_sub_comm.mpr H
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
H : √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2) ≤ 1 - x / 2
calc : √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ≤ √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) (s * x) 2)
calc₁ :
  √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) (s * x) 2) = √((1 + HPow.hPow (β := ℕ) s 2) * HPow.hPow (β := ℕ) x 2)
calc₂ : √((1 + HPow.hPow (β := ℕ) s 2) * HPow.hPow (β := ℕ) x 2) = √(1 + HPow.hPow (β := ℕ) s 2) * x
⊢ √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) <
    (2 * √(1 + HPow.hPow (β := ℕ) s 2) + 1) * (1 - √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2))
have calc₃ : √(1 + HPow.hPow (β := ℕ) s 2) * x = 2 * √(1 + HPow.hPow (β := ℕ) s 2) * (x / 2)
Tactic: calc √(x ^ 2 + y ^ 2)
    _ ≤ √(x ^ 2 + (s * x) ^ 2) := by rw [← sq_abs y]; gcongr
    _ = √((1 + s ^ 2) * x ^ 2) := by congr; ring
    _ = √(1 + s ^ 2) * x := by rw [sqrt_mul' _ (sq_nonneg x), sqrt_sq hx₀.le]
    _ = 2 * √(1 + s ^ 2) * (x / 2) := by ring
    _ < (2 * √(1 + s ^ 2) + 1) * (x / 2) := by gcongr; exact lt_add_one _
    _ ≤ _ := by gcongr; exact le_sub_comm.mpr H
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
H : √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2) ≤ 1 - x / 2
calc : √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ≤ √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) (s * x) 2)
calc₁ :
  √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) (s * x) 2) = √((1 + HPow.hPow (β := ℕ) s 2) * HPow.hPow (β := ℕ) x 2)
calc₂ : √((1 + HPow.hPow (β := ℕ) s 2) * HPow.hPow (β := ℕ) x 2) = √(1 + HPow.hPow (β := ℕ) s 2) * x
calc₃ : √(1 + HPow.hPow (β := ℕ) s 2) * x = 2 * √(1 + HPow.hPow (β := ℕ) s 2) * (x / 2)
⊢ √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) <
    (2 * √(1 + HPow.hPow (β := ℕ) s 2) + 1) * (1 - √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2))
have calc₄ : 2 * √(1 + HPow.hPow (β := ℕ) s 2) * (x / 2) < (2 * √(1 + HPow.hPow (β := ℕ) s 2) + 1) * (x / 2)
Tactic: calc √(x ^ 2 + y ^ 2)
    _ ≤ √(x ^ 2 + (s * x) ^ 2) := by rw [← sq_abs y]; gcongr
    _ = √((1 + s ^ 2) * x ^ 2) := by congr; ring
    _ = √(1 + s ^ 2) * x := by rw [sqrt_mul' _ (sq_nonneg x), sqrt_sq hx₀.le]
    _ = 2 * √(1 + s ^ 2) * (x / 2) := by ring
    _ < (2 * √(1 + s ^ 2) + 1) * (x / 2) := by gcongr; exact lt_add_one _
    _ ≤ _ := by gcongr; exact le_sub_comm.mpr H
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + HPow.hPow (β := ℕ) s 2)
hy : |y| < s * x
H : √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2) ≤ 1 - x / 2
calc : √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ≤ √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) (s * x) 2)
calc₁ :
  √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) (s * x) 2) = √((1 + HPow.hPow (β := ℕ) s 2) * HPow.hPow (β := ℕ) x 2)
calc₂ : √((1 + HPow.hPow (β := ℕ) s 2) * HPow.hPow (β := ℕ) x 2) = √(1 + HPow.hPow (β := ℕ) s 2) * x
calc₃ : √(1 + HPow.hPow (β := ℕ) s 2) * x = 2 * √(1 + HPow.hPow (β := ℕ) s 2) * (x / 2)
calc₄ : 2 * √(1 + HPow.hPow (β := ℕ) s 2) * (x / 2) < (2 * √(1 + HPow.hPow (β := ℕ) s 2) + 1) * (x / 2)
⊢ √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) <
    (2 * √(1 + HPow.hPow (β := ℕ) s 2) + 1) * (1 - √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2))
have calc₅ : (2 * √(1 + HPow.hPow (β := ℕ) s 2) + 1) * (x / 2) ≤
  (2 * √(1 + HPow.hPow (β := ℕ) s 2) + 1) * (1 - √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2))
Tactic: calc √(x ^ 2 + y ^ 2)
    _ ≤ √(x ^ 2 + (s * x) ^ 2) := by rw [← sq_abs y]; gcongr
    _ = √((1 + s ^ 2) * x ^ 2) := by congr; ring
    _ = √(1 + s ^ 2) * x := by rw [sqrt_mul' _ (sq_nonneg x), sqrt_sq hx₀.le]
    _ = 2 * √(1 + s ^ 2) * (x / 2) := by ring
    _ < (2 * √(1 + s ^ 2) + 1) * (x / 2) := by gcongr; exact lt_add_one _
    _ ≤ _ := by gcongr; exact le_sub_comm.mpr H
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
s : ℝ
hs : 0 < s
⊢ ∃ (M : ℝ) (ε : ℝ), 0 < M ∧ 0 < ε ∧ {z : ℂ | 1 - ε < z.re} ∩ stolzCone s ⊆ stolzSet M
have h : ∀ (M ε : ℝ) (hM : 0 < M) (hε : 0 < ε)
  (H :
    ∀ (x y : ℝ),
      0 < x →
        x < ε →
          |y| < s * x →
            √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) <
              M * (1 - √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2))),
  {z : ℂ | 1 - ε < z.re} ∩ stolzCone s ⊆ stolzSet M
Tactic: peel stolzCone_subset_stolzSet_aux' s with M ε hM hε H
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (hypothesis)
Goal:
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
H :
  ∀ (x y : ℝ),
    0 < x →
      x < ε →
        |y| < s * x →
          √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) <
            M * (1 - √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2))
z : ℂ
hzl : Membership.mem (γ := Set ℂ) {z : ℂ | 1 - ε < z.re} z
hzr : z ∈ stolzCone s
⊢ z ∈ stolzSet M
have hzl₁ : (1 - z).re < ε
Tactic: rw [Set.mem_setOf_eq, sub_lt_comm, ← one_re, ← sub_re] at hzl
Cleared hypotheses: hzl, hzr
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (hypothesis)
Goal:
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
H :
  ∀ (x y : ℝ),
    0 < x →
      x < ε →
        |y| < s * x →
          √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) <
            M * (1 - √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2))
z : ℂ
hzl : (1 - z).re < ε
hzr : z ∈ stolzCone s
⊢ z ∈ stolzSet M
have hzr₁ : |z.im| < s * (1 - z).re
Tactic: rw [stolzCone, Set.mem_setOf_eq, ← one_re, ← sub_re] at hzr
Cleared hypotheses: hzr
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (hypothesis)
Goal:
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
H :
  ∀ (x y : ℝ),
    0 < x →
      x < ε →
        |y| < s * x →
          √(HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) <
            M * (1 - √(HPow.hPow (β := ℕ) (1 - x) 2 + HPow.hPow (β := ℕ) y 2))
z : ℂ
hzl : (1 - z).re < ε
hzr : |z.im| < s * (1 - z).re
⊢ z ∈ stolzSet M
have H₁ : √(HPow.hPow (β := ℕ) (1 - z).re 2 + HPow.hPow (β := ℕ) z.im 2) <
  M * (1 - √(HPow.hPow (β := ℕ) (1 - (1 - z).re) 2 + HPow.hPow (β := ℕ) z.im 2))
Tactic: replace H :=
    H (1 - z).re z.im ((mul_pos_iff_of_pos_left hs).mp <| (abs_nonneg z.im).trans_lt hzr) hzl hzr
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (hypothesis)
Goal:
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
z : ℂ
hzl : (1 - z).re < ε
hzr : |z.im| < s * (1 - z).re
H :
  √(HPow.hPow (β := ℕ) (1 - z).re 2 + HPow.hPow (β := ℕ) z.im 2) <
    M * (1 - √(HPow.hPow (β := ℕ) (1 - (1 - z).re) 2 + HPow.hPow (β := ℕ) z.im 2))
⊢ z ∈ stolzSet M
have h : HPow.hPow (β := ℕ) z.im 2 = HPow.hPow (β := ℕ) (1 - z).im 2
Tactic: have h : z.im ^ 2 = (1 - z).im ^ 2 := by
    simp only [sub_im, one_im, zero_sub, neg_sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (hypothesis)
Goal:
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
z : ℂ
hzl : (1 - z).re < ε
hzr : |z.im| < s * (1 - z).re
H :
  √(HPow.hPow (β := ℕ) (1 - z).re 2 + HPow.hPow (β := ℕ) z.im 2) <
    M * (1 - √(HPow.hPow (β := ℕ) (1 - (1 - z).re) 2 + HPow.hPow (β := ℕ) z.im 2))
h : HPow.hPow (β := ℕ) z.im 2 = HPow.hPow (β := ℕ) (1 - z).im 2
⊢ z ∈ stolzSet M
have H₁ : ‖1 - z‖ < M * (1 - ‖z‖)
Tactic: rw [h, ← norm_eq_sqrt_sq_add_sq, ← h, sub_re, one_re, sub_sub_cancel,
    ← norm_eq_sqrt_sq_add_sq] at H
Cleared hypotheses: H, h
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
s : ℝ
hs : 0 < s
⊢ ∃ (M : ℝ), 𝓝[stolzCone s] 1 ≤ 𝓝[stolzSet M] 1
have obtain : ∀ (M ε : ℝ),
  0 < M →
    ∀ (hε : 0 < ε) (H : {z : ℂ | 1 - ε < z.re} ∩ stolzCone s ⊆ stolzSet M),
      ∃ (M : ℝ), 𝓝[stolzCone s] 1 ≤ 𝓝[stolzSet M] 1
Tactic: obtain ⟨M, ε, _, hε, H⟩ := stolzCone_subset_stolzSet_aux hs
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
s : ℝ
hs : 0 < s
M ε : ℝ
left : 0 < M
hε : 0 < ε
H : {z : ℂ | 1 - ε < z.re} ∩ stolzCone s ⊆ stolzSet M
⊢ ∃ (M : ℝ), 𝓝[stolzCone s] 1 ≤ 𝓝[stolzSet M] 1
have h : 𝓝[stolzCone s] 1 ≤ 𝓝[stolzSet M] 1
Tactic: use M
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
s : ℝ
hs : 0 < s
M ε : ℝ
left : 0 < M
hε : 0 < ε
H : {z : ℂ | 1 - ε < z.re} ∩ stolzCone s ⊆ stolzSet M
⊢ 𝓝[stolzCone s] 1 ≤ 𝓝[stolzSet M] 1
have h : ∃ (u : Set ℂ), IsOpen u ∧ 1 ∈ u ∧ u ∩ stolzCone s ⊆ stolzSet M
Tactic: rw [nhdsWithin_le_iff, mem_nhdsWithin]
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
s : ℝ
hs : 0 < s
M ε : ℝ
left : 0 < M
hε : 0 < ε
H : {z : ℂ | 1 - ε < z.re} ∩ stolzCone s ⊆ stolzSet M
⊢ ∃ (u : Set ℂ), IsOpen u ∧ 1 ∈ u ∧ u ∩ stolzCone s ⊆ stolzSet M
have h : Membership.mem (γ := Set ℂ) {w : ℂ | 1 - ε < w.re} 1
Tactic: refine ⟨{w | 1 - ε < w.re}, isOpen_lt continuous_const continuous_re, ?_, H⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (hypothesis)
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
⊢ 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 k : Tendsto (fun (x : ℕ) ↦ HSub.hSub (α := ℂ) (∑ i ∈ range x, f i) (∑ i ∈ range x, f i * z ^ i)) atTop
  (𝓝 (l - ∑' (b : ℕ), f b * z ^ b))
Tactic: have k := h.sub (summable_powerSeries_of_norm_lt_one h.cauchySeq hz).hasSum.tendsto_sum_nat
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (hypothesis)
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 (x : ℕ) ↦ HSub.hSub (α := ℂ) (∑ i ∈ range x, f i) (∑ i ∈ range x, f i * z ^ i)) atTop
    (𝓝 (l - ∑' (b : ℕ), f b * z ^ b))
⊢ 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 k₁ : Tendsto (fun (x : ℕ) ↦ (1 - z) * ∑ x_1 ∈ range x, (∑ i ∈ Ico (x_1 + 1) x, f i) * z ^ x_1) atTop
  (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
Tactic: simp_rw [← sum_sub_distrib, ← mul_one_sub, ← geom_sum_mul_neg, ← mul_assoc, ← sum_mul,
    mul_comm, mul_sum _ _ (f _), range_eq_Ico, ← sum_Ico_Ico_comm', ← range_eq_Ico,
    ← sum_mul] at k
Cleared hypotheses: k
-- 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 (x : ℕ) ↦ (1 - z) * ∑ x_1 ∈ range x, (∑ i ∈ Ico (x_1 + 1) x, f i) * z ^ x_1) atTop
    (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
| Tendsto (fun (x : ℕ) ↦ (1 - z) * ∑ x_1 ∈ range x, (∑ i ∈ Ico (x_1 + 1) x, f i) * z ^ x_1) atTop
    (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
have h₁ : ∀ (n : ℕ), (1 - z) * ∑ x ∈ range n, (∑ i ∈ Ico (x + 1) n, f i) * z ^ x
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 (x : ℕ) ↦ (1 - z) * ∑ x_1 ∈ range x, (∑ i ∈ Ico (x_1 + 1) x, f i) * z ^ x_1) atTop
    (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
n j : ℕ
hj : j ∈ range n
⊢ (∑ i ∈ Ico (j + 1) n, f i) * z ^ j =
    (fun (j : ℕ) ↦ HSub.hSub (α := ℂ) (∑ k ∈ range n, f k) (∑ k ∈ range (j + 1), f k) * z ^ j) j
have e_a : ∑ i ∈ Ico (j + 1) n, f i = HSub.hSub (α := ℂ) (∑ k ∈ range n, f k) (∑ k ∈ range (j + 1), f k)
Tactic: congr 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 (x : ℕ) ↦ (1 - z) * ∑ x_1 ∈ range x, (∑ i ∈ Ico (x_1 + 1) x, f i) * z ^ x_1) atTop
    (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
n : ℕ
| (1 - z) * ∑ x ∈ range n, (∑ i ∈ Ico (x + 1) n, f i) * z ^ x
have h₁ : (1 - z) * ∑ j ∈ range n, HSub.hSub (α := ℂ) (∑ k ∈ range n, f k) (∑ k ∈ range (j + 1), f k) * z ^ j
Tactic: rw [sum_congr (g := fun j ↦ (∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k) * z ^ j)
      rfl (fun j hj ↦ by congr 1; exact sum_Ico_eq_sub _ (mem_range.mp hj))]
-- 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 (x : ℕ) ↦ (1 - z) * ∑ x_1 ∈ range x, (∑ i ∈ Ico (x_1 + 1) x, f i) * z ^ x_1) atTop
    (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
| Tendsto (fun (x : ℕ) ↦ (1 - z) * ∑ x_1 ∈ range x, (∑ i ∈ Ico (x_1 + 1) x, f i) * z ^ x_1) atTop
    (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
have h₁ : ∀ (n : ℕ), (1 - z) * ∑ j ∈ range n, HSub.hSub (α := ℂ) (∑ k ∈ range n, f k) (∑ k ∈ range (j + 1), f k) * z ^ j
Tactic: enter [1, n]
    rw [sum_congr (g := fun j ↦ (∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k) * z ^ j)
      rfl (fun j hj ↦ by congr 1; exact sum_Ico_eq_sub _ (mem_range.mp hj))]
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (hypothesis)
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 (x : ℕ) ↦ (1 - z) * ∑ x_1 ∈ range x, (∑ i ∈ Ico (x_1 + 1) x, f i) * z ^ x_1) 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 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))
Tactic: conv at k =>
    enter [1, n]
    rw [sum_congr (g := fun j ↦ (∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k) * z ^ j)
      rfl (fun j hj ↦ by congr 1; exact sum_Ico_eq_sub _ (mem_range.mp hj))]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (hypothesis)
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 : ℕ) ↦ (l - s n) * ∑ i ∈ range n, z ^ i) atTop (𝓝 0)
⊢ 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 this₁ : Tendsto (β := ℂ) (fun (n : ℕ) ↦ ∑ i ∈ range n, (l - s n) * z ^ i) atTop (𝓝 0)
Tactic: simp_rw [mul_sum] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (hypothesis)
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 : ℕ) ↦ ∑ i ∈ range n, (l - s n) * z ^ i) atTop (𝓝 0)
⊢ 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 this₁ : Tendsto
  (fun (x : ℕ) ↦
    (1 - z) * ∑ i ∈ range x, (l - s x) * z ^ i +
      (1 - z) * ∑ j ∈ range x, HSub.hSub (α := ℂ) (∑ k ∈ range x, f k) (∑ k ∈ range (j + 1), f k) * z ^ j)
  atTop (𝓝 ((1 - z) * 0 + (l - ∑' (i : ℕ), f i * z ^ i)))
Tactic: replace this := (this.const_mul (1 - z)).add k
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 (x : ℕ) ↦
      (1 - z) * ∑ i ∈ range x, (l - s x) * z ^ i +
        (1 - z) * ∑ j ∈ range x, HSub.hSub (α := ℂ) (∑ k ∈ range x, f k) (∑ k ∈ range (j + 1), f k) * z ^ j)
    atTop (𝓝 ((1 - z) * 0 + (l - ∑' (i : ℕ), f i * z ^ i)))
| Tendsto
    (fun (x : ℕ) ↦
      (1 - z) * ∑ i ∈ range x, (l - s x) * z ^ i +
        (1 - z) * ∑ j ∈ range x, HSub.hSub (α := ℂ) (∑ k ∈ range x, f k) (∑ k ∈ range (j + 1), f k) * z ^ j)
    atTop (𝓝 ((1 - z) * 0 + (l - ∑' (i : ℕ), f i * z ^ i)))
have h₁ : ∀ (n : ℕ),
  (1 - z) * ∑ i ∈ range n, (l - s n) * z ^ i +
    (1 - z) * ∑ j ∈ range n, HSub.hSub (α := ℂ) (∑ k ∈ range n, f k) (∑ k ∈ range (j + 1), f k) * z ^ j
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))
this :
  Tendsto
    (fun (x : ℕ) ↦
      (1 - z) * ∑ i ∈ range x, (l - s x) * z ^ i +
        (1 - z) * ∑ j ∈ range x, HSub.hSub (α := ℂ) (∑ k ∈ range x, f k) (∑ k ∈ range (j + 1), f k) * z ^ j)
    atTop (𝓝 ((1 - z) * 0 + (l - ∑' (i : ℕ), f i * z ^ i)))
n : ℕ
| (1 - z) * ∑ i ∈ range n, (l - s n) * z ^ i +
    (1 - z) * ∑ j ∈ range n, HSub.hSub (α := ℂ) (∑ k ∈ range n, f k) (∑ k ∈ range (j + 1), f k) * z ^ j
have h₁ : (1 - z) *
  ∑ x ∈ range n, ((l - s n) * z ^ x + HSub.hSub (α := ℂ) (∑ k ∈ range n, f k) (∑ k ∈ range (x + 1), f k) * z ^ x)
Tactic: rw [← mul_add, ← sum_add_distrib]
-- 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 (x : ℕ) ↦
      (1 - z) * ∑ i ∈ range x, (l - s x) * z ^ i +
        (1 - z) * ∑ j ∈ range x, HSub.hSub (α := ℂ) (∑ k ∈ range x, f k) (∑ k ∈ range (j + 1), f k) * z ^ j)
    atTop (𝓝 ((1 - z) * 0 + (l - ∑' (i : ℕ), f i * z ^ i)))
n : ℕ
| (1 - z) *
    ∑ x ∈ range n, ((l - s n) * z ^ x + HSub.hSub (α := ℂ) (∑ k ∈ range n, f k) (∑ k ∈ range (x + 1), f k) * z ^ x)
have h₁ : ∀ (i : ℕ), (l - s n) * z ^ i + HSub.hSub (α := ℂ) (∑ k ∈ range n, f k) (∑ k ∈ range (i + 1), f k) * z ^ i
Tactic: enter [2, 2, i]
-- 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 (x : ℕ) ↦
      (1 - z) * ∑ i ∈ range x, (l - s x) * z ^ i +
        (1 - z) * ∑ j ∈ range x, HSub.hSub (α := ℂ) (∑ k ∈ range x, f k) (∑ k ∈ range (j + 1), f k) * z ^ j)
    atTop (𝓝 ((1 - z) * 0 + (l - ∑' (i : ℕ), f i * z ^ i)))
n i : ℕ
| (l - s n) * z ^ i + HSub.hSub (α := ℂ) (∑ k ∈ range n, f k) (∑ k ∈ range (i + 1), f k) * z ^ i
have h₁ : (l - ∑ k ∈ range (i + 1), f k) * z ^ i
Tactic: rw [← add_mul, sub_add_sub_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)
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 (x : ℕ) ↦
      (1 - z) * ∑ i ∈ range x, (l - s x) * z ^ i +
        (1 - z) * ∑ j ∈ range x, HSub.hSub (α := ℂ) (∑ k ∈ range x, f k) (∑ k ∈ range (j + 1), f k) * z ^ j)
    atTop (𝓝 ((1 - z) * 0 + (l - ∑' (i : ℕ), f i * z ^ i)))
| Tendsto
    (fun (x : ℕ) ↦
      (1 - z) * ∑ i ∈ range x, (l - s x) * z ^ i +
        (1 - z) * ∑ j ∈ range x, HSub.hSub (α := ℂ) (∑ k ∈ range x, f k) (∑ k ∈ range (j + 1), f k) * z ^ j)
    atTop (𝓝 ((1 - z) * 0 + (l - ∑' (i : ℕ), f i * z ^ i)))
have h₁ : ∀ (n i : ℕ), (l - ∑ k ∈ range (i + 1), f k) * z ^ i
Tactic: enter [1, n]
      rw [← mul_add, ← sum_add_distrib]
      enter [2, 2, i]
      rw [← add_mul, sub_add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (hypothesis)
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 (x : ℕ) ↦
      (1 - z) * ∑ i ∈ range x, (l - s x) * z ^ i +
        (1 - z) * ∑ j ∈ range x, HSub.hSub (α := ℂ) (∑ k ∈ range x, f k) (∑ k ∈ range (j + 1), f k) * z ^ j)
    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 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)))
Tactic: conv at this =>
      enter [1, n]
      rw [← mul_add, ← sum_add_distrib]
      enter [2, 2, i]
      rw [← add_mul, sub_add_sub_cancel]
Cleared hypotheses: this