awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.AbelLimit
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))
⊢ 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]
-- Module: Mathlib.Analysis.Complex.AbelLimit
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
⊢ ‖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

Premises used: Complex.sub_re, sub_sub_cancel, Complex.norm_eq_sqrt_sq_add_sq, Complex.one_re
-- Module: Mathlib.Analysis.Complex.AbelLimit
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
H₁ : ‖1 - z‖ < M * (1 - ‖z‖)
⊢ HPow.hPow (β := ℕ) z.im 2 = HPow.hPow (β := ℕ) (1 - z).im 2

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

Premises used: Complex.sub_re, sub_sub_cancel, Complex.norm_eq_sqrt_sq_add_sq, Complex.one_re
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
z : ℂ
hzl : (1 - z).re < ε
hzr : |z.im| < s * (1 - z).re
H : ‖1 - z‖ < M * (1 - ‖z‖)
h : HPow.hPow (β := ℕ) z.im 2 = HPow.hPow (β := ℕ) (1 - z).im 2
⊢ z ∈ stolzSet M

Tactic:
⟨sub_pos.mp <| (mul_pos_iff_of_pos_left hM).mp <| (norm_nonneg _).trans_lt H, H⟩

Premises used: sub_pos, Set.Mem, setOf, mul_pos_iff_of_pos_left, And.intro, Iff.mp, LE.le.trans_lt, norm_nonneg, Complex.stolzSet
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
z : ℂ
hzl : (1 - z).re < ε
hzr : |z.im| < s * (1 - z).re
H : ‖1 - z‖ < M * (1 - ‖z‖)
h : HPow.hPow (β := ℕ) z.im 2 = HPow.hPow (β := ℕ) (1 - z).im 2
⊢ z ∈ stolzSet M

Tactic:
exact ⟨sub_pos.mp <| (mul_pos_iff_of_pos_left hM).mp <| (norm_nonneg _).trans_lt H, H⟩
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s : ℝ
hs : 0 < s
obtain :
  ∀ (M ε : ℝ),
    0 < M →
      ∀ (hε : 0 < ε) (H : {z : ℂ | 1 - ε < z.re} ∩ stolzCone s ⊆ stolzSet M),
        ∃ (M : ℝ), 𝓝[stolzCone s] 1 ≤ 𝓝[stolzSet M] 1
⊢ ∃ (M : ℝ), 𝓝[stolzCone s] 1 ≤ 𝓝[stolzSet M] 1

Tactic:
obtain ⟨M, ε, _, hε, H⟩ := stolzCone_subset_stolzSet_aux hs

Premises used: Complex.stolzCone_subset_stolzSet_aux
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s : ℝ
hs : 0 < s
M ε : ℝ
left : 0 < M
hε : 0 < ε
H : {z : ℂ | 1 - ε < z.re} ∩ stolzCone s ⊆ stolzSet M
h : 𝓝[stolzCone s] 1 ≤ 𝓝[stolzSet M] 1
⊢ ∃ (M : ℝ), 𝓝[stolzCone s] 1 ≤ 𝓝[stolzSet M] 1

Tactic:
use M
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s : ℝ
hs : 0 < s
M ε : ℝ
left : 0 < M
hε : 0 < ε
H : {z : ℂ | 1 - ε < z.re} ∩ stolzCone s ⊆ stolzSet M
h : ∃ (u : Set ℂ), IsOpen u ∧ 1 ∈ u ∧ u ∩ stolzCone s ⊆ stolzSet M
⊢ 𝓝[stolzCone s] 1 ≤ 𝓝[stolzSet M] 1

Tactic:
rw [nhdsWithin_le_iff, mem_nhdsWithin]

Premises used: mem_nhdsWithin, nhdsWithin_le_iff
-- Module: Mathlib.Analysis.Complex.AbelLimit
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

Tactic:
⟨{w | 1 - ε < w.re}, isOpen_lt continuous_const continuous_re, ?_, H⟩

