-- Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean
lemma term_sum_of_lt (N : ℕ) {s : ℝ} (hs : 1 < s) :
    term_sum s N = 1 / (s - 1) * (1 - 1 / (N + 1) ^ (s - 1))
    - 1 / s * ((∑ n ∈ Finset.range N, 1 / (n + 1 : ℝ) ^ s) - N / (N + 1) ^ s)

Proof state:
case e_a.e_a
N : ℕ
s : ℝ
hs : 1 < s
⊢ ∑ i ∈ Finset.range N, (1 / ↑(i + 1) ^ s - 1 / (↑(i + 1) + 1) ^ s) * ↑(i + 1) =
    ∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s

Tactic:
induction N with
| zero => simp
| succ N hN =>
  simp_rw [Finset.sum_range_succ, hN, Nat.cast_add_one, sub_eq_add_neg, add_assoc]
  congr 1
  ring_nf

Result:
no goals

Proof state:
case e_a
N : ℕ
s : ℝ
hs : 1 < s
⊢ (∑ i ∈ Finset.range N, (1 / ↑(i + 1) ^ s - 1 / (↑(i + 1) + 1) ^ s) * ↑(i + 1)) * s⁻¹ =
    (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s) * s⁻¹

Tactic:
congr 1

Result:
case e_a.e_a
N : ℕ
s : ℝ
hs : 1 < s
⊢ ∑ i ∈ Finset.range N, (1 / ↑(i + 1) ^ s - 1 / (↑(i + 1) + 1) ^ s) * ↑(i + 1) =
    ∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s

Proof state:
N : ℕ
s : ℝ
hs : 1 < s
⊢ ∑ n ∈ Finset.range N,
      (1 / (s - 1) * (1 / ↑(n + 1) ^ (s - 1) - 1 / (↑(n + 1) + 1) ^ (s - 1)) -
        ↑(n + 1) / s * (1 / ↑(n + 1) ^ s - 1 / (↑(n + 1) + 1) ^ s)) =
    1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1)) - 1 / s * (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s)

Tactic:
rw [Finset.sum_sub_distrib]

Result:
N : ℕ
s : ℝ
hs : 1 < s
⊢ ∑ x ∈ Finset.range N, 1 / (s - 1) * (1 / ↑(x + 1) ^ (s - 1) - 1 / (↑(x + 1) + 1) ^ (s - 1)) -
      ∑ x ∈ Finset.range N, ↑(x + 1) / s * (1 / ↑(x + 1) ^ s - 1 / (↑(x + 1) + 1) ^ s) =
    1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1)) - 1 / s * (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s)

Proof state:
case e_a
N : ℕ
s : ℝ
hs : 1 < s
⊢ ∑ x ∈ Finset.range N, ↑(x + 1) / s * (1 / ↑(x + 1) ^ s - 1 / (↑(x + 1) + 1) ^ s) =
    1 / s * (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s)

Tactic:
simp_rw [mul_comm (_ / _), ← mul_div_assoc, div_eq_mul_inv _ s, ← Finset.sum_mul, mul_one]

Result:
case e_a
N : ℕ
s : ℝ
hs : 1 < s
⊢ (∑ i ∈ Finset.range N, (1 / ↑(i + 1) ^ s - 1 / (↑(i + 1) + 1) ^ s) * ↑(i + 1)) * s⁻¹ =
    (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s) * s⁻¹

Proof state:
case e_a.succ
s : ℝ
hs : 1 < s
N : ℕ
hN :
  ∑ x ∈ Finset.range N, 1 / (s - 1) * (1 / ↑(x + 1) ^ (s - 1) - 1 / (↑(x + 1) + 1) ^ (s - 1)) =
    1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1))
⊢ 1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1)) + 1 / (s - 1) * (1 / (↑N + 1) ^ (s - 1) - 1 / (↑N + 1 + 1) ^ (s - 1)) =
    1 / (s - 1) * (1 - 1 / (↑N + 1 + 1) ^ (s - 1))

Tactic:
ring_nf

Result:
no goals

