-- Mathlib/Analysis/Complex/AbelLimit.lean
/-- Auxiliary lemma for Abel's limit theorem. The difference between the sum `l` at 1 and the
power series's value at a point `z` away from 1 can be rewritten as `1 - z` times a power series
whose coefficients are tail sums of `l`. -/
lemma abel_aux (h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)) {z : ℂ} (hz : ‖z‖ < 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))

Proof state:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i
k :
  Tendsto (fun n => (1 - z) * ∑ j ∈ range n, (∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k) * z ^ j) atTop
    (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
⊢ Tendsto (fun n => (l - s n) * ∑ i ∈ range n, z ^ i) atTop (𝓝 0)

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

Result:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i
k :
  Tendsto (fun n => (1 - z) * ∑ j ∈ range n, (∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k) * z ^ j) atTop
    (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
⊢ Tendsto (fun n => (l - s n) * ∑ i ∈ range n, z ^ i) atTop (𝓝 (0 * (-1 / (z - 1))))

Proof state:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i
k : Tendsto (fun x => ∑ 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))

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

Result:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : ℕ → ℂ := 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))

Proof state:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i
k :
  Tendsto (fun n => (1 - z) * ∑ j ∈ range n, (∑ 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))

Tactic:
replace this := (this.const_mul (1 - z)).add k

Result:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i
k :
  Tendsto (fun n => (1 - z) * ∑ j ∈ range n, (∑ 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, (∑ 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))

Proof state:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i
k :
  Tendsto (fun n => (1 - z) * ∑ j ∈ range n, (∑ 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]

Result:
no goals

Proof state:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i
k :
  Tendsto (fun n => (1 - z) * ∑ j ∈ range n, (∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k) * z ^ j) atTop
    (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
⊢ Tendsto (fun n => (1 - z) * ∑ i ∈ range n, (l - ∑ j ∈ range (i + 1), f j) * z ^ i) atTop
    (𝓝 (l - ∑' (n : ℕ), f n * z ^ n))

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

Result:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i
k :
  Tendsto (fun n => (1 - z) * ∑ j ∈ range n, (∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k) * z ^ j) atTop
    (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
⊢ Tendsto (fun n => (l - s n) * ∑ i ∈ range n, z ^ i) atTop (𝓝 0)

Proof state:
case e_a
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : ℕ → ℂ := 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 = ∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k

Tactic:
exact sum_Ico_eq_sub _ (mem_range.mp hj)

Result:
no goals

Proof state:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : ℕ → ℂ := 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 => (∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k) * z ^ j) j

Tactic:
congr 1

Result:
case e_a
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : ℕ → ℂ := 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 = ∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k

Proof state:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 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:
let s := fun n ↦ ∑ i ∈ range n, f i

Result:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : ℕ → ℂ := 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))

Proof state:
case hg
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i
k :
  Tendsto (fun n => (1 - z) * ∑ j ∈ range n, (∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k) * z ^ j) atTop
    (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
⊢ Tendsto (fun x => ∑ i ∈ range x, z ^ i) atTop (𝓝 (-1 / (z - 1)))

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

Result:
case hg
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i
k :
  Tendsto (fun n => (1 - z) * ∑ j ∈ range n, (∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k) * z ^ j) atTop
    (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
⊢ Tendsto (fun n => z ^ n / (z - 1) + -1 / (z - 1)) atTop (𝓝 (-1 / (z - 1)))