Premises used: isOpen_lt, Complex.continuous_re, continuous_const, setOf, HSub.hSub, Complex.re, And.intro, LT.lt, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s : ℝ
hs : 0 < s
M ε : ℝ
left : 0 < M
hε : 0 < ε
H : {z : ℂ | 1 - ε < z.re} ∩ stolzCone s ⊆ stolzSet M
h : Membership.mem (γ := Set ℂ) {w : ℂ | 1 - ε < w.re} 1
⊢ ∃ (u : Set ℂ), IsOpen u ∧ 1 ∈ u ∧ u ∩ stolzCone s ⊆ stolzSet M

Tactic:
refine ⟨{w | 1 - ε < w.re}, isOpen_lt continuous_const continuous_re, ?_, H⟩
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
s : ℝ
hs : 0 < s
M ε : ℝ
left : 0 < M
hε : 0 < ε
H : {z : ℂ | 1 - ε < z.re} ∩ stolzCone s ⊆ stolzSet M
⊢ Membership.mem (γ := Set ℂ) {w : ℂ | 1 - ε < w.re} 1

Tactic:
simp only [Set.mem_setOf_eq, one_re, sub_lt_self_iff, hε]

Premises used: Set.mem_setOf_eq, sub_lt_self_iff, Complex.one_re
-- 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
⊢ 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
-- 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 (x : ℕ) ↦ HSub.hSub (α := ℂ) (∑ i ∈ range x, f i) (∑ i ∈ range x, f i * z ^ i)) atTop
    (𝓝 (l - ∑' (b : ℕ), f b * z ^ b))
⊢ 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

Premises used: Finset.sum_Ico_Ico_comm', Finset.mul_sum, mul_assoc, mul_one_sub, Finset.sum_sub_distrib, mul_comm, Finset.range_eq_Ico, geom_sum_mul_neg, Finset.sum_mul
-- 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 (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))
h₁ : ∀ (n : ℕ), (1 - z) * ∑ x ∈ range n, (∑ i ∈ Ico (x + 1) n, f i) * z ^ x
| 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:
enter [1, n]
-- 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 (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
e_a : ∑ i ∈ Ico (j + 1) n, f i = HSub.hSub (α := ℂ) (∑ k ∈ range n, f k) (∑ k ∈ range (j + 1), f k)
⊢ (∑ 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

Tactic:
congr 1
-- 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 (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 = HSub.hSub (α := ℂ) (∑ k ∈ range n, f k) (∑ k ∈ range (j + 1), f k)

Tactic:
sum_Ico_eq_sub _ (mem_range.mp hj)

Premises used: Finset.sum_Ico_eq_sub, Finset.mem_range, Iff.mp
-- 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 (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 = HSub.hSub (α := ℂ) (∑ k ∈ range n, f k) (∑ k ∈ range (j + 1), f k)

Tactic:
exact sum_Ico_eq_sub _ (mem_range.mp hj)

Premises used: Finset.sum_Ico_eq_sub, Finset.mem_range, Iff.mp
-- 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 (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 : ℕ
h₁ : (1 - z) * ∑ j ∈ range n, HSub.hSub (α := ℂ) (∑ k ∈ range n, f k) (∑ k ∈ range (j + 1), f k) * z ^ j
| (1 - z) * ∑ x ∈ range n, (∑ i ∈ Ico (x + 1) n, f i) * z ^ x

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))]

Premises used: Finset.sum_congr, rfl
-- 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 (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))
h₁ : ∀ (n : ℕ), (1 - z) * ∑ j ∈ range n, HSub.hSub (α := ℂ) (∑ k ∈ range n, f k) (∑ k ∈ range (j + 1), f k) * z ^ j
| 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:
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))]
-- 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 (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) * ∑ 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))]
-- 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))
this : Tendsto (β := ℂ) (fun (n : ℕ) ↦ (l - s n) * ∑ i ∈ range n, z ^ i) atTop (𝓝 0)
⊢ Tendsto (β := ℂ) (fun (n : ℕ) ↦ ∑ i ∈ range n, (l - s n) * z ^ i) atTop (𝓝 0)

Tactic:
simp_rw [mul_sum] at this