Proof state:
case e_a.succ
s : ℝ
hs : 1 < s
N : ℕ
hN :
  ∑ x ∈ Finset.range N, 1 / (s - 1) * (1 / ↑(x + 1) ^ (s - 1) - 1 / (↑(x + 1) + 1) ^ (s - 1)) =
    1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1))
⊢ ∑ x ∈ Finset.range (N + 1), 1 / (s - 1) * (1 / ↑(x + 1) ^ (s - 1) - 1 / (↑(x + 1) + 1) ^ (s - 1)) =
    1 / (s - 1) * (1 - 1 / (↑(N + 1) + 1) ^ (s - 1))

Tactic:
rw [Finset.sum_range_succ, hN, Nat.cast_add_one]

Result:
case e_a.succ
s : ℝ
hs : 1 < s
N : ℕ
hN :
  ∑ x ∈ Finset.range N, 1 / (s - 1) * (1 / ↑(x + 1) ^ (s - 1) - 1 / (↑(x + 1) + 1) ^ (s - 1)) =
    1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1))
⊢ 1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1)) + 1 / (s - 1) * (1 / (↑N + 1) ^ (s - 1) - 1 / (↑N + 1 + 1) ^ (s - 1)) =
    1 / (s - 1) * (1 - 1 / (↑N + 1 + 1) ^ (s - 1))

Proof state:
case e_a
N : ℕ
s : ℝ
hs : 1 < s
⊢ ∑ x ∈ Finset.range N, 1 / (s - 1) * (1 / ↑(x + 1) ^ (s - 1) - 1 / (↑(x + 1) + 1) ^ (s - 1)) =
    1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1))

Tactic:
induction N with
| zero => simp
| succ N hN =>
  rw [Finset.sum_range_succ, hN, Nat.cast_add_one]
  ring_nf

Result:
no goals

Proof state:
case e_a.e_a.zero
s : ℝ
hs : 1 < s
⊢ ∑ i ∈ Finset.range 0, (1 / ↑(i + 1) ^ s - 1 / (↑(i + 1) + 1) ^ s) * ↑(i + 1) =
    ∑ n ∈ Finset.range 0, 1 / (↑n + 1) ^ s - ↑0 / (↑0 + 1) ^ s

Tactic:
simp

Result:
no goals

Proof state:
case e_a.e_a.succ.e_a
s : ℝ
hs : 1 < s
N : ℕ
hN :
  ∑ i ∈ Finset.range N, (1 / ↑(i + 1) ^ s - 1 / (↑(i + 1) + 1) ^ s) * ↑(i + 1) =
    ∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s
⊢ -(↑N / (↑N + 1) ^ s) + (1 / (↑N + 1) ^ s + -(1 / (↑N + (1 + 1)) ^ s)) * (↑N + 1) =
    1 / (↑N + 1) ^ s + -((↑N + 1) / (↑N + (1 + 1)) ^ s)

Tactic:
ring_nf

Result:
no goals

Proof state:
case e_a.zero
s : ℝ
hs : 1 < s
⊢ ∑ x ∈ Finset.range 0, 1 / (s - 1) * (1 / ↑(x + 1) ^ (s - 1) - 1 / (↑(x + 1) + 1) ^ (s - 1)) =
    1 / (s - 1) * (1 - 1 / (↑0 + 1) ^ (s - 1))

Tactic:
simp

Result:
no goals

Proof state:
case e_a.e_a.succ
s : ℝ
hs : 1 < s
N : ℕ
hN :
  ∑ i ∈ Finset.range N, (1 / ↑(i + 1) ^ s - 1 / (↑(i + 1) + 1) ^ s) * ↑(i + 1) =
    ∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s
⊢ ∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s +
      (-(↑N / (↑N + 1) ^ s) + (1 / (↑N + 1) ^ s + -(1 / (↑N + (1 + 1)) ^ s)) * (↑N + 1)) =
    ∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s + (1 / (↑N + 1) ^ s + -((↑N + 1) / (↑N + (1 + 1)) ^ s))

Tactic:
congr 1

