awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n x : ℕ
hx : x ≤ n
⊢ Eq (α := ℚ[X]) ((monomial (n - x) : (a : ℚ) → ℚ[X]) (_root_.bernoulli x * (↑(n.choose x) : ℚ)) : ℚ[X])
    ((monomial (n - x) : (a : ℚ) → ℚ[X]) (_root_.bernoulli (n - (n - x)) * (↑(n.choose (n - x)) : ℚ)) : ℚ[X])
have rw : Eq (α := ℚ[X]) ((monomial (n - x) : (a : ℚ) → ℚ[X]) (_root_.bernoulli x * (↑(n.choose x) : ℚ)) : ℚ[X])
  ((monomial (n - x) : (a : ℚ) → ℚ[X]) (_root_.bernoulli (n - (n - x)) * (↑(n.choose x) : ℚ)) : ℚ[X])
Tactic: rw [choose_symm hx, tsub_tsub_cancel_of_le hx]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n x : ℕ
hx : x ≤ n
rw :
  Eq (α := ℚ[X]) ((monomial (n - x) : (a : ℚ) → ℚ[X]) (_root_.bernoulli x * (↑(n.choose x) : ℚ)) : ℚ[X])
    ((monomial (n - x) : (a : ℚ) → ℚ[X]) (_root_.bernoulli (n - (n - x)) * (↑(n.choose x) : ℚ)) : ℚ[X])
⊢ Eq (α := ℚ[X]) ((monomial (n - x) : (a : ℚ) → ℚ[X]) (_root_.bernoulli x * (↑(n.choose x) : ℚ)) : ℚ[X])
    ((monomial (n - x) : (a : ℚ) → ℚ[X]) (_root_.bernoulli (n - (n - x)) * (↑(n.choose (n - x)) : ℚ)) : ℚ[X])
have rw₁ : Eq (α := ℚ[X]) ((monomial (n - x) : (a : ℚ) → ℚ[X]) (_root_.bernoulli x * (↑(n.choose x) : ℚ)) : ℚ[X])
  ((monomial (n - x) : (a : ℚ) → ℚ[X]) (_root_.bernoulli x * (↑(n.choose x) : ℚ)) : ℚ[X])
Tactic: rw [choose_symm hx, tsub_tsub_cancel_of_le hx]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n i : ℕ
⊢ (bernoulli n).coeff i = if i ≤ n then _root_.bernoulli (n - i) * (↑(n.choose i) : ℚ) else 0
have simp : (∑ x ∈ range (n + 1), if n - x = i then _root_.bernoulli x * (↑(n.choose x) : ℚ) else 0) =
  if i ≤ n then _root_.bernoulli (n - i) * (↑(n.choose i) : ℚ) else 0
Tactic: simp only [bernoulli, finsetSum_coeff, coeff_monomial]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n i : ℕ
⊢ (∑ x ∈ range (n + 1), if n - x = i then _root_.bernoulli x * (↑(n.choose x) : ℚ) else 0) =
    if i ≤ n then _root_.bernoulli (n - i) * (↑(n.choose i) : ℚ) else 0
have pos : ∀ (h : i ≤ n),
  (∑ x ∈ range (n + 1), if n - x = i then _root_.bernoulli x * (↑(n.choose x) : ℚ) else 0) =
    _root_.bernoulli (n - i) * (↑(n.choose i) : ℚ)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n i : ℕ
pos :
  ∀ (h : i ≤ n),
    (∑ x ∈ range (n + 1), if n - x = i then _root_.bernoulli x * (↑(n.choose x) : ℚ) else 0) =
      _root_.bernoulli (n - i) * (↑(n.choose i) : ℚ)
⊢ (∑ x ∈ range (n + 1), if n - x = i then _root_.bernoulli x * (↑(n.choose x) : ℚ) else 0) =
    if i ≤ n then _root_.bernoulli (n - i) * (↑(n.choose i) : ℚ) else 0
have neg : ∀ (h : ¬i ≤ n), Eq (α := ℚ) (∑ x ∈ range (n + 1), if n - x = i then _root_.bernoulli x * (↑(n.choose x) : ℚ) else 0) 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n i : ℕ
h : i ≤ n
⊢ (∑ x ∈ range (n + 1), if n - x = i then _root_.bernoulli x * (↑(n.choose x) : ℚ) else 0) =
    _root_.bernoulli (n - i) * (↑(n.choose i) : ℚ)
