awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
n p : ℕ
f : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
f' : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli' i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
hle : 1 ≤ n + 1
hne : HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1 ≠ 0
h1 :
  ∀ (r : ℚ),
    r * (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ / (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) =
      r * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
h2 : f 1 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ = 1 / 2 * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
⊢ Eq (α := ℚ) (∑ k ∈ Ico 1 n.succ, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ) (∑ i ∈ range p.succ.succ, f' i)
have this : Eq (α := ℚ)
  (∑ i ∈ range p,
    bernoulli (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ))
  (∑ i ∈ range p,
    bernoulli' (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ))
Tactic: have :
    (∑ i ∈ range p, bernoulli (i + 2) * (p + 2).choose (i + 2) * (n : ℚ) ^ (p - i) / ↑(p + 2)) =
      ∑ i ∈ range p, bernoulli' (i + 2) * (p + 2).choose (i + 2) * (n : ℚ) ^ (p - i) / ↑(p + 2) :=
    sum_congr rfl fun i _ => by rw [bernoulli_eq_bernoulli'_of_ne_one (succ_succ_ne_one i)]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n p : ℕ
f : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
f' : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli' i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
hle : 1 ≤ n + 1
hne : HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1 ≠ 0
h1 :
  ∀ (r : ℚ),
    r * (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ / (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) =
      r * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
h2 : f 1 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ = 1 / 2 * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
this :
  Eq (α := ℚ)
    (∑ i ∈ range p,
      bernoulli (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ))
    (∑ i ∈ range p,
      bernoulli' (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ))
⊢ ∑ k ∈ range n.succ, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ =
    ∑ k ∈ range n, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
have rw : ∑ x ∈ range n, HPow.hPow (α := ℚ) (↑x : ℚ) p.succ + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ =
  ∑ k ∈ range n, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
Tactic: rw [sum_range_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n p : ℕ
f : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
f' : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli' i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
hle : 1 ≤ n + 1
hne : HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1 ≠ 0
h1 :
  ∀ (r : ℚ),
    r * (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ / (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) =
      r * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
h2 : f 1 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ = 1 / 2 * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
this :
  Eq (α := ℚ)
    (∑ i ∈ range p,
      bernoulli (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ))
    (∑ i ∈ range p,
      bernoulli' (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ))
⊢ ∑ i ∈ range p, f i.succ.succ + (f 1 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ) + f 0 =
    ∑ i ∈ range p, f i.succ.succ + 1 / 2 * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ + f 0
have rw : ∑ i ∈ range p, f i.succ.succ + 1 / 2 * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ + f 0 =
  ∑ i ∈ range p, f i.succ.succ + 1 / 2 * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ + f 0
Tactic: rw [h2]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n p : ℕ
f : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
f' : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli' i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
hle : 1 ≤ n + 1
hne : HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1 ≠ 0
h1 :
  ∀ (r : ℚ),
    r * (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ / (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) =
      r * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
h2 : f 1 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ = 1 / 2 * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
this :
  Eq (α := ℚ)
    (∑ i ∈ range p,
      bernoulli (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ))
    (∑ i ∈ range p,
      bernoulli' (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ))
⊢ Eq (α := ℚ) (∑ k ∈ Ico 1 n.succ, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ) (∑ i ∈ range p.succ.succ, f' i)
have replace : Eq (α := ℚ) (∑ k ∈ Ico 1 n.succ, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ)
  (∑ k ∈ range n.succ, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ)
Tactic: calc
    (-- replace sum over `Ico` with sum over `range` and simplify
        ∑ k ∈ Ico 1 n.succ, (k : ℚ) ^ p.succ)
    _ = ∑ k ∈ range n.succ, (k : ℚ) ^ p.succ := by simp [sum_Ico_eq_sub _ hle]
    -- extract the last term of the sum
    _ = (∑ k ∈ range n, (k : ℚ) ^ p.succ) + (n : ℚ) ^ p.succ := by rw [sum_range_succ]
    -- apply the key lemma, `sum_range_pow`
    _ = (∑ i ∈ range p.succ.succ, f i) + (n : ℚ) ^ p.succ := by simp [f, sum_range_pow]
    -- extract the first two terms of the sum
    _ = (∑ i ∈ range p, f i.succ.succ) + f 1 + f 0 + (n : ℚ) ^ p.succ := by
      simp_rw [sum_range_succ']
    _ = (∑ i ∈ range p, f i.succ.succ) + (f 1 + (n : ℚ) ^ p.succ) + f 0 := by ring
    _ = (∑ i ∈ range p, f i.succ.succ) + 1 / 2 * (n : ℚ) ^ p.succ + f 0 := by rw [h2]
    -- convert from `bernoulli` to `bernoulli'`
    _ = (∑ i ∈ range p, f' i.succ.succ) + f' 1 + f' 0 := by
      simpa [f, f', h1, fun i => show i + 2 = i + 1 + 1 from rfl]
    -- rejoin the first two terms of the sum
    _ = ∑ i ∈ range p.succ.succ, f' i := by simp_rw [sum_range_succ']
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n p : ℕ
f : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
f' : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli' i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
hle : 1 ≤ n + 1
hne : HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1 ≠ 0
h1 :
  ∀ (r : ℚ),
    r * (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ / (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) =
      r * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
h2 : f 1 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ = 1 / 2 * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
this :
  Eq (α := ℚ)
    (∑ i ∈ range p,
      bernoulli (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ))
    (∑ i ∈ range p,
      bernoulli' (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ))
replace :
  Eq (α := ℚ) (∑ k ∈ Ico 1 n.succ, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ)
    (∑ k ∈ range n.succ, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ)
⊢ Eq (α := ℚ) (∑ k ∈ Ico 1 n.succ, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ) (∑ i ∈ range p.succ.succ, f' i)
have replace₁ : ∑ k ∈ range n.succ, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ =
  ∑ k ∈ range n, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
Tactic: calc
    (-- replace sum over `Ico` with sum over `range` and simplify
        ∑ k ∈ Ico 1 n.succ, (k : ℚ) ^ p.succ)
    _ = ∑ k ∈ range n.succ, (k : ℚ) ^ p.succ := by simp [sum_Ico_eq_sub _ hle]
    -- extract the last term of the sum
    _ = (∑ k ∈ range n, (k : ℚ) ^ p.succ) + (n : ℚ) ^ p.succ := by rw [sum_range_succ]
    -- apply the key lemma, `sum_range_pow`
    _ = (∑ i ∈ range p.succ.succ, f i) + (n : ℚ) ^ p.succ := by simp [f, sum_range_pow]
    -- extract the first two terms of the sum
    _ = (∑ i ∈ range p, f i.succ.succ) + f 1 + f 0 + (n : ℚ) ^ p.succ := by
      simp_rw [sum_range_succ']
    _ = (∑ i ∈ range p, f i.succ.succ) + (f 1 + (n : ℚ) ^ p.succ) + f 0 := by ring
    _ = (∑ i ∈ range p, f i.succ.succ) + 1 / 2 * (n : ℚ) ^ p.succ + f 0 := by rw [h2]
    -- convert from `bernoulli` to `bernoulli'`
    _ = (∑ i ∈ range p, f' i.succ.succ) + f' 1 + f' 0 := by
      simpa [f, f', h1, fun i => show i + 2 = i + 1 + 1 from rfl]
    -- rejoin the first two terms of the sum
    _ = ∑ i ∈ range p.succ.succ, f' i := by simp_rw [sum_range_succ']
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n p : ℕ
f : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
f' : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli' i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
hle : 1 ≤ n + 1
hne : HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1 ≠ 0
h1 :
  ∀ (r : ℚ),
    r * (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ / (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) =
      r * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
h2 : f 1 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ = 1 / 2 * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
this :
  Eq (α := ℚ)
    (∑ i ∈ range p,
      bernoulli (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ))
    (∑ i ∈ range p,
      bernoulli' (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ))
replace :
  Eq (α := ℚ) (∑ k ∈ Ico 1 n.succ, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ)
    (∑ k ∈ range n.succ, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ)
replace₁ :
  ∑ k ∈ range n.succ, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ =
    ∑ k ∈ range n, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
⊢ Eq (α := ℚ) (∑ k ∈ Ico 1 n.succ, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ) (∑ i ∈ range p.succ.succ, f' i)
have replace₂ : ∑ k ∈ range n, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ =
  ∑ i ∈ range p.succ.succ, f i + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
Tactic: calc
    (-- replace sum over `Ico` with sum over `range` and simplify
        ∑ k ∈ Ico 1 n.succ, (k : ℚ) ^ p.succ)
    _ = ∑ k ∈ range n.succ, (k : ℚ) ^ p.succ := by simp [sum_Ico_eq_sub _ hle]
    -- extract the last term of the sum
    _ = (∑ k ∈ range n, (k : ℚ) ^ p.succ) + (n : ℚ) ^ p.succ := by rw [sum_range_succ]
    -- apply the key lemma, `sum_range_pow`
    _ = (∑ i ∈ range p.succ.succ, f i) + (n : ℚ) ^ p.succ := by simp [f, sum_range_pow]
    -- extract the first two terms of the sum
    _ = (∑ i ∈ range p, f i.succ.succ) + f 1 + f 0 + (n : ℚ) ^ p.succ := by
      simp_rw [sum_range_succ']
    _ = (∑ i ∈ range p, f i.succ.succ) + (f 1 + (n : ℚ) ^ p.succ) + f 0 := by ring
    _ = (∑ i ∈ range p, f i.succ.succ) + 1 / 2 * (n : ℚ) ^ p.succ + f 0 := by rw [h2]
    -- convert from `bernoulli` to `bernoulli'`
    _ = (∑ i ∈ range p, f' i.succ.succ) + f' 1 + f' 0 := by
      simpa [f, f', h1, fun i => show i + 2 = i + 1 + 1 from rfl]
    -- rejoin the first two terms of the sum
    _ = ∑ i ∈ range p.succ.succ, f' i := by simp_rw [sum_range_succ']
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n p : ℕ
f : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
f' : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli' i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
hle : 1 ≤ n + 1
hne : HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1 ≠ 0
h1 :
  ∀ (r : ℚ),
    r * (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ / (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) =
      r * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
h2 : f 1 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ = 1 / 2 * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
this :
  Eq (α := ℚ)
    (∑ i ∈ range p,
      bernoulli (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ))
    (∑ i ∈ range p,
      bernoulli' (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ))
replace :
  Eq (α := ℚ) (∑ k ∈ Ico 1 n.succ, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ)
    (∑ k ∈ range n.succ, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ)
replace₁ :
  ∑ k ∈ range n.succ, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ =
    ∑ k ∈ range n, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
replace₂ :
  ∑ k ∈ range n, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ =
    ∑ i ∈ range p.succ.succ, f i + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
⊢ Eq (α := ℚ) (∑ k ∈ Ico 1 n.succ, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ) (∑ i ∈ range p.succ.succ, f' i)
have replace₃ : ∑ i ∈ range p.succ.succ, f i + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ =
  ∑ i ∈ range p, f i.succ.succ + f 1 + f 0 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
Tactic: calc
    (-- replace sum over `Ico` with sum over `range` and simplify
        ∑ k ∈ Ico 1 n.succ, (k : ℚ) ^ p.succ)
    _ = ∑ k ∈ range n.succ, (k : ℚ) ^ p.succ := by simp [sum_Ico_eq_sub _ hle]
    -- extract the last term of the sum
    _ = (∑ k ∈ range n, (k : ℚ) ^ p.succ) + (n : ℚ) ^ p.succ := by rw [sum_range_succ]
    -- apply the key lemma, `sum_range_pow`
    _ = (∑ i ∈ range p.succ.succ, f i) + (n : ℚ) ^ p.succ := by simp [f, sum_range_pow]
    -- extract the first two terms of the sum
    _ = (∑ i ∈ range p, f i.succ.succ) + f 1 + f 0 + (n : ℚ) ^ p.succ := by
      simp_rw [sum_range_succ']
    _ = (∑ i ∈ range p, f i.succ.succ) + (f 1 + (n : ℚ) ^ p.succ) + f 0 := by ring
    _ = (∑ i ∈ range p, f i.succ.succ) + 1 / 2 * (n : ℚ) ^ p.succ + f 0 := by rw [h2]
    -- convert from `bernoulli` to `bernoulli'`
    _ = (∑ i ∈ range p, f' i.succ.succ) + f' 1 + f' 0 := by
      simpa [f, f', h1, fun i => show i + 2 = i + 1 + 1 from rfl]
    -- rejoin the first two terms of the sum
    _ = ∑ i ∈ range p.succ.succ, f' i := by simp_rw [sum_range_succ']
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n p : ℕ
f : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
f' : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli' i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
hle : 1 ≤ n + 1
hne : HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1 ≠ 0
h1 :
  ∀ (r : ℚ),
    r * (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ / (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) =
      r * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
h2 : f 1 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ = 1 / 2 * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
this :
  Eq (α := ℚ)
    (∑ i ∈ range p,
      bernoulli (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ))
    (∑ i ∈ range p,
      bernoulli' (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ))
replace :
  Eq (α := ℚ) (∑ k ∈ Ico 1 n.succ, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ)
    (∑ k ∈ range n.succ, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ)
replace₁ :
  ∑ k ∈ range n.succ, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ =
    ∑ k ∈ range n, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
replace₂ :
  ∑ k ∈ range n, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ =
    ∑ i ∈ range p.succ.succ, f i + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
replace₃ :
  ∑ i ∈ range p.succ.succ, f i + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ =
    ∑ i ∈ range p, f i.succ.succ + f 1 + f 0 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
⊢ Eq (α := ℚ) (∑ k ∈ Ico 1 n.succ, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ) (∑ i ∈ range p.succ.succ, f' i)
have replace₄ : ∑ i ∈ range p, f i.succ.succ + f 1 + f 0 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ =
  ∑ i ∈ range p, f i.succ.succ + (f 1 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ) + f 0
Tactic: calc
    (-- replace sum over `Ico` with sum over `range` and simplify
        ∑ k ∈ Ico 1 n.succ, (k : ℚ) ^ p.succ)
    _ = ∑ k ∈ range n.succ, (k : ℚ) ^ p.succ := by simp [sum_Ico_eq_sub _ hle]
    -- extract the last term of the sum
    _ = (∑ k ∈ range n, (k : ℚ) ^ p.succ) + (n : ℚ) ^ p.succ := by rw [sum_range_succ]
    -- apply the key lemma, `sum_range_pow`
    _ = (∑ i ∈ range p.succ.succ, f i) + (n : ℚ) ^ p.succ := by simp [f, sum_range_pow]
    -- extract the first two terms of the sum
    _ = (∑ i ∈ range p, f i.succ.succ) + f 1 + f 0 + (n : ℚ) ^ p.succ := by
      simp_rw [sum_range_succ']
    _ = (∑ i ∈ range p, f i.succ.succ) + (f 1 + (n : ℚ) ^ p.succ) + f 0 := by ring
    _ = (∑ i ∈ range p, f i.succ.succ) + 1 / 2 * (n : ℚ) ^ p.succ + f 0 := by rw [h2]
    -- convert from `bernoulli` to `bernoulli'`
    _ = (∑ i ∈ range p, f' i.succ.succ) + f' 1 + f' 0 := by
      simpa [f, f', h1, fun i => show i + 2 = i + 1 + 1 from rfl]
    -- rejoin the first two terms of the sum
    _ = ∑ i ∈ range p.succ.succ, f' i := by simp_rw [sum_range_succ']
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n p : ℕ
f : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
f' : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli' i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
hle : 1 ≤ n + 1
hne : HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1 ≠ 0
h1 :
  ∀ (r : ℚ),
    r * (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ / (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) =
      r * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
h2 : f 1 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ = 1 / 2 * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
this :
  Eq (α := ℚ)
    (∑ i ∈ range p,
      bernoulli (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ))
    (∑ i ∈ range p,
      bernoulli' (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ))
replace :
  Eq (α := ℚ) (∑ k ∈ Ico 1 n.succ, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ)
    (∑ k ∈ range n.succ, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ)
replace₁ :
  ∑ k ∈ range n.succ, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ =
    ∑ k ∈ range n, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
replace₂ :
  ∑ k ∈ range n, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ =
    ∑ i ∈ range p.succ.succ, f i + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
replace₃ :
  ∑ i ∈ range p.succ.succ, f i + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ =
    ∑ i ∈ range p, f i.succ.succ + f 1 + f 0 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
replace₄ :
  ∑ i ∈ range p, f i.succ.succ + f 1 + f 0 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ =
    ∑ i ∈ range p, f i.succ.succ + (f 1 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ) + f 0
⊢ Eq (α := ℚ) (∑ k ∈ Ico 1 n.succ, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ) (∑ i ∈ range p.succ.succ, f' i)
have replace₅ : ∑ i ∈ range p, f i.succ.succ + (f 1 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ) + f 0 =
  ∑ i ∈ range p, f i.succ.succ + 1 / 2 * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ + f 0
Tactic: calc
    (-- replace sum over `Ico` with sum over `range` and simplify
        ∑ k ∈ Ico 1 n.succ, (k : ℚ) ^ p.succ)
    _ = ∑ k ∈ range n.succ, (k : ℚ) ^ p.succ := by simp [sum_Ico_eq_sub _ hle]
    -- extract the last term of the sum
    _ = (∑ k ∈ range n, (k : ℚ) ^ p.succ) + (n : ℚ) ^ p.succ := by rw [sum_range_succ]
    -- apply the key lemma, `sum_range_pow`
    _ = (∑ i ∈ range p.succ.succ, f i) + (n : ℚ) ^ p.succ := by simp [f, sum_range_pow]
    -- extract the first two terms of the sum
    _ = (∑ i ∈ range p, f i.succ.succ) + f 1 + f 0 + (n : ℚ) ^ p.succ := by
      simp_rw [sum_range_succ']
    _ = (∑ i ∈ range p, f i.succ.succ) + (f 1 + (n : ℚ) ^ p.succ) + f 0 := by ring
    _ = (∑ i ∈ range p, f i.succ.succ) + 1 / 2 * (n : ℚ) ^ p.succ + f 0 := by rw [h2]
    -- convert from `bernoulli` to `bernoulli'`
    _ = (∑ i ∈ range p, f' i.succ.succ) + f' 1 + f' 0 := by
      simpa [f, f', h1, fun i => show i + 2 = i + 1 + 1 from rfl]
    -- rejoin the first two terms of the sum
    _ = ∑ i ∈ range p.succ.succ, f' i := by simp_rw [sum_range_succ']
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n p : ℕ
⊢ Eq (α := ℚ) (∑ k ∈ Ico 1 (n + 1), HPow.hPow (α := ℚ) (↑k : ℚ) p)
    (∑ i ∈ range (p + 1),
      bernoulli' i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / (↑p.succ : ℚ))
have zero : Eq (α := ℚ) (∑ k ∈ Ico 1 (n + 1), HPow.hPow (α := ℚ) (β := ℕ) (↑k : ℚ) 0)
  (∑ i ∈ range (HAdd.hAdd (α := ℕ) 0 1),
    bernoulli' i * (↑((HAdd.hAdd (α := ℕ) 0 1).choose i) : ℚ) *
        HPow.hPow (α := ℚ) (↑n : ℚ) (HAdd.hAdd (α := ℕ) 0 1 - i) /
      (↑(succ 0) : ℚ))
Tactic: cases p with | zero => simp | succ p =>
  let f i := bernoulli i * p.succ.succ.choose i * (n : ℚ) ^ (p.succ.succ - i) / p.succ.succ
  let f' i := bernoulli' i * p.succ.succ.choose i * (n : ℚ) ^ (p.succ.succ - i) / p.succ.succ
  suffices (∑ k ∈ Ico 1 n.succ, (k : ℚ) ^ p.succ) = ∑ i ∈ range p.succ.succ, f' i by convert!
    this
  -- prove some algebraic facts that will make things easier for us later on
  have hle := Nat.le_add_left 1 n
  have hne : (p + 1 + 1 : ℚ) ≠ 0 := by norm_cast
  have h1 : ∀ r : ℚ, r * (p + 1 + 1) * (n : ℚ) ^ p.succ / (p + 1 + 1 : ℚ) = r * (n : ℚ) ^ p.succ :=
      fun r => by rw [mul_div_right_comm, mul_div_cancel_right₀ _ hne]
  have h2 : f 1 + (n : ℚ) ^ p.succ = 1 / 2 * (n : ℚ) ^ p.succ := by
    simp_rw [f, bernoulli_one, choose_one_right, succ_sub_succ_eq_sub, cast_succ, tsub_zero, h1]
    ring
  have :
    (∑ i ∈ range p, bernoulli (i + 2) * (p + 2).choose (i + 2) * (n : ℚ) ^ (p - i) / ↑(p + 2)) =
      ∑ i ∈ range p, bernoulli' (i + 2) * (p + 2).choose (i + 2) * (n : ℚ) ^ (p - i) / ↑(p + 2) :=
    sum_congr rfl fun i _ => by rw [bernoulli_eq_bernoulli'_of_ne_one (succ_succ_ne_one i)]
  calc
    (-- replace sum over `Ico` with sum over `range` and simplify
        ∑ k ∈ Ico 1 n.succ, (k : ℚ) ^ p.succ)
    _ = ∑ k ∈ range n.succ, (k : ℚ) ^ p.succ := by simp [sum_Ico_eq_sub _ hle]
    -- extract the last term of the sum
    _ = (∑ k ∈ range n, (k : ℚ) ^ p.succ) + (n : ℚ) ^ p.succ := by rw [sum_range_succ]
    -- apply the key lemma, `sum_range_pow`
    _ = (∑ i ∈ range p.succ.succ, f i) + (n : ℚ) ^ p.succ := by simp [f, sum_range_pow]
    -- extract the first two terms of the sum
    _ = (∑ i ∈ range p, f i.succ.succ) + f 1 + f 0 + (n : ℚ) ^ p.succ := by
      simp_rw [sum_range_succ']
    _ = (∑ i ∈ range p, f i.succ.succ) + (f 1 + (n : ℚ) ^ p.succ) + f 0 := by ring
    _ = (∑ i ∈ range p, f i.succ.succ) + 1 / 2 * (n : ℚ) ^ p.succ + f 0 := by rw [h2]
    -- convert from `bernoulli` to `bernoulli'`
    _ = (∑ i ∈ range p, f' i.succ.succ) + f' 1 + f' 0 := by
      simpa [f, f', h1, fun i => show i + 2 = i + 1 + 1 from rfl]
    -- rejoin the first two terms of the sum
    _ = ∑ i ∈ range p.succ.succ, f' i := by simp_rw [sum_range_succ']
Cleared hypotheses: p