awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ term n s =
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1)) -
      (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
have calc : term n s = ∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, (x - (↑n : ℝ)) / x ^ (s + 1)
Tactic: calc term n s
    _ = ∫ x : ℝ in n..(n + 1), (x - n) / x ^ (s + 1) := by rfl
    _ = ∫ x : ℝ in n..(n + 1), (x ^ (-s) - n * x ^ (-(s + 1))) := by
      refine intervalIntegral.integral_congr (fun x hx ↦ ?_)
      rw [sub_div, rpow_add_one (hv x hx).ne', mul_comm, ← div_div, div_self (hv x hx).ne',
        rpow_neg (hv x hx).le, rpow_neg (hv x hx).le, one_div, rpow_add_one (hv x hx).ne', mul_comm,
        div_eq_mul_inv]
    _ = (∫ x : ℝ in n..(n + 1), x ^ (-s)) - n * (∫ x : ℝ in n..(n + 1), x ^ (-(s + 1))) := by
      rw [intervalIntegral.integral_sub, intervalIntegral.integral_const_mul] <;>
      [skip; apply IntervalIntegrable.const_mul] <;>
      · refine intervalIntegral.intervalIntegrable_rpow (Or.inr <| notMem_uIcc_of_lt ?_ ?_)
        · exact_mod_cast hn
        · linarith
    _ = 1 / (s - 1) * (1 / n ^ (s - 1) - 1 / (n + 1) ^ (s - 1))
          - n / s * (1 / n ^ s - 1 / (n + 1) ^ s) := by
      have : 0 ∉ uIcc (n : ℝ) (n + 1) := (lt_irrefl _ <| hv _ ·)
      rw [integral_rpow (Or.inr ⟨by linarith, this⟩), integral_rpow (Or.inr ⟨by linarith, this⟩)]
      congr 1
      · rw [show -s + 1 = -(s - 1) by ring, div_neg, ← neg_div, mul_comm, mul_one_div, neg_sub,
          rpow_neg (Nat.cast_nonneg _), one_div, rpow_neg (by linarith), one_div]
      · rw [show -(s + 1) + 1 = -s by ring, div_neg, ← neg_div, neg_sub, div_mul_eq_mul_div,
          mul_div_assoc, rpow_neg (Nat.cast_nonneg _), one_div, rpow_neg (by linarith), one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
calc : term n s = ∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, (x - (↑n : ℝ)) / x ^ (s + 1)
⊢ term n s =
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1)) -
      (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
have calc₁ : Eq (α := ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, (x - (↑n : ℝ)) / x ^ (s + 1))
  (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1)))
Tactic: calc term n s
    _ = ∫ x : ℝ in n..(n + 1), (x - n) / x ^ (s + 1) := by rfl
    _ = ∫ x : ℝ in n..(n + 1), (x ^ (-s) - n * x ^ (-(s + 1))) := by
      refine intervalIntegral.integral_congr (fun x hx ↦ ?_)
      rw [sub_div, rpow_add_one (hv x hx).ne', mul_comm, ← div_div, div_self (hv x hx).ne',
        rpow_neg (hv x hx).le, rpow_neg (hv x hx).le, one_div, rpow_add_one (hv x hx).ne', mul_comm,
        div_eq_mul_inv]
    _ = (∫ x : ℝ in n..(n + 1), x ^ (-s)) - n * (∫ x : ℝ in n..(n + 1), x ^ (-(s + 1))) := by
      rw [intervalIntegral.integral_sub, intervalIntegral.integral_const_mul] <;>
      [skip; apply IntervalIntegrable.const_mul] <;>
      · refine intervalIntegral.intervalIntegrable_rpow (Or.inr <| notMem_uIcc_of_lt ?_ ?_)
        · exact_mod_cast hn
        · linarith
    _ = 1 / (s - 1) * (1 / n ^ (s - 1) - 1 / (n + 1) ^ (s - 1))
          - n / s * (1 / n ^ s - 1 / (n + 1) ^ s) := by
      have : 0 ∉ uIcc (n : ℝ) (n + 1) := (lt_irrefl _ <| hv _ ·)
      rw [integral_rpow (Or.inr ⟨by linarith, this⟩), integral_rpow (Or.inr ⟨by linarith, this⟩)]
      congr 1
      · rw [show -s + 1 = -(s - 1) by ring, div_neg, ← neg_div, mul_comm, mul_one_div, neg_sub,
          rpow_neg (Nat.cast_nonneg _), one_div, rpow_neg (by linarith), one_div]
      · rw [show -(s + 1) + 1 = -s by ring, div_neg, ← neg_div, neg_sub, div_mul_eq_mul_div,
          mul_div_assoc, rpow_neg (Nat.cast_nonneg _), one_div, rpow_neg (by linarith), one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
calc : term n s = ∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, (x - (↑n : ℝ)) / x ^ (s + 1)
calc₁ :
  Eq (α := ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, (x - (↑n : ℝ)) / x ^ (s + 1))
    (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1)))