Result:
case e_a.e_a.succ.e_a
s : ℝ
hs : 1 < s
N : ℕ
hN :
  ∑ i ∈ Finset.range N, (1 / ↑(i + 1) ^ s - 1 / (↑(i + 1) + 1) ^ s) * ↑(i + 1) =
    ∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s
⊢ -(↑N / (↑N + 1) ^ s) + (1 / (↑N + 1) ^ s + -(1 / (↑N + (1 + 1)) ^ s)) * (↑N + 1) =
    1 / (↑N + 1) ^ s + -((↑N + 1) / (↑N + (1 + 1)) ^ s)

Proof state:
N : ℕ
s : ℝ
hs : 1 < s
n : ℕ
⊢ 0 < n + 1

Tactic:
simp

Result:
no goals

Proof state:
N : ℕ
s : ℝ
hs : 1 < s
⊢ ∑ n ∈ Finset.range N, term (n + 1) s =
    1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1)) - 1 / s * (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s)

Tactic:
conv => enter [1, 2, n]; rw [term_of_lt (by simp) hs]

Result:
N : ℕ
s : ℝ
hs : 1 < s
⊢ ∑ n ∈ Finset.range N,
      (1 / (s - 1) * (1 / ↑(n + 1) ^ (s - 1) - 1 / (↑(n + 1) + 1) ^ (s - 1)) -
        ↑(n + 1) / s * (1 / ↑(n + 1) ^ s - 1 / (↑(n + 1) + 1) ^ s)) =
    1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1)) - 1 / s * (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s)

Proof state:
N : ℕ
s : ℝ
hs : 1 < s
⊢ ∑ x ∈ Finset.range N, 1 / (s - 1) * (1 / ↑(x + 1) ^ (s - 1) - 1 / (↑(x + 1) + 1) ^ (s - 1)) -
      ∑ x ∈ Finset.range N, ↑(x + 1) / s * (1 / ↑(x + 1) ^ s - 1 / (↑(x + 1) + 1) ^ s) =
    1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1)) - 1 / s * (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s)

Tactic:
congr 1

Result:
case e_a
N : ℕ
s : ℝ
hs : 1 < s
⊢ ∑ x ∈ Finset.range N, 1 / (s - 1) * (1 / ↑(x + 1) ^ (s - 1) - 1 / (↑(x + 1) + 1) ^ (s - 1)) =
    1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1))

case e_a
N : ℕ
s : ℝ
hs : 1 < s
⊢ ∑ x ∈ Finset.range N, ↑(x + 1) / s * (1 / ↑(x + 1) ^ s - 1 / (↑(x + 1) + 1) ^ s) =
    1 / s * (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s)

Proof state:
case e_a.e_a.succ
s : ℝ
hs : 1 < s
N : ℕ
hN :
  ∑ i ∈ Finset.range N, (1 / ↑(i + 1) ^ s - 1 / (↑(i + 1) + 1) ^ s) * ↑(i + 1) =
    ∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s
⊢ ∑ i ∈ Finset.range (N + 1), (1 / ↑(i + 1) ^ s - 1 / (↑(i + 1) + 1) ^ s) * ↑(i + 1) =
    ∑ n ∈ Finset.range (N + 1), 1 / (↑n + 1) ^ s - ↑(N + 1) / (↑(N + 1) + 1) ^ s

Tactic:
simp_rw [Finset.sum_range_succ, hN, Nat.cast_add_one, sub_eq_add_neg, add_assoc]

Result:
case e_a.e_a.succ
s : ℝ
hs : 1 < s
N : ℕ
hN :
  ∑ i ∈ Finset.range N, (1 / ↑(i + 1) ^ s - 1 / (↑(i + 1) + 1) ^ s) * ↑(i + 1) =
    ∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s
⊢ ∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s +
      (-(↑N / (↑N + 1) ^ s) + (1 / (↑N + 1) ^ s + -(1 / (↑N + (1 + 1)) ^ s)) * (↑N + 1)) =
    ∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s + (1 / (↑N + 1) ^ s + -((↑N + 1) / (↑N + (1 + 1)) ^ s))