awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
a b : R
h : (↑p : R) ∣ a - b
k : ℕ
zero : HPow.hPow (α := R) (↑p : R) (HAdd.hAdd (α := ℕ) 0 1) ∣ a ^ HPow.hPow (β := ℕ) p 0 - b ^ HPow.hPow (β := ℕ) p 0
⊢ HPow.hPow (α := R) (↑p : R) (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
have succ : ∀ (k : ℕ) (ih : HPow.hPow (α := R) (↑p : R) (k + 1) ∣ a ^ p ^ k - b ^ p ^ k),
  HPow.hPow (α := R) (↑p : R) (k + 1 + 1) ∣ a ^ p ^ (k + 1) - b ^ p ^ (k + 1)
Tactic: induction k with
  | zero => rwa [pow_one, pow_zero, pow_one, pow_one]
  | succ k ih =>
    rw [pow_succ p k, pow_mul, pow_mul, ← geom_sum₂_mul, pow_succ']
    refine mul_dvd_mul ?_ ih
    let f : R →+* R ⧸ span {(p : R)} := mk (span {(p : R)})
    have hf : ∀ r : R, (p : R) ∣ r ↔ f r = 0 := fun r ↦ by rw [eq_zero_iff_mem, mem_span_singleton]
    rw [hf, map_sub, sub_eq_zero] at h
    rw [hf, RingHom.map_geom_sum₂, map_pow, map_pow, h, geom_sum₂_self, mul_eq_zero_of_left]
    rw [← map_natCast f, eq_zero_iff_mem, mem_span_singleton]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
⊢ bernoulli' n =
    HSub.hSub (α := ℚ) 1
      (∑ k : Fin n,
        (↑(n.choose (↑k : ℕ)) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑(↑k : ℕ) : ℚ) + 1) * bernoulli' (↑k : ℕ))
have rw : HSub.hSub (α := ℚ) 1
    (∑ k : Fin n,
      (↑(n.choose (↑k : ℕ)) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑(↑k : ℕ) : ℚ) + 1) * bernoulli' (↑k : ℕ)) =
  HSub.hSub (α := ℚ) 1
    (∑ k : Fin n, (↑(n.choose (↑k : ℕ)) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑(↑k : ℕ) : ℚ) + 1) * bernoulli' (↑k : ℕ))
Tactic: rw [bernoulli']
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
⊢ bernoulli' n =
    HSub.hSub (α := ℚ) 1
      (∑ k ∈ range n, (↑(n.choose k) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑k : ℚ) + 1) * bernoulli' k)
have rw : HSub.hSub (α := ℚ) 1
    (∑ k : Fin n,
      (↑(n.choose (↑k : ℕ)) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑(↑k : ℕ) : ℚ) + 1) * bernoulli' (↑k : ℕ)) =
  HSub.hSub (α := ℚ) 1 (∑ k ∈ range n, (↑(n.choose k) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑k : ℚ) + 1) * bernoulli' k)
Tactic: rw [bernoulli'_def', ← Fin.sum_univ_eq_sum_range]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
rw :
  HSub.hSub (α := ℚ) 1
      (∑ k : Fin n,
        (↑(n.choose (↑k : ℕ)) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑(↑k : ℕ) : ℚ) + 1) * bernoulli' (↑k : ℕ)) =
    HSub.hSub (α := ℚ) 1
      (∑ k ∈ range n, (↑(n.choose k) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑k : ℚ) + 1) * bernoulli' k)
⊢ bernoulli' n =
    HSub.hSub (α := ℚ) 1
      (∑ k ∈ range n, (↑(n.choose k) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑k : ℚ) + 1) * bernoulli' k)
have rw₁ : HSub.hSub (α := ℚ) 1
    (∑ k : Fin n,
      (↑(n.choose (↑k : ℕ)) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑(↑k : ℕ) : ℚ) + 1) * bernoulli' (↑k : ℕ)) =
  HSub.hSub (α := ℚ) 1
    (∑ i : Fin n, (↑(n.choose (↑i : ℕ)) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑(↑i : ℕ) : ℚ) + 1) * bernoulli' (↑i : ℕ))
Tactic: rw [bernoulli'_def', ← Fin.sum_univ_eq_sum_range]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
⊢ Eq (α := ℚ)
    (∑ k ∈ range n.succ, (↑(n.choose (n - k)) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑k : ℚ) + 1) * bernoulli' k) 1
have rw : Eq (α := ℚ)
  (∑ x ∈ range n,
    ((↑(n.choose x) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑x : ℚ) + 1) * bernoulli' x -
      (↑(n.choose (n - x)) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑x : ℚ) + 1) * bernoulli' x))
  0
Tactic: rw [sum_range_succ_comm, bernoulli'_def n, tsub_self, choose_zero_right, sub_self, zero_add,
    div_one, cast_one, one_mul, sub_add, ← sum_sub_distrib, ← sub_eq_zero, sub_sub_cancel_left,
    neg_eq_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n x : ℕ
hx : x ∈ range n
⊢ (↑(n.choose x) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑x : ℚ) + 1) * bernoulli' x -
      (↑(n.choose (n - x)) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑x : ℚ) + 1) * bernoulli' x =
    0
have rw : (↑(n.choose x) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑x : ℚ) + 1) * bernoulli' x -
    (↑(n.choose x) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑x : ℚ) + 1) * bernoulli' x =
  0