⊢ term n s =
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1)) -
      (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
have calc₂ : ∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1)) =
  (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, x ^ (-s)) -
    HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, x ^ (-(s + 1)))
Tactic: calc term n s
    _ = ∫ x : ℝ in n..(n + 1), (x - n) / x ^ (s + 1) := by rfl
    _ = ∫ x : ℝ in n..(n + 1), (x ^ (-s) - n * x ^ (-(s + 1))) := by
      refine intervalIntegral.integral_congr (fun x hx ↦ ?_)
      rw [sub_div, rpow_add_one (hv x hx).ne', mul_comm, ← div_div, div_self (hv x hx).ne',
        rpow_neg (hv x hx).le, rpow_neg (hv x hx).le, one_div, rpow_add_one (hv x hx).ne', mul_comm,
        div_eq_mul_inv]
    _ = (∫ x : ℝ in n..(n + 1), x ^ (-s)) - n * (∫ x : ℝ in n..(n + 1), x ^ (-(s + 1))) := by
      rw [intervalIntegral.integral_sub, intervalIntegral.integral_const_mul] <;>
      [skip; apply IntervalIntegrable.const_mul] <;>
      · refine intervalIntegral.intervalIntegrable_rpow (Or.inr <| notMem_uIcc_of_lt ?_ ?_)
        · exact_mod_cast hn
        · linarith
    _ = 1 / (s - 1) * (1 / n ^ (s - 1) - 1 / (n + 1) ^ (s - 1))
          - n / s * (1 / n ^ s - 1 / (n + 1) ^ s) := by
      have : 0 ∉ uIcc (n : ℝ) (n + 1) := (lt_irrefl _ <| hv _ ·)
      rw [integral_rpow (Or.inr ⟨by linarith, this⟩), integral_rpow (Or.inr ⟨by linarith, this⟩)]
      congr 1
      · rw [show -s + 1 = -(s - 1) by ring, div_neg, ← neg_div, mul_comm, mul_one_div, neg_sub,
          rpow_neg (Nat.cast_nonneg _), one_div, rpow_neg (by linarith), one_div]
      · rw [show -(s + 1) + 1 = -s by ring, div_neg, ← neg_div, neg_sub, div_mul_eq_mul_div,
          mul_div_assoc, rpow_neg (Nat.cast_nonneg _), one_div, rpow_neg (by linarith), one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
calc : term n s = ∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, (x - (↑n : ℝ)) / x ^ (s + 1)
calc₁ :
  Eq (α := ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, (x - (↑n : ℝ)) / x ^ (s + 1))
    (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1)))
calc₂ :
  ∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1)) =
    (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, x ^ (-s)) -
      HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, x ^ (-(s + 1)))