have h₁ : ∀ x ∈ range (n + 1), n - x = i ↔ n - i = x
Tactic: convert! sum_ite_eq_of_mem (range (n + 1)) (n - i) _ (by grind) using 3
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n i : ℕ
h : i ≤ n
h₁ : ∀ x ∈ range (n + 1), n - x = i ↔ n - i = x
⊢ (∑ x ∈ range (n + 1), if n - x = i then _root_.bernoulli x * (↑(n.choose x) : ℚ) else 0) =
    _root_.bernoulli (n - i) * (↑(n.choose i) : ℚ)
have h₂ : n.choose i = n.choose (n - i)
Tactic: convert! sum_ite_eq_of_mem (range (n + 1)) (n - i) _ (by grind) using 3
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n : ℕ
⊢ eval 0 (bernoulli n) = _root_.bernoulli n
have rw : (bernoulli n).coeff 0 = _root_.bernoulli n
Tactic: rw [← coeff_zero_eq_eval_zero, coeff_bernoulli, if_pos (Nat.zero_le n), Nat.sub_zero,
    Nat.choose_zero_right, Nat.cast_one, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n : ℕ
rw : (bernoulli n).coeff 0 = _root_.bernoulli n
⊢ eval 0 (bernoulli n) = _root_.bernoulli n
have rw₁ : (if 0 ≤ n then _root_.bernoulli (n - 0) * (↑(n.choose 0) : ℚ) else 0) = _root_.bernoulli n
Tactic: rw [← coeff_zero_eq_eval_zero, coeff_bernoulli, if_pos (Nat.zero_le n), Nat.sub_zero,
    Nat.choose_zero_right, Nat.cast_one, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n : ℕ
rw : (bernoulli n).coeff 0 = _root_.bernoulli n
rw₁ : (if 0 ≤ n then _root_.bernoulli (n - 0) * (↑(n.choose 0) : ℚ) else 0) = _root_.bernoulli n
⊢ eval 0 (bernoulli n) = _root_.bernoulli n
have rw₂ : _root_.bernoulli (n - 0) * (↑(n.choose 0) : ℚ) = _root_.bernoulli n
Tactic: rw [← coeff_zero_eq_eval_zero, coeff_bernoulli, if_pos (Nat.zero_le n), Nat.sub_zero,
    Nat.choose_zero_right, Nat.cast_one, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n : ℕ
rw : (bernoulli n).coeff 0 = _root_.bernoulli n
rw₁ : (if 0 ≤ n then _root_.bernoulli (n - 0) * (↑(n.choose 0) : ℚ) else 0) = _root_.bernoulli n
rw₂ : _root_.bernoulli (n - 0) * (↑(n.choose 0) : ℚ) = _root_.bernoulli n
⊢ eval 0 (bernoulli n) = _root_.bernoulli n
have rw₃ : _root_.bernoulli n * (↑(n.choose 0) : ℚ) = _root_.bernoulli n
Tactic: rw [← coeff_zero_eq_eval_zero, coeff_bernoulli, if_pos (Nat.zero_le n), Nat.sub_zero,
    Nat.choose_zero_right, Nat.cast_one, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n : ℕ
rw : (bernoulli n).coeff 0 = _root_.bernoulli n
rw₁ : (if 0 ≤ n then _root_.bernoulli (n - 0) * (↑(n.choose 0) : ℚ) else 0) = _root_.bernoulli n
rw₂ : _root_.bernoulli (n - 0) * (↑(n.choose 0) : ℚ) = _root_.bernoulli n
rw₃ : _root_.bernoulli n * (↑(n.choose 0) : ℚ) = _root_.bernoulli n
⊢ eval 0 (bernoulli n) = _root_.bernoulli n
have rw₄ : _root_.bernoulli n * (↑1 : ℚ) = _root_.bernoulli n
Tactic: rw [← coeff_zero_eq_eval_zero, coeff_bernoulli, if_pos (Nat.zero_le n), Nat.sub_zero,
    Nat.choose_zero_right, Nat.cast_one, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n : ℕ
rw : (bernoulli n).coeff 0 = _root_.bernoulli n
rw₁ : (if 0 ≤ n then _root_.bernoulli (n - 0) * (↑(n.choose 0) : ℚ) else 0) = _root_.bernoulli n
rw₂ : _root_.bernoulli (n - 0) * (↑(n.choose 0) : ℚ) = _root_.bernoulli n
rw₃ : _root_.bernoulli n * (↑(n.choose 0) : ℚ) = _root_.bernoulli n
rw₄ : _root_.bernoulli n * (↑1 : ℚ) = _root_.bernoulli n
⊢ eval 0 (bernoulli n) = _root_.bernoulli n
have rw₅ : _root_.bernoulli n * 1 = _root_.bernoulli n
Tactic: rw [← coeff_zero_eq_eval_zero, coeff_bernoulli, if_pos (Nat.zero_le n), Nat.sub_zero,
    Nat.choose_zero_right, Nat.cast_one, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n : ℕ
rw : (bernoulli n).coeff 0 = _root_.bernoulli n
rw₁ : (if 0 ≤ n then _root_.bernoulli (n - 0) * (↑(n.choose 0) : ℚ) else 0) = _root_.bernoulli n
rw₂ : _root_.bernoulli (n - 0) * (↑(n.choose 0) : ℚ) = _root_.bernoulli n
rw₃ : _root_.bernoulli n * (↑(n.choose 0) : ℚ) = _root_.bernoulli n
rw₄ : _root_.bernoulli n * (↑1 : ℚ) = _root_.bernoulli n
rw₅ : _root_.bernoulli n * 1 = _root_.bernoulli n
⊢ eval 0 (bernoulli n) = _root_.bernoulli n
have rw₆ : _root_.bernoulli n = _root_.bernoulli n
Tactic: rw [← coeff_zero_eq_eval_zero, coeff_bernoulli, if_pos (Nat.zero_le n), Nat.sub_zero,
    Nat.choose_zero_right, Nat.cast_one, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n : ℕ
⊢ eval 1 (bernoulli n) = bernoulli' n
have simp : ∑ i ∈ range (n + 1), eval 1 ((monomial (n - i) : (a : ℚ) → ℚ[X]) (_root_.bernoulli i * (↑(n.choose i) : ℚ))) =
  bernoulli' n
Tactic: simp only [bernoulli, eval_finsetSum]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n : ℕ
⊢ ∑ i ∈ range (n + 1), eval 1 ((monomial (n - i) : (a : ℚ) → ℚ[X]) (_root_.bernoulli i * (↑(n.choose i) : ℚ))) =
    bernoulli' n
have simp : (if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n
Tactic: simp only [← succ_eq_add_one, sum_range_succ, mul_one, cast_one, choose_self,
    (_root_.bernoulli _).mul_comm, sum_bernoulli, one_pow, mul_one, eval_monomial, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n : ℕ
⊢ (if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n
have pos : ∀ (h : n = 1), (if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n
Tactic: by_cases h : n = 1
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n : ℕ
pos : ∀ (h : n = 1), (if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n
⊢ (if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n
have neg : ∀ (h : ¬n = 1), (if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n
Tactic: by_cases h : n = 1
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
⊢ eval (1 / 4) (bernoulli 3) = 3 / 64
have simp_rw : eval (1 / 4) (∑ i ∈ range 0, (monomial (3 - i) : (a : ℚ) → ℚ[X]) (_root_.bernoulli i * (↑(Nat.choose 3 i) : ℚ))) +
          _root_.bernoulli 0 * (↑(Nat.choose 3 0) : ℚ) * (1 / 4) ^ HSub.hSub (α := ℕ) 3 0 +
        _root_.bernoulli 1 * (↑(Nat.choose 3 1) : ℚ) * (1 / 4) ^ HSub.hSub (α := ℕ) 3 1 +
      _root_.bernoulli 2 * (↑(Nat.choose 3 2) : ℚ) * (1 / 4) ^ HSub.hSub (α := ℕ) 3 2 +
    _root_.bernoulli 3 * (↑(Nat.choose 3 3) : ℚ) * (1 / 4) ^ HSub.hSub (α := ℕ) 3 3 =
  3 / 64
Tactic: simp_rw [Polynomial.bernoulli, Finset.sum_range_succ, Polynomial.eval_add,
    Polynomial.eval_monomial]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
⊢ eval (1 / 4) (∑ i ∈ range 0, (monomial (3 - i) : (a : ℚ) → ℚ[X]) (_root_.bernoulli i * (↑(Nat.choose 3 i) : ℚ))) +
            _root_.bernoulli 0 * (↑(Nat.choose 3 0) : ℚ) * (1 / 4) ^ HSub.hSub (α := ℕ) 3 0 +
          _root_.bernoulli 1 * (↑(Nat.choose 3 1) : ℚ) * (1 / 4) ^ HSub.hSub (α := ℕ) 3 1 +
        _root_.bernoulli 2 * (↑(Nat.choose 3 2) : ℚ) * (1 / 4) ^ HSub.hSub (α := ℕ) 3 2 +
      _root_.bernoulli 3 * (↑(Nat.choose 3 3) : ℚ) * (1 / 4) ^ HSub.hSub (α := ℕ) 3 3 =
    3 / 64
have rw : _root_.bernoulli 0 * (↑(Nat.choose 3 0) : ℚ) * (1 / 4) ^ HSub.hSub (α := ℕ) 3 0 +
        -1 / 2 * (↑(Nat.choose 3 1) : ℚ) * (1 / 4) ^ HSub.hSub (α := ℕ) 3 1 +
      _root_.bernoulli 2 * (↑(Nat.choose 3 2) : ℚ) * (1 / 4) ^ HSub.hSub (α := ℕ) 3 2 +
    _root_.bernoulli 3 * (↑(Nat.choose 3 3) : ℚ) * (1 / 4) ^ HSub.hSub (α := ℕ) 3 3 =
  3 / 64
Tactic: rw [Finset.sum_range_zero, Polynomial.eval_zero, zero_add, _root_.bernoulli_one]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
⊢ _root_.bernoulli 0 * (↑(Nat.choose 3 0) : ℚ) * (1 / 4) ^ HSub.hSub (α := ℕ) 3 0 +
          -1 / 2 * (↑(Nat.choose 3 1) : ℚ) * (1 / 4) ^ HSub.hSub (α := ℕ) 3 1 +
        _root_.bernoulli 2 * (↑(Nat.choose 3 2) : ℚ) * (1 / 4) ^ HSub.hSub (α := ℕ) 3 2 +
      _root_.bernoulli 3 * (↑(Nat.choose 3 3) : ℚ) * (1 / 4) ^ HSub.hSub (α := ℕ) 3 3 =
    3 / 64
have rw : HMul.hMul (α := ℚ) 1 (↑(Nat.choose 3 0) : ℚ) * (1 / 4) ^ HSub.hSub (α := ℕ) 3 0 +
        -1 / 2 * (↑(Nat.choose 3 1) : ℚ) * (1 / 4) ^ HSub.hSub (α := ℕ) 3 1 +
      1 / 6 * (↑(Nat.choose 3 2) : ℚ) * (1 / 4) ^ HSub.hSub (α := ℕ) 3 2 +
    HMul.hMul (α := ℚ) 0 (↑(Nat.choose 3 3) : ℚ) * (1 / 4) ^ HSub.hSub (α := ℕ) 3 3 =
  3 / 64
Tactic: rw [bernoulli_eq_bernoulli'_of_ne_one zero_ne_one, bernoulli'_zero,
    bernoulli_eq_bernoulli'_of_ne_one (by decide : 2 ≠ 1), bernoulli'_two,
    bernoulli_eq_bernoulli'_of_ne_one (by decide : 3 ≠ 1), bernoulli'_three]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
k : ℕ
⊢ (derivative : (a : ℚ[X]) → ℚ[X]) (bernoulli (k + 1)) = HAdd.hAdd (α := ℚ[X]) (↑k : ℚ[X]) 1 * bernoulli k
have simp_rw : ∑ x ∈ range (k + 1 + 1),
    (monomial (k - x) : (a : ℚ) → ℚ[X]) (_root_.bernoulli x * (↑((k + 1).choose x) : ℚ) * (↑(k + 1 - x) : ℚ)) =
  HAdd.hAdd (α := ℚ[X]) (↑k : ℚ[X]) 1 *
    ∑ i ∈ range (k + 1), (monomial (k - i) : (a : ℚ) → ℚ[X]) (_root_.bernoulli i * (↑(k.choose i) : ℚ))
Tactic: simp_rw [bernoulli, derivative_sum, derivative_monomial, Nat.sub_sub, Nat.add_sub_add_right]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
k : ℕ
⊢ ∑ x ∈ range (k + 1 + 1),
      (monomial (k - x) : (a : ℚ) → ℚ[X]) (_root_.bernoulli x * (↑((k + 1).choose x) : ℚ) * (↑(k + 1 - x) : ℚ)) =
    HAdd.hAdd (α := ℚ[X]) (↑k : ℚ[X]) 1 *
      ∑ i ∈ range (k + 1), (monomial (k - i) : (a : ℚ) → ℚ[X]) (_root_.bernoulli i * (↑(k.choose i) : ℚ))
have rw : Eq (α := ℚ[X])
  (∑ x ∈ range (k + 1),
    (monomial (k - x) : (a : ℚ) → ℚ[X]) (_root_.bernoulli x * (↑((k + 1).choose x) : ℚ) * (↑(k + 1 - x) : ℚ)))
  (∑ i ∈ range (k + 1),
    HMul.hMul (β := ℚ[X]) (HAdd.hAdd (α := ℚ[X]) (↑k : ℚ[X]) 1)
      ((monomial (k - i) : (a : ℚ) → ℚ[X]) (_root_.bernoulli i * (↑(k.choose i) : ℚ)) : ℚ[X]))
Tactic: rw [range_add_one, sum_insert notMem_range_self, tsub_self, cast_zero, mul_zero,
    map_zero, zero_add, mul_sum]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
k : ℕ
⊢ Eq (α := ℚ[X])
    (∑ x ∈ range (k + 1),
      (monomial (k - x) : (a : ℚ) → ℚ[X]) (_root_.bernoulli x * (↑((k + 1).choose x) : ℚ) * (↑(k + 1 - x) : ℚ)))
    (∑ i ∈ range (k + 1),
      HMul.hMul (β := ℚ[X]) (HAdd.hAdd (α := ℚ[X]) (↑k : ℚ[X]) 1)
        ((monomial (k - i) : (a : ℚ) → ℚ[X]) (_root_.bernoulli i * (↑(k.choose i) : ℚ)) : ℚ[X]))
have refine : ∀ m ∈ range (k + 1),
  (monomial (k - m) : (a : ℚ) → ℚ[X]) (_root_.bernoulli m * (↑((k + 1).choose m) : ℚ) * (↑(k + 1 - m) : ℚ)) =
    HMul.hMul (β := ℚ[X]) (HAdd.hAdd (α := ℚ[X]) (↑k : ℚ[X]) 1)
      ((monomial (k - m) : (a : ℚ) → ℚ[X]) (_root_.bernoulli m * (↑(k.choose m) : ℚ)) : ℚ[X])
Tactic: refine sum_congr (by rfl) fun m _ => ?_
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
k m : ℕ
h : m ∈ range (k + 1)
| HMul.hMul (β := ℚ[X]) (HAdd.hAdd (α := ℚ[X]) (↑k : ℚ[X]) 1)
    ((monomial (k - m) : (a : ℚ) → ℚ[X]) (_root_.bernoulli m * (↑(k.choose m) : ℚ)) : ℚ[X])
have rw : ((monomial (k - m) : (a : ℚ) → ℚ[X]) (_root_.bernoulli m * (↑(k.choose m) : ℚ) * (↑(k + 1) : ℚ)) : ℚ[X])
Tactic: rw [← Nat.cast_one, ← Nat.cast_add, ← C_eq_natCast, C_mul_monomial, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
k m : ℕ
h : m ∈ range (k + 1)
⊢ (monomial (k - m) : (a : ℚ) → ℚ[X]) (_root_.bernoulli m * (↑((k + 1).choose m) : ℚ) * (↑(k + 1 - m) : ℚ)) =
    HMul.hMul (β := ℚ[X]) (HAdd.hAdd (α := ℚ[X]) (↑k : ℚ[X]) 1)
      ((monomial (k - m) : (a : ℚ) → ℚ[X]) (_root_.bernoulli m * (↑(k.choose m) : ℚ)) : ℚ[X])
have conv_rhs : Eq (α := ℚ[X])
  ((monomial (k - m) : (a : ℚ) → ℚ[X]) (_root_.bernoulli m * (↑((k + 1).choose m) : ℚ) * (↑(k + 1 - m) : ℚ)) : ℚ[X])
  ((monomial (k - m) : (a : ℚ) → ℚ[X]) (_root_.bernoulli m * (↑(k.choose m) : ℚ) * (↑(k + 1) : ℚ)) : ℚ[X])
Tactic: conv_rhs => rw [← Nat.cast_one, ← Nat.cast_add, ← C_eq_natCast, C_mul_monomial, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
k m : ℕ
h : m ∈ range (k + 1)
⊢ Eq (α := ℚ[X])
    ((monomial (k - m) : (a : ℚ) → ℚ[X]) (_root_.bernoulli m * (↑((k + 1).choose m) : ℚ) * (↑(k + 1 - m) : ℚ)) : ℚ[X])
    ((monomial (k - m) : (a : ℚ) → ℚ[X]) (_root_.bernoulli m * (↑(k.choose m) : ℚ) * (↑(k + 1) : ℚ)) : ℚ[X])
have rw : Eq (α := ℚ[X])
  ((monomial (k - m) : (a : ℚ) → ℚ[X]) (_root_.bernoulli m * (↑((k + 1).choose m * (k + 1 - m)) : ℚ)) : ℚ[X])
  ((monomial (k - m) : (a : ℚ) → ℚ[X]) (_root_.bernoulli m * (↑(k.choose m * (k + 1)) : ℚ)) : ℚ[X])
Tactic: rw [mul_assoc, mul_assoc, ← Nat.cast_mul, ← Nat.cast_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
k m : ℕ
h : m ∈ range (k + 1)
⊢ Eq (α := ℚ[X])
    ((monomial (k - m) : (a : ℚ) → ℚ[X]) (_root_.bernoulli m * (↑((k + 1).choose m * (k + 1 - m)) : ℚ)) : ℚ[X])
    ((monomial (k - m) : (a : ℚ) → ℚ[X]) (_root_.bernoulli m * (↑(k.choose m * (k + 1)) : ℚ)) : ℚ[X])
have h : (k + 1).choose m * (k + 1 - m) = k.choose m * (k + 1)
Tactic: congr 3
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
k m : ℕ
h : m ∈ range (k + 1)
⊢ (k + 1).choose m * (k + 1 - m) = k.choose m * (k + 1)
have h : k.choose m * (k + 1) = k.choose m * (k + 1)
Tactic: rw [(choose_mul_succ_eq k m).symm]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
⊢ (derivative : (a : ℚ[X]) → ℚ[X]) (bernoulli 0) = (↑0 : ℚ[X]) * bernoulli (HSub.hSub (α := ℕ) 0 1)
have zero : (derivative : (a : ℚ[X]) → ℚ[X]) (bernoulli 0) = 0 * bernoulli (HSub.hSub (α := ℕ) 0 1)
Tactic: rw [Nat.cast_zero, zero_mul, bernoulli_zero, derivative_one]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
zero : (derivative : (a : ℚ[X]) → ℚ[X]) (bernoulli 0) = 0 * bernoulli (HSub.hSub (α := ℕ) 0 1)
⊢ (derivative : (a : ℚ[X]) → ℚ[X]) (bernoulli 0) = (↑0 : ℚ[X]) * bernoulli (HSub.hSub (α := ℕ) 0 1)
have zero₁ : Eq (α := ℚ[X]) ((derivative : (a : ℚ[X]) → ℚ[X]) (bernoulli 0) : ℚ[X]) (0 : ℚ[X])
Tactic: rw [Nat.cast_zero, zero_mul, bernoulli_zero, derivative_one]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
zero : (derivative : (a : ℚ[X]) → ℚ[X]) (bernoulli 0) = 0 * bernoulli (HSub.hSub (α := ℕ) 0 1)
zero₁ : Eq (α := ℚ[X]) ((derivative : (a : ℚ[X]) → ℚ[X]) (bernoulli 0) : ℚ[X]) (0 : ℚ[X])
⊢ (derivative : (a : ℚ[X]) → ℚ[X]) (bernoulli 0) = (↑0 : ℚ[X]) * bernoulli (HSub.hSub (α := ℕ) 0 1)
have zero₂ : Eq (α := ℚ[X]) ((derivative : (a : ℚ[X]) → ℚ[X]) 1) 0
Tactic: rw [Nat.cast_zero, zero_mul, bernoulli_zero, derivative_one]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
zero : (derivative : (a : ℚ[X]) → ℚ[X]) (bernoulli 0) = 0 * bernoulli (HSub.hSub (α := ℕ) 0 1)
zero₁ : Eq (α := ℚ[X]) ((derivative : (a : ℚ[X]) → ℚ[X]) (bernoulli 0) : ℚ[X]) (0 : ℚ[X])
zero₂ : Eq (α := ℚ[X]) ((derivative : (a : ℚ[X]) → ℚ[X]) 1) 0
⊢ (derivative : (a : ℚ[X]) → ℚ[X]) (bernoulli 0) = (↑0 : ℚ[X]) * bernoulli (HSub.hSub (α := ℕ) 0 1)
have zero₃ : Eq (α := ℚ[X]) 0 0
Tactic: rw [Nat.cast_zero, zero_mul, bernoulli_zero, derivative_one]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
k : ℕ
⊢ (derivative : (a : ℚ[X]) → ℚ[X]) (bernoulli k) = (↑k : ℚ[X]) * bernoulli (k - 1)
have zero : (derivative : (a : ℚ[X]) → ℚ[X]) (bernoulli 0) = (↑0 : ℚ[X]) * bernoulli (HSub.hSub (α := ℕ) 0 1)
Tactic: cases k with
  | zero => rw [Nat.cast_zero, zero_mul, bernoulli_zero, derivative_one]
  | succ k => exact mod_cast derivative_bernoulli_add_one k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
k : ℕ
zero : (derivative : (a : ℚ[X]) → ℚ[X]) (bernoulli 0) = (↑0 : ℚ[X]) * bernoulli (HSub.hSub (α := ℕ) 0 1)
⊢ (derivative : (a : ℚ[X]) → ℚ[X]) (bernoulli k) = (↑k : ℚ[X]) * bernoulli (k - 1)
have succ : ∀ (k : ℕ), (derivative : (a : ℚ[X]) → ℚ[X]) (bernoulli (k + 1)) = (↑(k + 1) : ℚ[X]) * bernoulli (k + 1 - 1)
Tactic: cases k with
  | zero => rw [Nat.cast_zero, zero_mul, bernoulli_zero, derivative_one]
  | succ k => exact mod_cast derivative_bernoulli_add_one k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n : ℕ
⊢ Eq (α := ℚ[X]) (∑ k ∈ range (n + 1), HSMul.hSMul (α := ℚ) (↑((n + 1).choose k) : ℚ) (bernoulli k) : ℚ[X])
    ((monomial n : (a : ℚ) → ℚ[X]) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1) : ℚ[X])
have simp_rw : Eq (α := ℚ[X])
  (∑ k ∈ range (n + 1 - 0),
      ∑ k_1 ∈ range (n + 1 - (0 + k)),
        HSMul.hSMul (α := ℚ) (β := ℚ[X]) (↑((n + 1).choose (0 + k + k_1)) : ℚ)
          ((monomial (0 + k) : (a : ℚ) → ℚ[X])
              (_root_.bernoulli (0 + k + k_1 - (0 + k)) * (↑((0 + k + k_1).choose (0 + k)) : ℚ)) :
            ℚ[X]) :
    ℚ[X])
  ((monomial n : (a : ℚ) → ℚ[X]) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1) : ℚ[X])
Tactic: simp_rw [bernoulli_def, Finset.smul_sum, Finset.range_eq_Ico, ← Finset.sum_Ico_Ico_comm,
    Finset.sum_Ico_eq_sum_range]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n : ℕ
⊢ Eq (α := ℚ[X])
    (∑ k ∈ range (n + 1 - 0),
        ∑ k_1 ∈ range (n + 1 - (0 + k)),
          HSMul.hSMul (α := ℚ) (β := ℚ[X]) (↑((n + 1).choose (0 + k + k_1)) : ℚ)
            ((monomial (0 + k) : (a : ℚ) → ℚ[X])
                (_root_.bernoulli (0 + k + k_1 - (0 + k)) * (↑((0 + k + k_1).choose (0 + k)) : ℚ)) :
              ℚ[X]) :
      ℚ[X])
    ((monomial n : (a : ℚ) → ℚ[X]) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1) : ℚ[X])
have simp : ∑ x ∈ range (n + 1 - 0),
    ∑ x_1 ∈ range (n + 1 - x),
      HSMul.hSMul (α := ℚ) (β := ℚ[X]) (↑((n + 1).choose (x + x_1)) : ℚ)
        ((monomial x : (a : ℚ) → ℚ[X]) (_root_.bernoulli x_1 * (↑((x + x_1).choose x) : ℚ)) : ℚ[X]) =
  HAdd.hAdd (α := ℚ[X]) ((monomial n : (a : ℚ) → ℚ[X]) (↑n : ℚ)) ((monomial n : (a : ℚ) → ℚ[X]) 1)
Tactic: simp only [add_tsub_cancel_left, zero_add, map_add]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n : ℕ
⊢ ∑ x ∈ range (n + 1 - 0),
      ∑ x_1 ∈ range (n + 1 - x),
        HSMul.hSMul (α := ℚ) (β := ℚ[X]) (↑((n + 1).choose (x + x_1)) : ℚ)
          ((monomial x : (a : ℚ) → ℚ[X]) (_root_.bernoulli x_1 * (↑((x + x_1).choose x) : ℚ)) : ℚ[X]) =
    HAdd.hAdd (α := ℚ[X]) ((monomial n : (a : ℚ) → ℚ[X]) (↑n : ℚ)) ((monomial n : (a : ℚ) → ℚ[X]) 1)
have simp_rw : ∑ x ∈ range (n + 1 - 0),
    ∑ x_1 ∈ range (n + 1 - x),
      (monomial x : (a : ℚ) → ℚ[X])
        (HMul.hMul (α := ℚ) (↑((n + 1).choose (x + x_1)) : ℚ) (↑((x + x_1).choose x) : ℚ) * _root_.bernoulli x_1) =
  HAdd.hAdd (α := ℚ[X]) ((monomial n : (a : ℚ) → ℚ[X]) (↑n : ℚ)) ((monomial n : (a : ℚ) → ℚ[X]) 1)
Tactic: simp_rw [smul_monomial, mul_comm (_root_.bernoulli _) _, smul_eq_mul, ← mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n : ℕ
| ∑ x ∈ range (n + 1 - 0),
    ∑ x_1 ∈ range (n + 1 - x),
      (monomial x : (a : ℚ) → ℚ[X])
        (HMul.hMul (α := ℚ) (↑((n + 1).choose (x + x_1)) : ℚ) (↑((x + x_1).choose x) : ℚ) * _root_.bernoulli x_1)
have h : range (n + 1 - 0) = range (n + 1 - 0)
Tactic: apply_congr
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n : ℕ
h : range (n + 1 - 0) = range (n + 1 - 0)
| ∑ x ∈ range (n + 1 - 0),
    ∑ x_1 ∈ range (n + 1 - x),
      (monomial x : (a : ℚ) → ℚ[X])
        (HMul.hMul (α := ℚ) (↑((n + 1).choose (x + x_1)) : ℚ) (↑((x + x_1).choose x) : ℚ) * _root_.bernoulli x_1)
have a : ∀ x ∈ range (n + 1 - 0),
  Eq (α := ℚ[X])
    (∑ x_1 ∈ range (n + 1 - x),
      (monomial x : (a : ℚ) → ℚ[X])
        (HMul.hMul (α := ℚ) (↑((n + 1).choose (x + x_1)) : ℚ) (↑((x + x_1).choose x) : ℚ) * _root_.bernoulli x_1))
    (∑ x_1 ∈ range (n + 1 - x),
      HSMul.hSMul (β := ℚ[X]) ((↑((n + 1 - x).choose x_1) : ℚ) * _root_.bernoulli x_1)
        ((monomial x : (a : ℚ) → ℚ[X]) (↑((n + 1).choose x) : ℚ)))
Tactic: apply_congr
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n x : ℕ
h : x ∈ range (n + 1 - 0)
| ∑ x_1 ∈ range (n + 1 - x),
    (monomial x : (a : ℚ) → ℚ[X])
      (HMul.hMul (α := ℚ) (↑((n + 1).choose (x + x_1)) : ℚ) (↑((x + x_1).choose x) : ℚ) * _root_.bernoulli x_1)
have h : range (n + 1 - x) = range (n + 1 - x)
Tactic: apply_congr
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n x : ℕ
h_1 : x ∈ range (n + 1 - 0)
h : range (n + 1 - x) = range (n + 1 - x)
| ∑ x_1 ∈ range (n + 1 - x),
    (monomial x : (a : ℚ) → ℚ[X])
      (HMul.hMul (α := ℚ) (↑((n + 1).choose (x + x_1)) : ℚ) (↑((x + x_1).choose x) : ℚ) * _root_.bernoulli x_1)
have a : ∀ x_1 ∈ range (n + 1 - x),
  (monomial x : (a : ℚ) → ℚ[X])
      (HMul.hMul (α := ℚ) (↑((n + 1).choose (x + x_1)) : ℚ) (↑((x + x_1).choose x) : ℚ) * _root_.bernoulli x_1) =
    HSMul.hSMul (β := ℚ[X]) ((↑((n + 1 - x).choose x_1) : ℚ) * _root_.bernoulli x_1)
      ((monomial x : (a : ℚ) → ℚ[X]) (↑((n + 1).choose x) : ℚ))
Tactic: apply_congr