awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun (n : ℕ) ↦ bernoulli' n / (↑n ! : ℚ)
this : HSub.hSub (β := ℚ⟦X⟧) B ((evalNegHom : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧) * (exp ℚ - 1) = X * (exp ℚ - 1)
h : exp ℚ - 1 = 0
⊢ bernoulli' n = 0
have h₁ : ∀ (n : ℕ), Eq (α := ℚ) ((coeff n : (a : ℚ⟦X⟧) → ℚ) (exp ℚ - 1) : ℚ) ((coeff n : (a : ℚ⟦X⟧) → ℚ) 0 : ℚ)
Tactic: simp only [PowerSeries.ext_iff, evalNegHom, coeff_X] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun (n : ℕ) ↦ bernoulli' n / (↑n ! : ℚ)
this : HSub.hSub (β := ℚ⟦X⟧) B ((evalNegHom : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧) * (exp ℚ - 1) = X * (exp ℚ - 1)
h :
  ∀ (n : ℕ),
    Eq (α := ℚ) ((coeff n : (a : ℚ⟦X⟧) → ℚ) (HSub.hSub (β := ℚ⟦X⟧) B ((rescale (-1) : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧)) : ℚ)
      (if n = 1 then 1 else 0 : ℚ)
⊢ bernoulli' n = 0
have inl : -bernoulli' n = bernoulli' n
Tactic: apply eq_zero_of_neg_eq
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun (n : ℕ) ↦ bernoulli' n / (↑n ! : ℚ)
this : HSub.hSub (β := ℚ⟦X⟧) B ((evalNegHom : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧) * (exp ℚ - 1) = X * (exp ℚ - 1)
h :
  ∀ (n : ℕ),
    Eq (α := ℚ) ((coeff n : (a : ℚ⟦X⟧) → ℚ) (HSub.hSub (β := ℚ⟦X⟧) B ((rescale (-1) : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧)) : ℚ)
      (if n = 1 then 1 else 0 : ℚ)
⊢ -bernoulli' n = bernoulli' n
have h₁ : Eq (α := ℚ) ((coeff n : (a : ℚ⟦X⟧) → ℚ) (HSub.hSub (β := ℚ⟦X⟧) B ((rescale (-1) : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧)) : ℚ)
  (if n = 1 then 1 else 0 : ℚ)
Tactic: specialize h n
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun (n : ℕ) ↦ bernoulli' n / (↑n ! : ℚ)
this : HSub.hSub (β := ℚ⟦X⟧) B ((evalNegHom : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧) * (exp ℚ - 1) = X * (exp ℚ - 1)
h :
  Eq (α := ℚ) ((coeff n : (a : ℚ⟦X⟧) → ℚ) (HSub.hSub (β := ℚ⟦X⟧) B ((rescale (-1) : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧)) : ℚ)
    (if n = 1 then 1 else 0 : ℚ)
⊢ -bernoulli' n = bernoulli' n
have pos : n = 1 →
  ∀
    (h :
      Eq (α := ℚ)
        ((coeff n : (a : ℚ⟦X⟧) → ℚ) (HSub.hSub (β := ℚ⟦X⟧) B ((rescale (-1) : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧)) : ℚ)
        (1 : ℚ)),
    -bernoulli' n = bernoulli' n
Tactic: split_ifs at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun (n : ℕ) ↦ bernoulli' n / (↑n ! : ℚ)
this : HSub.hSub (β := ℚ⟦X⟧) B ((evalNegHom : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧) * (exp ℚ - 1) = X * (exp ℚ - 1)
h :
  Eq (α := ℚ) ((coeff n : (a : ℚ⟦X⟧) → ℚ) (HSub.hSub (β := ℚ⟦X⟧) B ((rescale (-1) : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧)) : ℚ)
    (if n = 1 then 1 else 0 : ℚ)
pos :
  n = 1 →
    ∀
      (h :
        Eq (α := ℚ)
          ((coeff n : (a : ℚ⟦X⟧) → ℚ) (HSub.hSub (β := ℚ⟦X⟧) B ((rescale (-1) : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧)) : ℚ)
          (1 : ℚ)),
      -bernoulli' n = bernoulli' n
⊢ -bernoulli' n = bernoulli' n
have neg : ¬n = 1 →
  ∀
    (h :
      Eq (α := ℚ)
        ((coeff n : (a : ℚ⟦X⟧) → ℚ) (HSub.hSub (β := ℚ⟦X⟧) B ((rescale (-1) : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧)) : ℚ)
        (0 : ℚ)),
    -bernoulli' n = bernoulli' n
Tactic: split_ifs at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun (n : ℕ) ↦ bernoulli' n / (↑n ! : ℚ)
⊢ bernoulli' n = 0
have suffices : HSub.hSub (β := ℚ⟦X⟧) B ((evalNegHom : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧) * (exp ℚ - 1) = X * (exp ℚ - 1)
Tactic: suffices (B - evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1) by
    rcases mul_eq_mul_right_iff.mp this with h | h <;>
      simp only [PowerSeries.ext_iff, evalNegHom, coeff_X] at h
    · apply eq_zero_of_neg_eq
      specialize h n
      split_ifs at h <;> simp_all [B, h_odd.neg_one_pow, factorial_ne_zero]
    · simpa +decide [Nat.factorial] using h 1
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun (n : ℕ) ↦ bernoulli' n / (↑n ! : ℚ)
⊢ HSub.hSub (β := ℚ⟦X⟧) B ((evalNegHom : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧) * (exp ℚ - 1) = X * (exp ℚ - 1)
have h : B * (exp ℚ - 1) = X * exp ℚ
Tactic: have h : B * (exp ℚ - 1) = X * exp ℚ := by
    simpa [bernoulli'PowerSeries] using bernoulli'PowerSeries_mul_exp_sub_one ℚ
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun (n : ℕ) ↦ bernoulli' n / (↑n ! : ℚ)
h : B * (exp ℚ - 1) = X * exp ℚ
⊢ HSub.hSub (β := ℚ⟦X⟧) B ((evalNegHom : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧) * (exp ℚ - 1) = X * (exp ℚ - 1)
have rw : HMul.hMul (α := ℚ⟦X⟧) ((evalNegHom : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧) (1 - exp ℚ) = -HMul.hMul (α := ℚ⟦X⟧) X 1
Tactic: rw [sub_mul, h, mul_sub X, sub_right_inj, ← neg_sub, mul_neg, neg_eq_iff_eq_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun (n : ℕ) ↦ bernoulli' n / (↑n ! : ℚ)
h : B * (exp ℚ - 1) = X * exp ℚ
⊢ HMul.hMul (α := ℚ⟦X⟧) ((evalNegHom : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧) (1 - exp ℚ) = -HMul.hMul (α := ℚ⟦X⟧) X 1
have suffices : HMul.hMul (α := ℚ⟦X⟧) ((evalNegHom : (a : ℚ⟦X⟧) → ℚ⟦X⟧) (B * (exp ℚ - 1)) : ℚ⟦X⟧) (exp ℚ) =
  HMul.hMul (α := ℚ⟦X⟧) ((evalNegHom : (a : ℚ⟦X⟧) → ℚ⟦X⟧) (X * exp ℚ) : ℚ⟦X⟧) (exp ℚ)
Tactic: suffices evalNegHom (B * (exp ℚ - 1)) * exp ℚ = evalNegHom (X * exp ℚ) * exp ℚ by
    simpa [mul_assoc, sub_mul, mul_comm (evalNegHom (exp ℚ)), exp_mul_exp_neg_eq_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
h_odd : Odd n
hlt : 1 < n
⊢ bernoulli n = 0
have rw : HPow.hPow (α := ℚ) (-1) n * bernoulli' n = 0
Tactic: rw [bernoulli, bernoulli'_eq_zero_of_odd h_odd hlt, mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
h_odd : Odd n
hlt : 1 < n
rw : HPow.hPow (α := ℚ) (-1) n * bernoulli' n = 0
⊢ bernoulli n = 0
have rw₁ : HPow.hPow (α := ℚ) (-1) n * 0 = 0
Tactic: rw [bernoulli, bernoulli'_eq_zero_of_odd h_odd hlt, mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
h_odd : Odd n
hlt : 1 < n
rw : HPow.hPow (α := ℚ) (-1) n * bernoulli' n = 0
rw₁ : HPow.hPow (α := ℚ) (-1) n * 0 = 0
⊢ bernoulli n = 0
have rw₂ : Eq (α := ℚ) 0 0
Tactic: rw [bernoulli, bernoulli'_eq_zero_of_odd h_odd hlt, mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
hn : n ≠ 1
hgt : 1 < n
heven : Even n
⊢ bernoulli n = bernoulli' n
have inr : HPow.hPow (α := ℚ) (-1) n * bernoulli' n = bernoulli' n
Tactic: rw [bernoulli, heven.neg_one_pow, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
hn : n ≠ 1
hgt : 1 < n
heven : Even n
inr : HPow.hPow (α := ℚ) (-1) n * bernoulli' n = bernoulli' n
⊢ bernoulli n = bernoulli' n
have inr₁ : 1 * bernoulli' n = bernoulli' n
Tactic: rw [bernoulli, heven.neg_one_pow, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
hn : n ≠ 1
hgt : 1 < n
heven : Even n
inr : HPow.hPow (α := ℚ) (-1) n * bernoulli' n = bernoulli' n
inr₁ : 1 * bernoulli' n = bernoulli' n
⊢ bernoulli n = bernoulli' n
have inr₂ : bernoulli' n = bernoulli' n
Tactic: rw [bernoulli, heven.neg_one_pow, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
hn : n ≠ 1
hgt : 1 < n
hodd : Odd n
⊢ bernoulli n = bernoulli' n
have inr : bernoulli n = 0
Tactic: rw [bernoulli'_eq_zero_of_odd hodd hgt, bernoulli_eq_zero_of_odd hodd hgt]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
hn : n ≠ 1
hgt : 1 < n
hodd : Odd n
inr : bernoulli n = 0
⊢ bernoulli n = bernoulli' n
have inr₁ : Eq (α := ℚ) 0 0
Tactic: rw [bernoulli'_eq_zero_of_odd hodd hgt, bernoulli_eq_zero_of_odd hodd hgt]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
n : ℕ
hn : n ≠ 1
hgt : 1 < n
⊢ bernoulli n = bernoulli' n
have x : Even n ∨ Odd n
Tactic: cases n.even_or_odd with
    | inl heven => rw [bernoulli, heven.neg_one_pow, one_mul]
    | inr hodd => rw [bernoulli'_eq_zero_of_odd hodd hgt, bernoulli_eq_zero_of_odd hodd hgt]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
n : ℕ
hn : n ≠ 1
⊢ bernoulli n = bernoulli' n
have x : n < 1 ∨ 1 < n
Tactic: cases hn.lt_or_gt with
  | inl hlt => simp [lt_one_iff.mp hlt]
  | inr hgt =>
    cases n.even_or_odd with
    | inl heven => rw [bernoulli, heven.neg_one_pow, one_mul]
    | inr hodd => rw [bernoulli'_eq_zero_of_odd hodd hgt, bernoulli_eq_zero_of_odd hodd hgt]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
this : ∑ i ∈ range n, (↑((n + 2).choose (i + 2)) : ℚ) * bernoulli (i + 2) = HDiv.hDiv (α := ℚ) (↑n : ℚ) 2
⊢ Eq (α := ℚ) (∑ k ∈ range (n + 1 + 1), (↑((n + 1 + 1).choose k) : ℚ) * bernoulli k) (if n + 1 + 1 = 1 then 1 else 0)
have simp : HDiv.hDiv (α := ℚ) (↑n : ℚ) 2 + (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 + 1) * (-1 / 2) + 1 = 0
Tactic: simp only [this, sum_range_succ', cast_succ, bernoulli_one, bernoulli_zero, choose_one_right,
      mul_one, choose_zero_right, cast_zero, if_false, zero_add, succ_succ_ne_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
⊢ Eq (α := ℚ) (∑ k ∈ range (n + 1 + 1), (↑((n + 1 + 1).choose k) : ℚ) * bernoulli k) (if n + 1 + 1 = 1 then 1 else 0)
have succ : ∑ i ∈ range n, (↑((n + 2).choose (i + 2)) : ℚ) * bernoulli (i + 2) = HDiv.hDiv (α := ℚ) (↑n : ℚ) 2
Tactic: suffices (∑ i ∈ range n, ↑((n + 2).choose (i + 2)) * bernoulli (i + 2)) = n / 2 by
    simp only [this, sum_range_succ', cast_succ, bernoulli_one, bernoulli_zero, choose_one_right,
      mul_one, choose_zero_right, cast_zero, if_false, zero_add, succ_succ_ne_one]
    ring
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
n : ℕ
⊢ ∑ i ∈ range n, (↑((n + 2).choose (i + 2)) : ℚ) * bernoulli (i + 2) = HDiv.hDiv (α := ℚ) (↑n : ℚ) 2
have f : Eq (α := ℚ) (∑ k ∈ range n.succ.succ, (↑(n.succ.succ.choose k) : ℚ) * bernoulli' k) (↑n.succ.succ : ℚ)
Tactic: have f := sum_bernoulli' n.succ.succ
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
n : ℕ
f : Eq (α := ℚ) (∑ k ∈ range n.succ.succ, (↑(n.succ.succ.choose k) : ℚ) * bernoulli' k) (↑n.succ.succ : ℚ)
⊢ ∑ i ∈ range n, (↑((n + 2).choose (i + 2)) : ℚ) * bernoulli (i + 2) = HDiv.hDiv (α := ℚ) (↑n : ℚ) 2
have f₁ : ∑ k ∈ range n, (↑(n.succ.succ.choose (k + 1 + 1)) : ℚ) * bernoulli' (k + 1 + 1) =
  HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 + 1 - (↑(n.succ.succ.choose 0) : ℚ) * bernoulli' 0 -
    (↑(n.succ.succ.choose (HAdd.hAdd (α := ℕ) 0 1)) : ℚ) * bernoulli' (HAdd.hAdd (α := ℕ) 0 1)
Tactic: simp_rw [sum_range_succ', cast_succ, ← eq_sub_iff_add_eq] at f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
f :
  ∑ k ∈ range n, (↑(n.succ.succ.choose (k + 1 + 1)) : ℚ) * bernoulli' (k + 1 + 1) =
    HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 + 1 - (↑(n.succ.succ.choose 0) : ℚ) * bernoulli' 0 -
      (↑(n.succ.succ.choose (HAdd.hAdd (α := ℕ) 0 1)) : ℚ) * bernoulli' (HAdd.hAdd (α := ℕ) 0 1)
⊢ ∑ i ∈ range n, (↑((n + 2).choose (i + 2)) : ℚ) * bernoulli (i + 2) = HDiv.hDiv (α := ℚ) (↑n : ℚ) 2
have succ : Eq (α := ℚ) (∑ i ∈ range n, (↑((n + 2).choose (i + 2)) : ℚ) * bernoulli (i + 2))
  (∑ k ∈ range n, (↑(n.succ.succ.choose (k + 1 + 1)) : ℚ) * bernoulli' (k + 1 + 1))
Tactic: refine Eq.trans ?_ (Eq.trans f ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
f :
  ∑ k ∈ range n, (↑(n.succ.succ.choose (k + 1 + 1)) : ℚ) * bernoulli' (k + 1 + 1) =
    HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 + 1 - (↑(n.succ.succ.choose 0) : ℚ) * bernoulli' 0 -
      (↑(n.succ.succ.choose (HAdd.hAdd (α := ℕ) 0 1)) : ℚ) * bernoulli' (HAdd.hAdd (α := ℕ) 0 1)
succ :
  Eq (α := ℚ) (∑ i ∈ range n, (↑((n + 2).choose (i + 2)) : ℚ) * bernoulli (i + 2))
    (∑ k ∈ range n, (↑(n.succ.succ.choose (k + 1 + 1)) : ℚ) * bernoulli' (k + 1 + 1))
⊢ ∑ i ∈ range n, (↑((n + 2).choose (i + 2)) : ℚ) * bernoulli (i + 2) = HDiv.hDiv (α := ℚ) (↑n : ℚ) 2
have succ₁ : HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 + 1 - (↑(n.succ.succ.choose 0) : ℚ) * bernoulli' 0 -
    (↑(n.succ.succ.choose (HAdd.hAdd (α := ℕ) 0 1)) : ℚ) * bernoulli' (HAdd.hAdd (α := ℕ) 0 1) =
  HDiv.hDiv (α := ℚ) (↑n : ℚ) 2
Tactic: refine Eq.trans ?_ (Eq.trans f ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
f :
  ∑ k ∈ range n, (↑(n.succ.succ.choose (k + 1 + 1)) : ℚ) * bernoulli' (k + 1 + 1) =
    HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 + 1 - (↑(n.succ.succ.choose 0) : ℚ) * bernoulli' 0 -
      (↑(n.succ.succ.choose (HAdd.hAdd (α := ℕ) 0 1)) : ℚ) * bernoulli' (HAdd.hAdd (α := ℕ) 0 1)
⊢ Eq (α := ℚ) (∑ i ∈ range n, (↑((n + 2).choose (i + 2)) : ℚ) * bernoulli (i + 2))
    (∑ k ∈ range n, (↑(n.succ.succ.choose (k + 1 + 1)) : ℚ) * bernoulli' (k + 1 + 1))
have succ : Eq (α := ℕ → ℚ) (fun (i : ℕ) ↦ (↑((n + 2).choose (i + 2)) : ℚ) * bernoulli (i + 2)) fun (k : ℕ) ↦
  (↑(n.succ.succ.choose (k + 1 + 1)) : ℚ) * bernoulli' (k + 1 + 1)
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
f :
  ∑ k ∈ range n, (↑(n.succ.succ.choose (k + 1 + 1)) : ℚ) * bernoulli' (k + 1 + 1) =
    HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 + 1 - (↑(n.succ.succ.choose 0) : ℚ) * bernoulli' 0 -
      (↑(n.succ.succ.choose (HAdd.hAdd (α := ℕ) 0 1)) : ℚ) * bernoulli' (HAdd.hAdd (α := ℕ) 0 1)
⊢ Eq (α := ℕ → ℚ) (fun (i : ℕ) ↦ (↑((n + 2).choose (i + 2)) : ℚ) * bernoulli (i + 2)) fun (k : ℕ) ↦
    (↑(n.succ.succ.choose (k + 1 + 1)) : ℚ) * bernoulli' (k + 1 + 1)
have succ : ∀ (x : ℕ),
  (↑((n + 2).choose (x + 2)) : ℚ) * bernoulli (x + 2) = (↑(n.succ.succ.choose (x + 1 + 1)) : ℚ) * bernoulli' (x + 1 + 1)
Tactic: funext x
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
f :
  ∑ k ∈ range n, (↑(n.succ.succ.choose (k + 1 + 1)) : ℚ) * bernoulli' (k + 1 + 1) =
    HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 + 1 - (↑(n.succ.succ.choose 0) : ℚ) * bernoulli' 0 -
      (↑(n.succ.succ.choose (HAdd.hAdd (α := ℕ) 0 1)) : ℚ) * bernoulli' (HAdd.hAdd (α := ℕ) 0 1)
x : ℕ
⊢ (↑((n + 2).choose (x + 2)) : ℚ) * bernoulli (x + 2) = (↑(n.succ.succ.choose (x + 1 + 1)) : ℚ) * bernoulli' (x + 1 + 1)
have succ : (↑((n + 2).choose (x + 2)) : ℚ) * bernoulli' x.succ.succ =
  (↑(n.succ.succ.choose (x + 1 + 1)) : ℚ) * bernoulli' (x + 1 + 1)
Tactic: rw [bernoulli_eq_bernoulli'_of_ne_one (succ_ne_zero x ∘ succ.inj)]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
f :
  ∑ k ∈ range n, (↑(n.succ.succ.choose (k + 1 + 1)) : ℚ) * bernoulli' (k + 1 + 1) =
    HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 + 1 - (↑(n.succ.succ.choose 0) : ℚ) * bernoulli' 0 -
      (↑(n.succ.succ.choose (HAdd.hAdd (α := ℕ) 0 1)) : ℚ) * bernoulli' (HAdd.hAdd (α := ℕ) 0 1)
⊢ HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 + 1 - (↑(n.succ.succ.choose 0) : ℚ) * bernoulli' 0 -
      (↑(n.succ.succ.choose (HAdd.hAdd (α := ℕ) 0 1)) : ℚ) * bernoulli' (HAdd.hAdd (α := ℕ) 0 1) =
    HDiv.hDiv (α := ℚ) (↑n : ℚ) 2
have succ : HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 + 1 - HAdd.hAdd (α := ℚ) (↑0 : ℚ) 1 - (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 + 1) * (1 / 2) =
  HDiv.hDiv (α := ℚ) (↑n : ℚ) 2
Tactic: simp only [mul_one, bernoulli'_zero, choose_zero_right,
      zero_add, choose_one_right, cast_succ, bernoulli'_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
⊢ Eq (α := ℚ) (∑ k ∈ range (n + 1), (↑((n + 1).choose k) : ℚ) * bernoulli k) (if n + 1 = 1 then 1 else 0)
have succ : Eq (α := ℚ) (∑ k ∈ range (HAdd.hAdd (α := ℕ) 0 1), (↑((HAdd.hAdd (α := ℕ) 0 1).choose k) : ℚ) * bernoulli k)
  (if HAdd.hAdd (α := ℕ) 0 1 = 1 then 1 else 0)
Tactic: cases n with
  | zero => simp
  | succ n =>
  suffices (∑ i ∈ range n, ↑((n + 2).choose (i + 2)) * bernoulli (i + 2)) = n / 2 by
    simp only [this, sum_range_succ', cast_succ, bernoulli_one, bernoulli_zero, choose_one_right,
      mul_one, choose_zero_right, cast_zero, if_false, zero_add, succ_succ_ne_one]
    ring
  have f := sum_bernoulli' n.succ.succ
  simp_rw [sum_range_succ', cast_succ, ← eq_sub_iff_add_eq] at f
  refine Eq.trans ?_ (Eq.trans f ?_)
  · congr
    funext x
    rw [bernoulli_eq_bernoulli'_of_ne_one (succ_ne_zero x ∘ succ.inj)]
  · simp only [mul_one, bernoulli'_zero, choose_zero_right,
      zero_add, choose_one_right, cast_succ, bernoulli'_one]
    ring
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
succ :
  Eq (α := ℚ) (∑ k ∈ range (HAdd.hAdd (α := ℕ) 0 1), (↑((HAdd.hAdd (α := ℕ) 0 1).choose k) : ℚ) * bernoulli k)
    (if HAdd.hAdd (α := ℕ) 0 1 = 1 then 1 else 0)
⊢ Eq (α := ℚ) (∑ k ∈ range (n + 1), (↑((n + 1).choose k) : ℚ) * bernoulli k) (if n + 1 = 1 then 1 else 0)
have succ₁ : ∀ (n : ℕ),
  Eq (α := ℚ) (∑ k ∈ range (n + 1 + 1), (↑((n + 1 + 1).choose k) : ℚ) * bernoulli k) (if n + 1 + 1 = 1 then 1 else 0)
Tactic: cases n with
  | zero => simp
  | succ n =>
  suffices (∑ i ∈ range n, ↑((n + 2).choose (i + 2)) * bernoulli (i + 2)) = n / 2 by
    simp only [this, sum_range_succ', cast_succ, bernoulli_one, bernoulli_zero, choose_one_right,
      mul_one, choose_zero_right, cast_zero, if_false, zero_add, succ_succ_ne_one]
    ring
  have f := sum_bernoulli' n.succ.succ
  simp_rw [sum_range_succ', cast_succ, ← eq_sub_iff_add_eq] at f
  refine Eq.trans ?_ (Eq.trans f ?_)
  · congr
    funext x
    rw [bernoulli_eq_bernoulli'_of_ne_one (succ_ne_zero x ∘ succ.inj)]
  · simp only [mul_one, bernoulli'_zero, choose_zero_right,
      zero_add, choose_one_right, cast_succ, bernoulli'_one]
    ring
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
⊢ Eq (α := ℚ) (∑ k ∈ range n, (↑(n.choose k) : ℚ) * bernoulli k) (if n = 1 then 1 else 0)
have zero : Eq (α := ℚ) (∑ k ∈ range 0, (↑(Nat.choose 0 k) : ℚ) * bernoulli k) (if Eq (α := ℕ) 0 1 then 1 else 0)
Tactic: cases n with | zero => simp | succ n =>
  cases n with
  | zero => simp
  | succ n =>
  suffices (∑ i ∈ range n, ↑((n + 2).choose (i + 2)) * bernoulli (i + 2)) = n / 2 by
    simp only [this, sum_range_succ', cast_succ, bernoulli_one, bernoulli_zero, choose_one_right,
      mul_one, choose_zero_right, cast_zero, if_false, zero_add, succ_succ_ne_one]
    ring
  have f := sum_bernoulli' n.succ.succ
  simp_rw [sum_range_succ', cast_succ, ← eq_sub_iff_add_eq] at f
  refine Eq.trans ?_ (Eq.trans f ?_)
  · congr
    funext x
    rw [bernoulli_eq_bernoulli'_of_ne_one (succ_ne_zero x ∘ succ.inj)]
  · simp only [mul_one, bernoulli'_zero, choose_zero_right,
      zero_add, choose_one_right, cast_succ, bernoulli'_one]
    ring
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
zero : Eq (α := ℚ) (∑ k ∈ range 0, (↑(Nat.choose 0 k) : ℚ) * bernoulli k) (if Eq (α := ℕ) 0 1 then 1 else 0)
⊢ Eq (α := ℚ) (∑ k ∈ range n, (↑(n.choose k) : ℚ) * bernoulli k) (if n = 1 then 1 else 0)
have succ : ∀ (n : ℕ), Eq (α := ℚ) (∑ k ∈ range (n + 1), (↑((n + 1).choose k) : ℚ) * bernoulli k) (if n + 1 = 1 then 1 else 0)
Tactic: cases n with | zero => simp | succ n =>
  cases n with
  | zero => simp
  | succ n =>
  suffices (∑ i ∈ range n, ↑((n + 2).choose (i + 2)) * bernoulli (i + 2)) = n / 2 by
    simp only [this, sum_range_succ', cast_succ, bernoulli_one, bernoulli_zero, choose_one_right,
      mul_one, choose_zero_right, cast_zero, if_false, zero_add, succ_succ_ne_one]
    ring
  have f := sum_bernoulli' n.succ.succ
  simp_rw [sum_range_succ', cast_succ, ← eq_sub_iff_add_eq] at f
  refine Eq.trans ?_ (Eq.trans f ?_)
  · congr
    funext x
    rw [bernoulli_eq_bernoulli'_of_ne_one (succ_ne_zero x ∘ succ.inj)]
  · simp only [mul_one, bernoulli'_zero, choose_zero_right,
      zero_add, choose_one_right, cast_succ, bernoulli'_one]
    ring
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
n : ℕ
⊢ Eq (α := ℚ)
    (∑ k ∈ @antidiagonal _ instAddMonoid _ (n + 1),
      (↑((k.1 + k.2).choose k.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑k.2 : ℚ) 1 * bernoulli k.1)
    0
have h₁ : (1, n) ∈ @antidiagonal _ instAddMonoid _ n.succ
Tactic: have h₁ : (1, n) ∈ antidiagonal n.succ := by simp [mem_antidiagonal, add_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
n : ℕ
h₁ : (1, n) ∈ @antidiagonal _ instAddMonoid _ n.succ
⊢ Eq (α := ℚ)
    (∑ k ∈ @antidiagonal _ instAddMonoid _ (n + 1),
      (↑((k.1 + k.2).choose k.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑k.2 : ℚ) 1 * bernoulli k.1)
    0
have h₃ : (1 + n).choose n = n + 1
Tactic: have h₃ : (1 + n).choose n = n + 1 := by simp [add_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
n : ℕ
h₁ : (1, n) ∈ @antidiagonal _ instAddMonoid _ n.succ
h₃ : (1 + n).choose n = n + 1
⊢ Eq (α := ℚ)
    (∑ k ∈ @antidiagonal _ instAddMonoid _ (n + 1),
      (↑((k.1 + k.2).choose k.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑k.2 : ℚ) 1 * bernoulli k.1)
    0
have H : Eq (α := ℚ)
  (∑ k ∈ @antidiagonal _ instAddMonoid _ n.succ,
    (↑((k.1 + k.2).choose k.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑k.2 : ℚ) 1 * bernoulli' k.1)
  1
Tactic: have H := bernoulli'_spec' n.succ
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
h₁ : (1, n) ∈ @antidiagonal _ instAddMonoid _ n.succ
h₃ : (1 + n).choose n = n + 1
H :
  Eq (α := ℚ)
    (∑ k ∈ @antidiagonal _ instAddMonoid _ n.succ,
      (↑((k.1 + k.2).choose k.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑k.2 : ℚ) 1 * bernoulli' k.1)
    1
⊢ Eq (α := ℚ)
    (∑ k ∈ @antidiagonal _ instAddMonoid _ (n + 1),
      (↑((k.1 + k.2).choose k.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑k.2 : ℚ) 1 * bernoulli k.1)
    0
have succ : ∀
  (H :
    (↑(((1, n).1 + (1, n).2).choose (1, n).2) : ℚ) / HAdd.hAdd (α := ℚ) (↑(1, n).2 : ℚ) 1 * bernoulli' (1, n).1 +
        ∑ x ∈ @antidiagonal _ instAddMonoid _ n.succ \ {(1, n)},
          (↑((x.1 + x.2).choose x.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * bernoulli' x.1 =
      1),
  (↑(((1, n).1 + (1, n).2).choose (1, n).2) : ℚ) / HAdd.hAdd (α := ℚ) (↑(1, n).2 : ℚ) 1 * bernoulli (1, n).1 +
      ∑ x ∈ @antidiagonal _ instAddMonoid _ n.succ \ {(1, n)},
        (↑((x.1 + x.2).choose x.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * bernoulli x.1 =
    0
Tactic: rw [sum_eq_add_sum_diff_singleton_of_mem h₁] at H ⊢
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
h₁ : (1, n) ∈ @antidiagonal _ instAddMonoid _ n.succ
h₃ : (1 + n).choose n = n + 1
H :
  (↑(((1, n).1 + (1, n).2).choose (1, n).2) : ℚ) / HAdd.hAdd (α := ℚ) (↑(1, n).2 : ℚ) 1 * bernoulli' (1, n).1 +
      ∑ x ∈ @antidiagonal _ instAddMonoid _ n.succ \ {(1, n)},
        (↑((x.1 + x.2).choose x.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * bernoulli' x.1 =
    1
⊢ (↑(((1, n).1 + (1, n).2).choose (1, n).2) : ℚ) / HAdd.hAdd (α := ℚ) (↑(1, n).2 : ℚ) 1 * bernoulli (1, n).1 +
      ∑ x ∈ @antidiagonal _ instAddMonoid _ n.succ \ {(1, n)},
        (↑((x.1 + x.2).choose x.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * bernoulli x.1 =
    0
have succ : ∑ x ∈ @antidiagonal _ instAddMonoid _ n.succ \ {(1, n)},
    (↑((x.1 + x.2).choose x.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * bernoulli x.1 =
  0 - (↑(((1, n).1 + (1, n).2).choose (1, n).2) : ℚ) / HAdd.hAdd (α := ℚ) (↑(1, n).2 : ℚ) 1 * bernoulli (1, n).1
Tactic: apply add_eq_of_eq_sub'
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
h₁ : (1, n) ∈ @antidiagonal _ instAddMonoid _ n.succ
h₃ : (1 + n).choose n = n + 1
H :
  (↑(((1, n).1 + (1, n).2).choose (1, n).2) : ℚ) / HAdd.hAdd (α := ℚ) (↑(1, n).2 : ℚ) 1 * bernoulli' (1, n).1 +
      ∑ x ∈ @antidiagonal _ instAddMonoid _ n.succ \ {(1, n)},
        (↑((x.1 + x.2).choose x.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * bernoulli' x.1 =
    1
⊢ ∑ x ∈ @antidiagonal _ instAddMonoid _ n.succ \ {(1, n)},
      (↑((x.1 + x.2).choose x.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * bernoulli x.1 =
    0 - (↑(((1, n).1 + (1, n).2).choose (1, n).2) : ℚ) / HAdd.hAdd (α := ℚ) (↑(1, n).2 : ℚ) 1 * bernoulli (1, n).1
have h : Eq (α := ℚ)
  (∑ x ∈ @antidiagonal _ instAddMonoid _ n.succ \ {(1, n)},
    (↑((x.1 + x.2).choose x.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * bernoulli x.1)
  (∑ x ∈ @antidiagonal _ instAddMonoid _ n.succ \ {(1, n)},
    (↑((x.1 + x.2).choose x.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * bernoulli' x.1)
Tactic: convert! eq_sub_of_add_eq' H using 1