⊢ term n s =
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1)) -
      (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
have calc₃ : (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, x ^ (-s)) -
    HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, x ^ (-(s + 1))) =
  1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1)) -
    (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
Tactic: calc term n s
    _ = ∫ x : ℝ in n..(n + 1), (x - n) / x ^ (s + 1) := by rfl
    _ = ∫ x : ℝ in n..(n + 1), (x ^ (-s) - n * x ^ (-(s + 1))) := by
      refine intervalIntegral.integral_congr (fun x hx ↦ ?_)
      rw [sub_div, rpow_add_one (hv x hx).ne', mul_comm, ← div_div, div_self (hv x hx).ne',
        rpow_neg (hv x hx).le, rpow_neg (hv x hx).le, one_div, rpow_add_one (hv x hx).ne', mul_comm,
        div_eq_mul_inv]
    _ = (∫ x : ℝ in n..(n + 1), x ^ (-s)) - n * (∫ x : ℝ in n..(n + 1), x ^ (-(s + 1))) := by
      rw [intervalIntegral.integral_sub, intervalIntegral.integral_const_mul] <;>
      [skip; apply IntervalIntegrable.const_mul] <;>
      · refine intervalIntegral.intervalIntegrable_rpow (Or.inr <| notMem_uIcc_of_lt ?_ ?_)
        · exact_mod_cast hn
        · linarith
    _ = 1 / (s - 1) * (1 / n ^ (s - 1) - 1 / (n + 1) ^ (s - 1))
          - n / s * (1 / n ^ s - 1 / (n + 1) ^ s) := by
      have : 0 ∉ uIcc (n : ℝ) (n + 1) := (lt_irrefl _ <| hv _ ·)
      rw [integral_rpow (Or.inr ⟨by linarith, this⟩), integral_rpow (Or.inr ⟨by linarith, this⟩)]
      congr 1
      · rw [show -s + 1 = -(s - 1) by ring, div_neg, ← neg_div, mul_comm, mul_one_div, neg_sub,
          rpow_neg (Nat.cast_nonneg _), one_div, rpow_neg (by linarith), one_div]
      · rw [show -(s + 1) + 1 = -s by ring, div_neg, ← neg_div, neg_sub, div_mul_eq_mul_div,
          mul_div_assoc, rpow_neg (Nat.cast_nonneg _), one_div, rpow_neg (by linarith), one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
N : ℕ
s : ℝ
hs : 1 < s
| ∑ n ∈ Finset.range N, term (n + 1) s =
    1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ (s - 1)) -
      1 / s *
        (∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s)
have h : ∀ (n : ℕ), term (n + 1) s
Tactic: enter [1, 2, n]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
N : ℕ
s : ℝ
hs : 1 < s
n : ℕ
| term (n + 1) s
have h : 1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑(n + 1) : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1 ^ (s - 1)) -
  (↑(n + 1) : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑(n + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1 ^ s)
Tactic: rw [term_of_lt (by simp) hs]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
N : ℕ
s : ℝ
hs : 1 < s
| ∑ n ∈ Finset.range N, term (n + 1) s =
    1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ (s - 1)) -
      1 / s *
        (∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s)
have h : ∀ (n : ℕ),
  1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑(n + 1) : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1 ^ (s - 1)) -
    (↑(n + 1) : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑(n + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1 ^ s)
Tactic: enter [1, 2, n]; rw [term_of_lt (by simp) hs]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
N : ℕ
s : ℝ
hs : 1 < s
⊢ ∑ n ∈ Finset.range N, term (n + 1) s =
    1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ (s - 1)) -
      1 / s *
        (∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s)
have conv : ∑ n ∈ Finset.range N,
    (1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑(n + 1) : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1 ^ (s - 1)) -
      (↑(n + 1) : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑(n + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1 ^ s)) =
  1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ (s - 1)) -
    1 / s * (∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s)