Premises used: Finset.mul_sum
-- 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))
this : Tendsto (β := ℂ) (fun (n : ℕ) ↦ ∑ i ∈ range n, (l - s n) * z ^ i) atTop (𝓝 0)
⊢ 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
-- 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))
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)))
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
| 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:
enter [1, n]
-- 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))
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 : ℕ
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)
| (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:
rw [← mul_add, ← sum_add_distrib]

Premises used: Finset.sum_add_distrib, mul_add
-- 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))
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 : ℕ
h₁ : ∀ (i : ℕ), (l - s n) * z ^ i + HSub.hSub (α := ℂ) (∑ k ∈ range n, f k) (∑ k ∈ range (i + 1), f k) * z ^ i
| (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:
enter [2, 2, i]
-- 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))
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 : ℕ
h₁ : (l - ∑ k ∈ range (i + 1), f k) * z ^ i
| (l - s n) * z ^ i + HSub.hSub (α := ℂ) (∑ k ∈ range n, f k) (∑ k ∈ range (i + 1), f k) * z ^ i

Tactic:
rw [← add_mul, sub_add_sub_cancel]

Premises used: add_mul, sub_add_sub_cancel
-- 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))
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)))
h₁ : ∀ (n i : ℕ), (l - ∑ k ∈ range (i + 1), f k) * 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)))

Tactic:
enter [1, n]
      rw [← mul_add, ← sum_add_distrib]
      enter [2, 2, i]
      rw [← add_mul, sub_add_sub_cancel]

Premises used: add_mul, sub_add_sub_cancel, Finset.sum_add_distrib, mul_add
-- 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))
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 - ∑ 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]

Premises used: add_mul, sub_add_sub_cancel, Finset.sum_add_distrib, mul_add
-- 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))
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))
rwa₁ rwa₂ rwa₃ 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))
⊢ 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

Premises used: zero_add, MulZeroClass.mul_zero
-- 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))
suffices : 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))

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
-- 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))
rw : Tendsto (fun (n : ℕ) ↦ (l - s n) * ∑ i ∈ range n, z ^ i) atTop (𝓝 (0 * (-1 / (z - 1))))
⊢ Tendsto (β := ℂ) (fun (n : ℕ) ↦ (l - s n) * ∑ i ∈ range n, z ^ i) atTop (𝓝 0)

Tactic:
rw [← zero_mul (-1 / (z - 1))]

Premises used: MulZeroClass.zero_mul, HSub.hSub, HDiv.hDiv, 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))
hf : Tendsto (β := ℂ) (fun (x : ℕ) ↦ l - s x) atTop (𝓝 0)
hg : Tendsto (fun (x : ℕ) ↦ ∑ i ∈ range x, z ^ i) atTop (𝓝 (-1 / (z - 1)))
⊢ Tendsto (fun (n : ℕ) ↦ (l - s n) * ∑ i ∈ range n, z ^ i) atTop (𝓝 (0 * (-1 / (z - 1))))

Tactic:
apply Tendsto.mul

Premises used: Filter.Tendsto.mul
-- 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 : ℕ) ↦ l - s x) atTop (𝓝 0)

Tactic:
simpa only [neg_zero, neg_sub] using (tendsto_sub_nhds_zero_iff.mpr h).neg

Premises used: Iff.mpr, Filter.Tendsto.neg, neg_sub, neg_zero, tendsto_sub_nhds_zero_iff
-- 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 : ℕ), ∑ i ∈ range n, z ^ i
| Tendsto (fun (x : ℕ) ↦ ∑ i ∈ range x, z ^ i) atTop (𝓝 (-1 / (z - 1)))

Tactic:
enter [1, n]
-- 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))
n : ℕ
contrapose! : ∀ (hz : z = 1), 1 ≤ ‖z‖
⊢ z ≠ 1

Tactic:
contrapose! hz
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
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 : ℕ
hz : z = 1
⊢ 1 ≤ ‖z‖

Tactic:
simp [hz]
-- 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))
n : ℕ
h₁ : z ^ n / (z - 1) + -1 / (z - 1)
| ∑ i ∈ range n, z ^ i

Tactic:
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