Tactic: rw [choose_symm (le_of_lt (mem_range.1 hx)), sub_self]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n x : ℕ
hx : x ∈ range n
rw :
  (↑(n.choose x) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑x : ℚ) + 1) * bernoulli' x -
      (↑(n.choose x) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑x : ℚ) + 1) * bernoulli' x =
    0
⊢ (↑(n.choose x) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑x : ℚ) + 1) * bernoulli' x -
      (↑(n.choose (n - x)) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑x : ℚ) + 1) * bernoulli' x =
    0
have rw₁ : Eq (α := ℚ) 0 0
Tactic: rw [choose_symm (le_of_lt (mem_range.1 hx)), sub_self]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
⊢ Eq (α := ℚ)
    (∑ k ∈ @antidiagonal _ instAddMonoid _ n,
      (↑((k.1 + k.2).choose k.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑k.2 : ℚ) 1 * bernoulli' k.1)
    1
have refine : Eq (α := ℚ)
  (∑ k ∈ range n.succ,
    (↑(((k, n - k).1 + (k, n - k).2).choose (k, n - k).2) : ℚ) / HAdd.hAdd (α := ℚ) (↑(k, n - k).2 : ℚ) 1 *
      bernoulli' (k, n - k).1)
  (∑ k ∈ range n.succ, (↑(n.choose (n - k)) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑k : ℚ) + 1) * bernoulli' k)
Tactic: refine ((sum_antidiagonal_eq_sum_range_succ_mk _ n).trans ?_).trans (bernoulli'_spec n)
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
⊢ Eq (α := ℚ)
    (∑ k ∈ range n.succ,
      (↑(((k, n - k).1 + (k, n - k).2).choose (k, n - k).2) : ℚ) / HAdd.hAdd (α := ℚ) (↑(k, n - k).2 : ℚ) 1 *
        bernoulli' (k, n - k).1)
    (∑ k ∈ range n.succ, (↑(n.choose (n - k)) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑k : ℚ) + 1) * bernoulli' k)
have refine : ∀ (x : ℕ) (hx : x ∈ range n.succ),
  (↑(((x, n - x).1 + (x, n - x).2).choose (x, n - x).2) : ℚ) / HAdd.hAdd (α := ℚ) (↑(x, n - x).2 : ℚ) 1 *
      bernoulli' (x, n - x).1 =
    (↑(n.choose (n - x)) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑x : ℚ) + 1) * bernoulli' x
Tactic: refine sum_congr rfl fun x hx => ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
⊢ bernoulli' 0 = 1
have rw : HSub.hSub (α := ℚ) 1
    (∑ k ∈ range 0, (↑(Nat.choose 0 k) : ℚ) / (HSub.hSub (α := ℚ) (↑0 : ℚ) (↑k : ℚ) + 1) * bernoulli' k) =
  1
Tactic: rw [bernoulli'_def]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
⊢ bernoulli' 1 = 1 / 2
have rw : HSub.hSub (α := ℚ) 1
    (∑ k ∈ range 1, (↑(Nat.choose 1 k) : ℚ) / (HSub.hSub (α := ℚ) (↑1 : ℚ) (↑k : ℚ) + 1) * bernoulli' k) =
  1 / 2
Tactic: rw [bernoulli'_def]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
⊢ bernoulli' 2 = 1 / 6
have rw : HSub.hSub (α := ℚ) 1
    (∑ k ∈ range 2, (↑(Nat.choose 2 k) : ℚ) / (HSub.hSub (α := ℚ) (↑2 : ℚ) (↑k : ℚ) + 1) * bernoulli' k) =
  1 / 6
Tactic: rw [bernoulli'_def]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
⊢ bernoulli' 3 = 0
have rw : HSub.hSub (α := ℚ) 1
    (∑ k ∈ range 3, (↑(Nat.choose 3 k) : ℚ) / (HSub.hSub (α := ℚ) (↑3 : ℚ) (↑k : ℚ) + 1) * bernoulli' k) =
  0
Tactic: rw [bernoulli'_def]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
⊢ bernoulli' 4 = -1 / 30
have this : Nat.choose 4 2 = 6
Tactic: have : Nat.choose 4 2 = 6 := by decide
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
this : Nat.choose 4 2 = 6
⊢ bernoulli' 4 = -1 / 30
have rw : HSub.hSub (α := ℚ) 1
    (∑ k ∈ range 4, (↑(Nat.choose 4 k) : ℚ) / (HSub.hSub (α := ℚ) (↑4 : ℚ) (↑k : ℚ) + 1) * bernoulli' k) =
  -1 / 30
Tactic: rw [bernoulli'_def]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
this :
  HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 *
      ∑ k ∈ range n, (↑(n.choose k) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑k : ℚ) + 1) * bernoulli' k =
    ∑ x ∈ range n, (↑(n.succ.choose x) : ℚ) * bernoulli' x
⊢ Eq (α := ℚ) (∑ k ∈ range (n + 1), (↑((n + 1).choose k) : ℚ) * bernoulli' k) (↑(n + 1) : ℚ)
have rw_mod_cast : ∀
  (this :
    HMul.hMul (α := ℚ) (↑(n + 1) : ℚ)
        (∑ x ∈ range n, Rat.divInt (↑(n.choose x) : ℤ) (Int.subNatNat n x + 1) * bernoulli' x) =
      ∑ x ∈ range n, (↑(n.succ.choose x) : ℚ) * bernoulli' x),
  HMul.hMul (α := ℚ) (↑(n + 1) : ℚ)
        (∑ x ∈ range n, Rat.divInt (↑(n.choose x) : ℤ) (Int.subNatNat n x + 1) * bernoulli' x) +
      (↑(n + 1) : ℚ) *
        HSub.hSub (α := ℚ) 1 (∑ x ∈ range n, Rat.divInt (↑(n.choose x) : ℤ) (Int.subNatNat n x + 1) * bernoulli' x) =
    (↑(n + 1) : ℚ)
Tactic: rw_mod_cast [sum_range_succ, bernoulli'_def, ← this, choose_succ_self_right]
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
⊢ Eq (α := ℚ) (∑ k ∈ range (n + 1), (↑((n + 1).choose k) : ℚ) * bernoulli' k) (↑(n + 1) : ℚ)
have succ : HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 *
    ∑ k ∈ range n, (↑(n.choose k) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑k : ℚ) + 1) * bernoulli' k =
  ∑ x ∈ range n, (↑(n.succ.choose x) : ℚ) * bernoulli' x
Tactic: suffices
    ((n + 1 : ℚ) * ∑ k ∈ range n, ↑(n.choose k) / (n - k + 1) * bernoulli' k) =
      ∑ x ∈ range n, ↑(n.succ.choose x) * bernoulli' x by
    rw_mod_cast [sum_range_succ, bernoulli'_def, ← this, choose_succ_self_right]
    ring
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
⊢ HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 *
      ∑ k ∈ range n, (↑(n.choose k) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑k : ℚ) + 1) * bernoulli' k =
    ∑ x ∈ range n, (↑(n.succ.choose x) : ℚ) * bernoulli' x
have succ : Eq (α := ℚ)
  (∑ x ∈ range n,
    HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 * ((↑(n.choose x) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑x : ℚ) + 1)) * bernoulli' x)
  (∑ x ∈ range n, (↑(n.succ.choose x) : ℚ) * bernoulli' x)
Tactic: simp_rw [mul_sum, ← mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
⊢ Eq (α := ℚ)
    (∑ x ∈ range n,
      HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 * ((↑(n.choose x) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑x : ℚ) + 1)) * bernoulli' x)
    (∑ x ∈ range n, (↑(n.succ.choose x) : ℚ) * bernoulli' x)
have succ : ∀ (k : ℕ) (hk : k ∈ range n),
  HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 * ((↑(n.choose k) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑k : ℚ) + 1)) * bernoulli' k =
    (↑(n.succ.choose k) : ℚ) * bernoulli' k
Tactic: refine sum_congr rfl fun k hk => ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n k : ℕ
hk : k ∈ range n
⊢ HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 * ((↑(n.choose k) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑k : ℚ) + 1)) * bernoulli' k =
    (↑(n.succ.choose k) : ℚ) * bernoulli' k
have succ : HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 * ((↑(n.choose k) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑k : ℚ) + 1)) =
  (↑(n.succ.choose k) : ℚ)
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n k : ℕ
hk : k ∈ range n
⊢ HAdd.hAdd (α := ℚ) (↑(n - k) : ℚ) 1 ≠ 0
have norm_cast : ¬False
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
n k : ℕ
hk : k ∈ range n
⊢ HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 * ((↑(n.choose k) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑k : ℚ) + 1)) =
    (↑(n.succ.choose k) : ℚ)
have this : HAdd.hAdd (α := ℚ) (↑(n - k) : ℚ) 1 ≠ 0
Tactic: have : ((n - k : ℕ) : ℚ) + 1 ≠ 0 := by norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n k : ℕ
hk : k ∈ range n
this : HAdd.hAdd (α := ℚ) (↑(n - k) : ℚ) 1 ≠ 0
⊢ HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 * ((↑(n.choose k) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑k : ℚ) + 1)) =
    (↑(n.succ.choose k) : ℚ)
have succ : (↑(n.choose k) : ℚ) * HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 = (↑((n + 1).choose k) : ℚ) * HAdd.hAdd (α := ℚ) (↑(n - k) : ℚ) 1
Tactic: simp only [← cast_sub (mem_range.1 hk).le, succ_eq_add_one, field, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n k : ℕ
hk : k ∈ range n
this : HAdd.hAdd (α := ℚ) (↑(n - k) : ℚ) 1 ≠ 0
⊢ (↑(n.choose k) : ℚ) * HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 = (↑((n + 1).choose k) : ℚ) * HAdd.hAdd (α := ℚ) (↑(n - k) : ℚ) 1
have succ : ∀ (this : ¬False), n.choose k * (n + 1) = (n + 1).choose k * (n - k + 1)
Tactic: rw_mod_cast [tsub_add_eq_add_tsub (mem_range.1 hk).le, choose_mul_succ_eq]
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n k : ℕ
hk : k ∈ range n
this : HAdd.hAdd (α := ℚ) (↑(n - k) : ℚ) 1 ≠ 0
succ succ₁ succ₂ succ₃ succ₄ succ₅ : ∀ (this : ¬False), n.choose k * (n + 1) = (n + 1).choose k * (n - k + 1)
⊢ (↑(n.choose k) : ℚ) * HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 = (↑((n + 1).choose k) : ℚ) * HAdd.hAdd (α := ℚ) (↑(n - k) : ℚ) 1
have succ₆ : ∀ (this : ¬False), n.choose k * (n + 1) = (n + 1).choose k * (n + 1 - k)
Tactic: rw_mod_cast [tsub_add_eq_add_tsub (mem_range.1 hk).le, choose_mul_succ_eq]
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
⊢ Eq (α := ℚ) (∑ k ∈ range n, (↑(n.choose k) : ℚ) * bernoulli' k) (↑n : ℚ)
have zero : Eq (α := ℚ) (∑ k ∈ range 0, (↑(Nat.choose 0 k) : ℚ) * bernoulli' k) (↑0 : ℚ)
Tactic: cases n with | zero => simp | succ n =>
  suffices
    ((n + 1 : ℚ) * ∑ k ∈ range n, ↑(n.choose k) / (n - k + 1) * bernoulli' k) =
      ∑ x ∈ range n, ↑(n.succ.choose x) * bernoulli' x by
    rw_mod_cast [sum_range_succ, bernoulli'_def, ← this, choose_succ_self_right]
    ring
  simp_rw [mul_sum, ← mul_assoc]
  refine sum_congr rfl fun k hk => ?_
  congr
  have : ((n - k : ℕ) : ℚ) + 1 ≠ 0 := by norm_cast
  simp only [← cast_sub (mem_range.1 hk).le, succ_eq_add_one, field, mul_comm]
  rw_mod_cast [tsub_add_eq_add_tsub (mem_range.1 hk).le, choose_mul_succ_eq]
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) (↑0 : ℚ)
⊢ Eq (α := ℚ) (∑ k ∈ range n, (↑(n.choose k) : ℚ) * bernoulli' k) (↑n : ℚ)
have succ : ∀ (n : ℕ), Eq (α := ℚ) (∑ k ∈ range (n + 1), (↑((n + 1).choose k) : ℚ) * bernoulli' k) (↑(n + 1) : ℚ)
Tactic: cases n with | zero => simp | succ n =>
  suffices
    ((n + 1 : ℚ) * ∑ k ∈ range n, ↑(n.choose k) / (n - k + 1) * bernoulli' k) =
      ∑ x ∈ range n, ↑(n.succ.choose x) * bernoulli' x by
    rw_mod_cast [sum_range_succ, bernoulli'_def, ← this, choose_succ_self_right]
    ring
  simp_rw [mul_sum, ← mul_assoc]
  refine sum_congr rfl fun k hk => ?_
  congr
  have : ((n - k : ℕ) : ℚ) + 1 ≠ 0 := by norm_cast
  simp only [← cast_sub (mem_range.1 hk).le, succ_eq_add_one, field, mul_comm]
  rw_mod_cast [tsub_add_eq_add_tsub (mem_range.1 hk).le, choose_mul_succ_eq]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
⊢ bernoulli'PowerSeries A * (exp A - 1) = X * exp A
have h : ∀ (n : ℕ),
  Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) (bernoulli'PowerSeries A * (exp A - 1)) : A)
    ((coeff n : (a : A⟦X⟧) → A) (X * exp A) : A)
Tactic: ext n
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
⊢ Eq (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (bernoulli'PowerSeries A * (exp A - 1)) : A)
    ((coeff (n + 1) : (a : A⟦X⟧) → A) (X * exp A) : A)
have h : HMul.hMul (α := A) (β := A)
      ((coeff (n + 1, 0).1 : (a : A⟦X⟧) → A)
          (PowerSeries.mk fun (n : ℕ) ↦ (algebraMap ℚ A : (a : ℚ) → A) (bernoulli' n / (↑n ! : ℚ))) :
        A)
      ((coeff (n + 1, 0).2 : (a : A⟦X⟧) → A) (exp A - 1) : A) +
    ∑ p ∈ @antidiagonal _ instAddMonoid _ n,
      HMul.hMul (α := A) (β := A)
        ((coeff (p.1, p.2 + 1).1 : (a : A⟦X⟧) → A)
            (PowerSeries.mk fun (n : ℕ) ↦ (algebraMap ℚ A : (a : ℚ) → A) (bernoulli' n / (↑n ! : ℚ))) :
          A)
        ((coeff (p.1, p.2 + 1).2 : (a : A⟦X⟧) → A) (exp A - 1) : A) =
  (coeff (n + 1) : (a : A⟦X⟧) → A) (exp A * X)
Tactic: rw [bernoulli'PowerSeries, coeff_mul, mul_comm X, sum_antidiagonal_succ']
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
⊢ HMul.hMul (α := A) (β := A)
        ((coeff (n + 1, 0).1 : (a : A⟦X⟧) → A)
            (PowerSeries.mk fun (n : ℕ) ↦ (algebraMap ℚ A : (a : ℚ) → A) (bernoulli' n / (↑n ! : ℚ))) :
          A)
        ((coeff (n + 1, 0).2 : (a : A⟦X⟧) → A) (exp A - 1) : A) +
      ∑ p ∈ @antidiagonal _ instAddMonoid _ n,
        HMul.hMul (α := A) (β := A)
          ((coeff (p.1, p.2 + 1).1 : (a : A⟦X⟧) → A)
              (PowerSeries.mk fun (n : ℕ) ↦ (algebraMap ℚ A : (a : ℚ) → A) (bernoulli' n / (↑n ! : ℚ))) :
            A)
          ((coeff (p.1, p.2 + 1).2 : (a : A⟦X⟧) → A) (exp A - 1) : A) =
    (coeff (n + 1) : (a : A⟦X⟧) → A) (exp A * X)
have h : Eq (α := ℚ)
  (∑ p ∈ @antidiagonal _ instAddMonoid _ n,
    bernoulli' p.1 / (↑p.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑p.2 : ℚ) 1 * (↑p.2! : ℚ))⁻¹)
  (↑n ! : ℚ)⁻¹
Tactic: suffices (∑ p ∈ antidiagonal n,
      bernoulli' p.1 / p.1! * ((p.2 + 1) * p.2! : ℚ)⁻¹) = (n ! : ℚ)⁻¹ by
    simpa [map_sum, Nat.factorial] using congr_arg (algebraMap ℚ A) this
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
⊢ Eq (α := ℚ)
    (∑ p ∈ @antidiagonal _ instAddMonoid _ n,
      bernoulli' p.1 / (↑p.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑p.2 : ℚ) 1 * (↑p.2! : ℚ))⁻¹)
    (↑n ! : ℚ)⁻¹
have h : HMul.hMul (α := ℚ)
    (∑ p ∈ @antidiagonal _ instAddMonoid _ n,
      bernoulli' p.1 / (↑p.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑p.2 : ℚ) 1 * (↑p.2! : ℚ))⁻¹)
    (↑n ! : ℚ) =
  1
Tactic: apply eq_inv_of_mul_eq_one_left
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
⊢ HMul.hMul (α := ℚ)
      (∑ p ∈ @antidiagonal _ instAddMonoid _ n,
        bernoulli' p.1 / (↑p.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑p.2 : ℚ) 1 * (↑p.2! : ℚ))⁻¹)
      (↑n ! : ℚ) =
    1
have h : Eq (α := ℚ)
  (∑ i ∈ @antidiagonal _ instAddMonoid _ n,
    bernoulli' i.1 / (↑i.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑i.2 : ℚ) 1 * (↑i.2! : ℚ))⁻¹ * (↑n ! : ℚ))
  1
Tactic: rw [sum_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
⊢ Eq (α := ℚ)
    (∑ i ∈ @antidiagonal _ instAddMonoid _ n,
      bernoulli' i.1 / (↑i.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑i.2 : ℚ) 1 * (↑i.2! : ℚ))⁻¹ * (↑n ! : ℚ))
    1
have h : Eq (α := ℚ)
  (∑ i ∈ @antidiagonal _ instAddMonoid _ n,
    bernoulli' i.1 / (↑i.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑i.2 : ℚ) 1 * (↑i.2! : ℚ))⁻¹ * (↑n ! : ℚ))
  (∑ k ∈ @antidiagonal _ instAddMonoid _ n,
    (↑((k.1 + k.2).choose k.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑k.2 : ℚ) 1 * bernoulli' k.1)
Tactic: convert! bernoulli'_spec' n using 1
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
⊢ Eq (α := ℚ)
    (∑ i ∈ @antidiagonal _ instAddMonoid _ n,
      bernoulli' i.1 / (↑i.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑i.2 : ℚ) 1 * (↑i.2! : ℚ))⁻¹ * (↑n ! : ℚ))
    (∑ k ∈ @antidiagonal _ instAddMonoid _ n,
      (↑((k.1 + k.2).choose k.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑k.2 : ℚ) 1 * bernoulli' k.1)
have h : ∀ x ∈ @antidiagonal _ instAddMonoid _ n,
  bernoulli' x.1 / (↑x.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * (↑x.2! : ℚ))⁻¹ * (↑n ! : ℚ) =
    (↑((x.1 + x.2).choose x.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * bernoulli' x.1
Tactic: apply sum_congr rfl
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
⊢ ∀ x ∈ @antidiagonal _ instAddMonoid _ n,
    bernoulli' x.1 / (↑x.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * (↑x.2! : ℚ))⁻¹ * (↑n ! : ℚ) =
      (↑((x.1 + x.2).choose x.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * bernoulli' x.1
have h : ∀ (x : ℕ × ℕ),
  x.1 + x.2 = n →
    bernoulli' x.1 / (↑x.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * (↑x.2! : ℚ))⁻¹ * (↑n ! : ℚ) =
      (↑((x.1 + x.2).choose x.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * bernoulli' x.1
Tactic: simp_rw [mem_antidiagonal]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
i j : ℕ
⊢ bernoulli' (i, j).1 / (↑(i, j).1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑(i, j).2 : ℚ) 1 * (↑(i, j).2! : ℚ))⁻¹ *
      (↑((i, j).1 + (i, j).2)! : ℚ) =
    (↑(((i, j).1 + (i, j).2).choose (i, j).2) : ℚ) / HAdd.hAdd (α := ℚ) (↑(i, j).2 : ℚ) 1 * bernoulli' (i, j).1
have this : i ! * j ! ∣ (i + j)!
Tactic: have := factorial_mul_factorial_dvd_factorial_add i j
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
⊢ Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) (bernoulli'PowerSeries A * (exp A - 1)) : A)
    ((coeff n : (a : A⟦X⟧) → A) (X * exp A) : A)
have h : Eq (α := A) ((coeff 0 : (a : A⟦X⟧) → A) (bernoulli'PowerSeries A * (exp A - 1)) : A)
  ((coeff 0 : (a : A⟦X⟧) → A) (X * exp A) : A)
Tactic: cases n with | zero => simp | succ n =>
  rw [bernoulli'PowerSeries, coeff_mul, mul_comm X, sum_antidiagonal_succ']
  suffices (∑ p ∈ antidiagonal n,
      bernoulli' p.1 / p.1! * ((p.2 + 1) * p.2! : ℚ)⁻¹) = (n ! : ℚ)⁻¹ by
    simpa [map_sum, Nat.factorial] using congr_arg (algebraMap ℚ A) this
  apply eq_inv_of_mul_eq_one_left
  rw [sum_mul]
  convert! bernoulli'_spec' n using 1
  apply sum_congr rfl
  simp_rw [mem_antidiagonal]
  rintro ⟨i, j⟩ rfl
  have := factorial_mul_factorial_dvd_factorial_add i j
  simp [field, add_choose, *]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
h :
  Eq (α := A) ((coeff 0 : (a : A⟦X⟧) → A) (bernoulli'PowerSeries A * (exp A - 1)) : A)
    ((coeff 0 : (a : A⟦X⟧) → A) (X * exp A) : A)
⊢ Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) (bernoulli'PowerSeries A * (exp A - 1)) : A)
    ((coeff n : (a : A⟦X⟧) → A) (X * exp A) : A)
have h₁ : ∀ (n : ℕ),
  Eq (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (bernoulli'PowerSeries A * (exp A - 1)) : A)
    ((coeff (n + 1) : (a : A⟦X⟧) → A) (X * exp A) : A)
Tactic: cases n with | zero => simp | succ n =>
  rw [bernoulli'PowerSeries, coeff_mul, mul_comm X, sum_antidiagonal_succ']
  suffices (∑ p ∈ antidiagonal n,
      bernoulli' p.1 / p.1! * ((p.2 + 1) * p.2! : ℚ)⁻¹) = (n ! : ℚ)⁻¹ by
    simpa [map_sum, Nat.factorial] using congr_arg (algebraMap ℚ A) this
  apply eq_inv_of_mul_eq_one_left
  rw [sum_mul]
  convert! bernoulli'_spec' n using 1
  apply sum_congr rfl
  simp_rw [mem_antidiagonal]
  rintro ⟨i, j⟩ rfl
  have := factorial_mul_factorial_dvd_factorial_add i j
  simp [field, add_choose, *]
Cleared hypotheses: n
-- 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)
⊢ bernoulli' n = 0
have inl : ∀ (h : HSub.hSub (β := ℚ⟦X⟧) B ((evalNegHom : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧) = X), bernoulli' n = 0
Tactic: rcases mul_eq_mul_right_iff.mp this with h | 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)
inl : ∀ (h : HSub.hSub (β := ℚ⟦X⟧) B ((evalNegHom : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧) = X), bernoulli' n = 0
⊢ bernoulli' n = 0
have inr : ∀ (h : exp ℚ - 1 = 0), bernoulli' n = 0
Tactic: rcases mul_eq_mul_right_iff.mp this with h | h
-- 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 : HSub.hSub (β := ℚ⟦X⟧) B ((evalNegHom : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧) = X
⊢ bernoulli' n = 0
have 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 : ℚ)
Tactic: simp only [PowerSeries.ext_iff, evalNegHom, coeff_X] at h
Cleared hypotheses: h