Tactic: conv => enter [1, 2, n]; rw [term_of_lt (by simp) hs]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
N : ℕ
s : ℝ
hs : 1 < s
⊢ ∑ n ∈ Finset.range N,
      (1 / (s - 1) *
          (1 / HPow.hPow (α := ℝ) (↑(n + 1) : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1 ^ (s - 1)) -
        (↑(n + 1) : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑(n + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1 ^ s)) =
    1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ (s - 1)) -
      1 / s *
        (∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s)
have rw : HSub.hSub (α := ℝ)
    (∑ x ∈ Finset.range N,
      1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑(x + 1) : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑(x + 1) : ℝ) 1 ^ (s - 1)))
    (∑ x ∈ Finset.range N,
      (↑(x + 1) : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑(x + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(x + 1) : ℝ) 1 ^ s)) =
  1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ (s - 1)) -
    1 / s * (∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s)
Tactic: rw [Finset.sum_sub_distrib]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
N : ℕ
s : ℝ
hs : 1 < s
⊢ HSub.hSub (α := ℝ)
      (∑ x ∈ Finset.range N,
        1 / (s - 1) *
          (1 / HPow.hPow (α := ℝ) (↑(x + 1) : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑(x + 1) : ℝ) 1 ^ (s - 1)))
      (∑ x ∈ Finset.range N,
        (↑(x + 1) : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑(x + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(x + 1) : ℝ) 1 ^ s)) =
    1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ (s - 1)) -
      1 / s *
        (∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s)
have e_a : ∑ x ∈ Finset.range N,
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑(x + 1) : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑(x + 1) : ℝ) 1 ^ (s - 1)) =
  1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ (s - 1))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
N : ℕ
s : ℝ
hs : 1 < s
e_a :
  ∑ x ∈ Finset.range N,
      1 / (s - 1) *
        (1 / HPow.hPow (α := ℝ) (↑(x + 1) : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑(x + 1) : ℝ) 1 ^ (s - 1)) =
    1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ (s - 1))
⊢ HSub.hSub (α := ℝ)
      (∑ x ∈ Finset.range N,
        1 / (s - 1) *
          (1 / HPow.hPow (α := ℝ) (↑(x + 1) : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑(x + 1) : ℝ) 1 ^ (s - 1)))
      (∑ x ∈ Finset.range N,
        (↑(x + 1) : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑(x + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(x + 1) : ℝ) 1 ^ s)) =
    1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ (s - 1)) -
      1 / s *
        (∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s)
have e_a₁ : ∑ x ∈ Finset.range N,
    (↑(x + 1) : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑(x + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(x + 1) : ℝ) 1 ^ s) =
  1 / s * (∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
s : ℝ
hs : 1 < s
N : ℕ
hN :
  ∑ x ∈ Finset.range N,
      1 / (s - 1) *
        (1 / HPow.hPow (α := ℝ) (↑(x + 1) : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑(x + 1) : ℝ) 1 ^ (s - 1)) =
    1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ (s - 1))
⊢ ∑ x ∈ Finset.range (N + 1),
      1 / (s - 1) *
        (1 / HPow.hPow (α := ℝ) (↑(x + 1) : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑(x + 1) : ℝ) 1 ^ (s - 1)) =
    1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑(N + 1) : ℝ) 1 ^ (s - 1))
have e_a : 1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ (s - 1)) +
    1 / (s - 1) * (1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ (s - 1) - 1 / (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 + 1) ^ (s - 1)) =
  1 / (s - 1) * (1 - 1 / (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 + 1) ^ (s - 1))
Tactic: rw [Finset.sum_range_succ, hN, Nat.cast_add_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
N : ℕ
s : ℝ
hs : 1 < s
⊢ ∑ x ∈ Finset.range N,
      1 / (s - 1) *
        (1 / HPow.hPow (α := ℝ) (↑(x + 1) : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑(x + 1) : ℝ) 1 ^ (s - 1)) =
    1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ (s - 1))
have e_a : ∑ x ∈ Finset.range 0,
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑(x + 1) : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑(x + 1) : ℝ) 1 ^ (s - 1)) =
  1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1 ^ (s - 1))
Tactic: induction N with
    | zero => simp
    | succ N hN =>
      rw [Finset.sum_range_succ, hN, Nat.cast_add_one]
      ring_nf
Cleared hypotheses: N
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
N : ℕ
s : ℝ
hs : 1 < s
e_a :
  ∑ x ∈ Finset.range 0,
      1 / (s - 1) *
        (1 / HPow.hPow (α := ℝ) (↑(x + 1) : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑(x + 1) : ℝ) 1 ^ (s - 1)) =
    1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1 ^ (s - 1))
⊢ ∑ x ∈ Finset.range N,
      1 / (s - 1) *
        (1 / HPow.hPow (α := ℝ) (↑(x + 1) : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑(x + 1) : ℝ) 1 ^ (s - 1)) =
    1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ (s - 1))
have e_a₁ : ∀ (N : ℕ)
  (hN :
    ∑ x ∈ Finset.range N,
        1 / (s - 1) *
          (1 / HPow.hPow (α := ℝ) (↑(x + 1) : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑(x + 1) : ℝ) 1 ^ (s - 1)) =
      1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ (s - 1))),
  ∑ x ∈ Finset.range (N + 1),
      1 / (s - 1) *
        (1 / HPow.hPow (α := ℝ) (↑(x + 1) : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑(x + 1) : ℝ) 1 ^ (s - 1)) =
    1 / (s - 1) * (1 - 1 / HAdd.hAdd (α := ℝ) (↑(N + 1) : ℝ) 1 ^ (s - 1))
Tactic: induction N with
    | zero => simp
    | succ N hN =>
      rw [Finset.sum_range_succ, hN, Nat.cast_add_one]
      ring_nf
Cleared hypotheses: N
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
N : ℕ
s : ℝ
hs : 1 < s
⊢ ∑ x ∈ Finset.range N,
      (↑(x + 1) : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑(x + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(x + 1) : ℝ) 1 ^ s) =
    1 / s * (∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s)
have e_a : (∑ i ∈ Finset.range N,
      (1 / HPow.hPow (α := ℝ) (↑(i + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(i + 1) : ℝ) 1 ^ s) * (↑(i + 1) : ℝ)) *
    s⁻¹ =
  (∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s) * s⁻¹
Tactic: simp_rw [mul_comm (_ / _), ← mul_div_assoc, div_eq_mul_inv _ s, ← Finset.sum_mul, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
N : ℕ
s : ℝ
hs : 1 < s
⊢ (∑ i ∈ Finset.range N,
        (1 / HPow.hPow (α := ℝ) (↑(i + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(i + 1) : ℝ) 1 ^ s) * (↑(i + 1) : ℝ)) *
      s⁻¹ =
    (∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s) * s⁻¹
have e_a : ∑ i ∈ Finset.range N,
    (1 / HPow.hPow (α := ℝ) (↑(i + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(i + 1) : ℝ) 1 ^ s) * (↑(i + 1) : ℝ) =
  ∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
s : ℝ
hs : 1 < s
N : ℕ
hN :
  ∑ i ∈ Finset.range N,
      (1 / HPow.hPow (α := ℝ) (↑(i + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(i + 1) : ℝ) 1 ^ s) * (↑(i + 1) : ℝ) =
    ∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s
⊢ ∑ i ∈ Finset.range (N + 1),
      (1 / HPow.hPow (α := ℝ) (↑(i + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(i + 1) : ℝ) 1 ^ s) * (↑(i + 1) : ℝ) =
    ∑ n ∈ Finset.range (N + 1), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s -
      (↑(N + 1) : ℝ) / HAdd.hAdd (α := ℝ) (↑(N + 1) : ℝ) 1 ^ s
have e_a : ∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s +
    (-((↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s) +
      (1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s + -(1 / ((↑N : ℝ) + HAdd.hAdd (α := ℝ) 1 1) ^ s)) *
        HAdd.hAdd (α := ℝ) (↑N : ℝ) 1) =
  ∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s +
    (1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s + -(HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 / ((↑N : ℝ) + HAdd.hAdd (α := ℝ) 1 1) ^ s))
Tactic: simp_rw [Finset.sum_range_succ, hN, Nat.cast_add_one, sub_eq_add_neg, add_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
s : ℝ
hs : 1 < s
N : ℕ
hN :
  ∑ i ∈ Finset.range N,
      (1 / HPow.hPow (α := ℝ) (↑(i + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(i + 1) : ℝ) 1 ^ s) * (↑(i + 1) : ℝ) =
    ∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s
⊢ ∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s +
      (-((↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s) +
        (1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s + -(1 / ((↑N : ℝ) + HAdd.hAdd (α := ℝ) 1 1) ^ s)) *
          HAdd.hAdd (α := ℝ) (↑N : ℝ) 1) =
    ∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s +
      (1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s +
        -(HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 / ((↑N : ℝ) + HAdd.hAdd (α := ℝ) 1 1) ^ s))
have e_a : -((↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s) +
    (1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s + -(1 / ((↑N : ℝ) + HAdd.hAdd (α := ℝ) 1 1) ^ s)) *
      HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 =
  1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s + -(HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 / ((↑N : ℝ) + HAdd.hAdd (α := ℝ) 1 1) ^ s)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
N : ℕ
s : ℝ
hs : 1 < s
⊢ ∑ i ∈ Finset.range N,
      (1 / HPow.hPow (α := ℝ) (↑(i + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(i + 1) : ℝ) 1 ^ s) * (↑(i + 1) : ℝ) =
    ∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s
have e_a : ∑ i ∈ Finset.range 0,
    (1 / HPow.hPow (α := ℝ) (↑(i + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(i + 1) : ℝ) 1 ^ s) * (↑(i + 1) : ℝ) =
  ∑ n ∈ Finset.range 0, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑0 : ℝ) / HAdd.hAdd (α := ℝ) (↑0 : ℝ) 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
Cleared hypotheses: N
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
N : ℕ
s : ℝ
hs : 1 < s
e_a :
  ∑ i ∈ Finset.range 0,
      (1 / HPow.hPow (α := ℝ) (↑(i + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(i + 1) : ℝ) 1 ^ s) * (↑(i + 1) : ℝ) =
    ∑ n ∈ Finset.range 0, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑0 : ℝ) / HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1 ^ s
⊢ ∑ i ∈ Finset.range N,
      (1 / HPow.hPow (α := ℝ) (↑(i + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(i + 1) : ℝ) 1 ^ s) * (↑(i + 1) : ℝ) =
    ∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s
have e_a₁ : ∀ (N : ℕ)
  (hN :
    ∑ i ∈ Finset.range N,
        (1 / HPow.hPow (α := ℝ) (↑(i + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(i + 1) : ℝ) 1 ^ s) * (↑(i + 1) : ℝ) =
      ∑ n ∈ Finset.range N, 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - (↑N : ℝ) / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ^ s),
  ∑ i ∈ Finset.range (N + 1),
      (1 / HPow.hPow (α := ℝ) (↑(i + 1) : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑(i + 1) : ℝ) 1 ^ s) * (↑(i + 1) : ℝ) =
    ∑ n ∈ Finset.range (N + 1), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s -
      (↑(N + 1) : ℝ) / HAdd.hAdd (α := ℝ) (↑(N + 1) : ℝ) 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
Cleared hypotheses: N
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
s : ℝ
hs : 1 < s
⊢ term_tsum s = 1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s
have ha : HasSum (fun (b : ℕ) ↦ term (b + 1) s) (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
Tactic: apply HasSum.tsum_eq
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
s : ℝ
hs : 1 < s
⊢ HasSum (fun (b : ℕ) ↦ term (b + 1) s) (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
have ha : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, term (i + 1) s) atTop
  (𝓝 (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s))
Tactic: rw [hasSum_iff_tendsto_nat_of_nonneg (fun n ↦ term_nonneg (n + 1) s)]