awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n x : ℕ
h : x ∈ range (n + 1 - 0)
x_1 : ℕ
h_1 : 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) : ℚ))
have a : HSMul.hSMul (β := ℚ[X]) ((↑((n + 1 - x).choose x_1) : ℚ) * _root_.bernoulli x_1)
  ((monomial x : (a : ℚ) → ℚ[X]) (↑((n + 1).choose x) : ℚ))
Tactic: rw [← Nat.cast_mul, choose_mul (le_add_right _ _), Nat.cast_mul, add_tsub_cancel_left,
          mul_assoc, mul_comm, ← smul_eq_mul, ← smul_monomial]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n x : ℕ
h : x ∈ range (n + 1 - 0)
x_1 : ℕ
h_1 : 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) : ℚ))
have a : (monomial x : (a : ℚ) → ℚ[X]) ((↑((n + 1).choose (x + x_1) * (x + x_1).choose x) : ℚ) * _root_.bernoulli x_1)
Tactic: · rw [← Nat.cast_mul, choose_mul (le_add_right _ _), Nat.cast_mul, add_tsub_cancel_left,
          mul_assoc, mul_comm, ← smul_eq_mul, ← smul_monomial]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n x : ℕ
h : x ∈ range (n + 1 - 0)
x_1 : ℕ
h_1 : x_1 ∈ range (n + 1 - x)
a : (monomial x : (a : ℚ) → ℚ[X]) ((↑((n + 1).choose (x + x_1) * (x + x_1).choose x) : ℚ) * _root_.bernoulli x_1)
⊢ (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) : ℚ))
have a₁ : (monomial x : (a : ℚ) → ℚ[X]) ((↑((n + 1).choose x * (n + 1 - x).choose (x + x_1 - x)) : ℚ) * _root_.bernoulli x_1)
Tactic: · rw [← Nat.cast_mul, choose_mul (le_add_right _ _), Nat.cast_mul, add_tsub_cancel_left,
          mul_assoc, mul_comm, ← smul_eq_mul, ← smul_monomial]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n x : ℕ
h : x ∈ range (n + 1 - 0)
x_1 : ℕ
h_1 : x_1 ∈ range (n + 1 - x)
a : (monomial x : (a : ℚ) → ℚ[X]) ((↑((n + 1).choose (x + x_1) * (x + x_1).choose x) : ℚ) * _root_.bernoulli x_1)
a₁ : (monomial x : (a : ℚ) → ℚ[X]) ((↑((n + 1).choose x * (n + 1 - x).choose (x + x_1 - x)) : ℚ) * _root_.bernoulli x_1)
⊢ (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) : ℚ))
have a₂ : (monomial x : (a : ℚ) → ℚ[X])
  (HMul.hMul (α := ℚ) (↑((n + 1).choose x) : ℚ) (↑((n + 1 - x).choose (x + x_1 - x)) : ℚ) * _root_.bernoulli x_1)
Tactic: · rw [← Nat.cast_mul, choose_mul (le_add_right _ _), Nat.cast_mul, add_tsub_cancel_left,
          mul_assoc, mul_comm, ← smul_eq_mul, ← smul_monomial]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n x : ℕ
h : x ∈ range (n + 1 - 0)
x_1 : ℕ
h_1 : x_1 ∈ range (n + 1 - x)
a : (monomial x : (a : ℚ) → ℚ[X]) ((↑((n + 1).choose (x + x_1) * (x + x_1).choose x) : ℚ) * _root_.bernoulli x_1)
a₁ : (monomial x : (a : ℚ) → ℚ[X]) ((↑((n + 1).choose x * (n + 1 - x).choose (x + x_1 - x)) : ℚ) * _root_.bernoulli x_1)
a₂ :
  (monomial x : (a : ℚ) → ℚ[X])
    (HMul.hMul (α := ℚ) (↑((n + 1).choose x) : ℚ) (↑((n + 1 - x).choose (x + x_1 - x)) : ℚ) * _root_.bernoulli x_1)
⊢ (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) : ℚ))
have a₃ : (monomial x : (a : ℚ) → ℚ[X])
  (HMul.hMul (α := ℚ) (↑((n + 1).choose x) : ℚ) (↑((n + 1 - x).choose x_1) : ℚ) * _root_.bernoulli x_1)
Tactic: · rw [← Nat.cast_mul, choose_mul (le_add_right _ _), Nat.cast_mul, add_tsub_cancel_left,
          mul_assoc, mul_comm, ← smul_eq_mul, ← smul_monomial]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n x : ℕ
h : x ∈ range (n + 1 - 0)
x_1 : ℕ
h_1 : x_1 ∈ range (n + 1 - x)
a : (monomial x : (a : ℚ) → ℚ[X]) ((↑((n + 1).choose (x + x_1) * (x + x_1).choose x) : ℚ) * _root_.bernoulli x_1)
a₁ : (monomial x : (a : ℚ) → ℚ[X]) ((↑((n + 1).choose x * (n + 1 - x).choose (x + x_1 - x)) : ℚ) * _root_.bernoulli x_1)
a₂ :
  (monomial x : (a : ℚ) → ℚ[X])
    (HMul.hMul (α := ℚ) (↑((n + 1).choose x) : ℚ) (↑((n + 1 - x).choose (x + x_1 - x)) : ℚ) * _root_.bernoulli x_1)
a₃ :
  (monomial x : (a : ℚ) → ℚ[X])
    (HMul.hMul (α := ℚ) (↑((n + 1).choose x) : ℚ) (↑((n + 1 - x).choose x_1) : ℚ) * _root_.bernoulli x_1)
⊢ (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) : ℚ))
have a₄ : (monomial x : (a : ℚ) → ℚ[X]) ((↑((n + 1).choose x) : ℚ) * ((↑((n + 1 - x).choose x_1) : ℚ) * _root_.bernoulli x_1))
Tactic: · rw [← Nat.cast_mul, choose_mul (le_add_right _ _), Nat.cast_mul, add_tsub_cancel_left,
          mul_assoc, mul_comm, ← smul_eq_mul, ← smul_monomial]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n x : ℕ
h : x ∈ range (n + 1 - 0)
x_1 : ℕ
h_1 : x_1 ∈ range (n + 1 - x)
a : (monomial x : (a : ℚ) → ℚ[X]) ((↑((n + 1).choose (x + x_1) * (x + x_1).choose x) : ℚ) * _root_.bernoulli x_1)
a₁ : (monomial x : (a : ℚ) → ℚ[X]) ((↑((n + 1).choose x * (n + 1 - x).choose (x + x_1 - x)) : ℚ) * _root_.bernoulli x_1)
a₂ :
  (monomial x : (a : ℚ) → ℚ[X])
    (HMul.hMul (α := ℚ) (↑((n + 1).choose x) : ℚ) (↑((n + 1 - x).choose (x + x_1 - x)) : ℚ) * _root_.bernoulli x_1)
a₃ :
  (monomial x : (a : ℚ) → ℚ[X])
    (HMul.hMul (α := ℚ) (↑((n + 1).choose x) : ℚ) (↑((n + 1 - x).choose x_1) : ℚ) * _root_.bernoulli x_1)
a₄ :
  (monomial x : (a : ℚ) → ℚ[X]) ((↑((n + 1).choose x) : ℚ) * ((↑((n + 1 - x).choose x_1) : ℚ) * _root_.bernoulli x_1))
⊢ (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) : ℚ))
have a₅ : (monomial x : (a : ℚ) → ℚ[X]) ((↑((n + 1 - x).choose x_1) : ℚ) * _root_.bernoulli x_1 * (↑((n + 1).choose x) : ℚ))
Tactic: · rw [← Nat.cast_mul, choose_mul (le_add_right _ _), Nat.cast_mul, add_tsub_cancel_left,
          mul_assoc, mul_comm, ← smul_eq_mul, ← smul_monomial]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n x : ℕ
h : x ∈ range (n + 1 - 0)
x_1 : ℕ
h_1 : x_1 ∈ range (n + 1 - x)
a : (monomial x : (a : ℚ) → ℚ[X]) ((↑((n + 1).choose (x + x_1) * (x + x_1).choose x) : ℚ) * _root_.bernoulli x_1)
a₁ : (monomial x : (a : ℚ) → ℚ[X]) ((↑((n + 1).choose x * (n + 1 - x).choose (x + x_1 - x)) : ℚ) * _root_.bernoulli x_1)
a₂ :
  (monomial x : (a : ℚ) → ℚ[X])
    (HMul.hMul (α := ℚ) (↑((n + 1).choose x) : ℚ) (↑((n + 1 - x).choose (x + x_1 - x)) : ℚ) * _root_.bernoulli x_1)
a₃ :
  (monomial x : (a : ℚ) → ℚ[X])
    (HMul.hMul (α := ℚ) (↑((n + 1).choose x) : ℚ) (↑((n + 1 - x).choose x_1) : ℚ) * _root_.bernoulli x_1)
a₄ :
  (monomial x : (a : ℚ) → ℚ[X]) ((↑((n + 1).choose x) : ℚ) * ((↑((n + 1 - x).choose x_1) : ℚ) * _root_.bernoulli x_1))
a₅ : (monomial x : (a : ℚ) → ℚ[X]) ((↑((n + 1 - x).choose x_1) : ℚ) * _root_.bernoulli x_1 * (↑((n + 1).choose 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) : ℚ))
have a₆ : (monomial x : (a : ℚ) → ℚ[X])
  (HSMul.hSMul (β := ℚ) ((↑((n + 1 - x).choose x_1) : ℚ) * _root_.bernoulli x_1) (↑((n + 1).choose x) : ℚ))
Tactic: · rw [← Nat.cast_mul, choose_mul (le_add_right _ _), Nat.cast_mul, add_tsub_cancel_left,
          mul_assoc, mul_comm, ← smul_eq_mul, ← smul_monomial]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n x : ℕ
h : x ∈ range (n + 1 - 0)
x_1 : ℕ
h_1 : x_1 ∈ range (n + 1 - x)
a : (monomial x : (a : ℚ) → ℚ[X]) ((↑((n + 1).choose (x + x_1) * (x + x_1).choose x) : ℚ) * _root_.bernoulli x_1)
a₁ : (monomial x : (a : ℚ) → ℚ[X]) ((↑((n + 1).choose x * (n + 1 - x).choose (x + x_1 - x)) : ℚ) * _root_.bernoulli x_1)
a₂ :
  (monomial x : (a : ℚ) → ℚ[X])
    (HMul.hMul (α := ℚ) (↑((n + 1).choose x) : ℚ) (↑((n + 1 - x).choose (x + x_1 - x)) : ℚ) * _root_.bernoulli x_1)
a₃ :
  (monomial x : (a : ℚ) → ℚ[X])
    (HMul.hMul (α := ℚ) (↑((n + 1).choose x) : ℚ) (↑((n + 1 - x).choose x_1) : ℚ) * _root_.bernoulli x_1)
a₄ :
  (monomial x : (a : ℚ) → ℚ[X]) ((↑((n + 1).choose x) : ℚ) * ((↑((n + 1 - x).choose x_1) : ℚ) * _root_.bernoulli x_1))
a₅ : (monomial x : (a : ℚ) → ℚ[X]) ((↑((n + 1 - x).choose x_1) : ℚ) * _root_.bernoulli x_1 * (↑((n + 1).choose x) : ℚ))
a₆ :
  (monomial x : (a : ℚ) → ℚ[X])
    (HSMul.hSMul (β := ℚ) ((↑((n + 1 - x).choose x_1) : ℚ) * _root_.bernoulli x_1) (↑((n + 1).choose 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) : ℚ))
have a₇ : HSMul.hSMul (β := ℚ[X]) ((↑((n + 1 - x).choose x_1) : ℚ) * _root_.bernoulli x_1)
  ((monomial x : (a : ℚ) → ℚ[X]) (↑((n + 1).choose x) : ℚ))
Tactic: · rw [← Nat.cast_mul, choose_mul (le_add_right _ _), Nat.cast_mul, add_tsub_cancel_left,
          mul_assoc, mul_comm, ← smul_eq_mul, ← smul_monomial]
-- 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
      · skip
      · rw [← Nat.cast_mul, choose_mul (le_add_right _ _), Nat.cast_mul, add_tsub_cancel_left,
          mul_assoc, mul_comm, ← smul_eq_mul, ← smul_monomial]
-- 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
      · skip
      · rw [← Nat.cast_mul, choose_mul (le_add_right _ _), Nat.cast_mul, add_tsub_cancel_left,
          mul_assoc, mul_comm, ← smul_eq_mul, ← smul_monomial]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n x : ℕ
h : 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) : ℚ)))
have a : ∑ 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: conv =>
      apply_congr
      · skip
      · rw [← Nat.cast_mul, choose_mul (le_add_right _ _), Nat.cast_mul, add_tsub_cancel_left,
          mul_assoc, mul_comm, ← smul_eq_mul, ← smul_monomial]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n x : ℕ
h : x ∈ range (n + 1 - 0)
conv :
  ∑ 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)
⊢ 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) : ℚ)))
have a : ∑ 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: · conv =>
      apply_congr
      · skip
      · rw [← Nat.cast_mul, choose_mul (le_add_right _ _), Nat.cast_mul, add_tsub_cancel_left,
          mul_assoc, mul_comm, ← smul_eq_mul, ← smul_monomial]
-- 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
    · skip
    · conv =>
      apply_congr
      · skip
      · rw [← Nat.cast_mul, choose_mul (le_add_right _ _), Nat.cast_mul, add_tsub_cancel_left,
          mul_assoc, mul_comm, ← smul_eq_mul, ← smul_monomial]
-- 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
    · skip
    · conv =>
      apply_congr
      · skip
      · rw [← Nat.cast_mul, choose_mul (le_add_right _ _), Nat.cast_mul, add_tsub_cancel_left,
          mul_assoc, mul_comm, ← smul_eq_mul, ← smul_monomial]
-- 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) =
    HAdd.hAdd (α := ℚ[X]) ((monomial n : (a : ℚ) → ℚ[X]) (↑n : ℚ)) ((monomial n : (a : ℚ) → ℚ[X]) 1)
have conv_lhs : ∑ x ∈ range (n + 1 - 0),
    ∑ 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) : ℚ)) =
  HAdd.hAdd (α := ℚ[X]) ((monomial n : (a : ℚ) → ℚ[X]) (↑n : ℚ)) ((monomial n : (a : ℚ) → ℚ[X]) 1)
Tactic: conv_lhs =>
    apply_congr
    · skip
    · conv =>
      apply_congr
      · skip
      · rw [← Nat.cast_mul, choose_mul (le_add_right _ _), Nat.cast_mul, add_tsub_cancel_left,
          mul_assoc, mul_comm, ← smul_eq_mul, ← smul_monomial]
-- 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 - x).choose x_1) : ℚ) * _root_.bernoulli x_1)
          ((monomial x : (a : ℚ) → ℚ[X]) (↑((n + 1).choose x) : ℚ)) =
    HAdd.hAdd (α := ℚ[X]) ((monomial n : (a : ℚ) → ℚ[X]) (↑n : ℚ)) ((monomial n : (a : ℚ) → ℚ[X]) 1)
have simp_rw : ∑ x ∈ range (n + 1),
    HSMul.hSMul (α := ℚ) (β := ℚ[X]) (∑ i ∈ range (n + 1 - x), (↑((n + 1 - x).choose i) : ℚ) * _root_.bernoulli i)
      ((monomial x : (a : ℚ) → ℚ[X]) (↑((n + 1).choose x) : ℚ)) =
  HAdd.hAdd (α := ℚ[X]) ((monomial n : (a : ℚ) → ℚ[X]) (↑n : ℚ)) ((monomial n : (a : ℚ) → ℚ[X]) 1)
Tactic: simp_rw [← sum_smul, Nat.sub_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n : ℕ
⊢ ∑ x ∈ range (n + 1),
      HSMul.hSMul (α := ℚ) (β := ℚ[X]) (∑ i ∈ range (n + 1 - x), (↑((n + 1 - x).choose i) : ℚ) * _root_.bernoulli i)
        ((monomial x : (a : ℚ) → ℚ[X]) (↑((n + 1).choose x) : ℚ)) =
    HAdd.hAdd (α := ℚ[X]) ((monomial n : (a : ℚ) → ℚ[X]) (↑n : ℚ)) ((monomial n : (a : ℚ) → ℚ[X]) 1)
have rw : HSMul.hSMul (α := ℚ) (β := ℚ[X]) (∑ i ∈ range (n + 1 - n), (↑((n + 1 - n).choose i) : ℚ) * _root_.bernoulli i)
      ((monomial n : (a : ℚ) → ℚ[X]) (↑((n + 1).choose n) : ℚ)) +
    ∑ x ∈ range n,
      HSMul.hSMul (α := ℚ) (β := ℚ[X]) (∑ i ∈ range (n + 1 - x), (↑((n + 1 - x).choose i) : ℚ) * _root_.bernoulli i)
        ((monomial x : (a : ℚ) → ℚ[X]) (↑((n + 1).choose x) : ℚ)) =
  HAdd.hAdd (α := ℚ[X]) ((monomial n : (a : ℚ) → ℚ[X]) (↑n : ℚ)) ((monomial n : (a : ℚ) → ℚ[X]) 1)
Tactic: rw [sum_range_succ_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n : ℕ
⊢ HSMul.hSMul (α := ℚ) (β := ℚ[X]) (∑ i ∈ range (n + 1 - n), (↑((n + 1 - n).choose i) : ℚ) * _root_.bernoulli i)
        ((monomial n : (a : ℚ) → ℚ[X]) (↑((n + 1).choose n) : ℚ)) +
      ∑ x ∈ range n,
        HSMul.hSMul (α := ℚ) (β := ℚ[X]) (∑ i ∈ range (n + 1 - x), (↑((n + 1 - x).choose i) : ℚ) * _root_.bernoulli i)
          ((monomial x : (a : ℚ) → ℚ[X]) (↑((n + 1).choose x) : ℚ)) =
    HAdd.hAdd (α := ℚ[X]) ((monomial n : (a : ℚ) → ℚ[X]) (↑n : ℚ)) ((monomial n : (a : ℚ) → ℚ[X]) 1)
have simp : Eq (α := ℚ[X])
  (∑ x ∈ range n,
    HSMul.hSMul (α := ℚ) (β := ℚ[X]) (∑ i ∈ range (n + 1 - x), (↑((n + 1 - x).choose i) : ℚ) * _root_.bernoulli i)
      ((monomial x : (a : ℚ) → ℚ[X]) (↑((n + 1).choose x) : ℚ)))
  0
Tactic: simp only [add_eq_left, mul_one, cast_one, cast_add, add_tsub_cancel_left,
    choose_succ_self_right, one_smul, _root_.bernoulli_zero, sum_singleton, zero_add,
    map_add, range_one, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n : ℕ
⊢ Eq (α := ℚ[X])
    (∑ x ∈ range n,
      HSMul.hSMul (α := ℚ) (β := ℚ[X]) (∑ i ∈ range (n + 1 - x), (↑((n + 1 - x).choose i) : ℚ) * _root_.bernoulli i)
        ((monomial x : (a : ℚ) → ℚ[X]) (↑((n + 1).choose x) : ℚ)))
    0
have refine : ∀ x ∈ range n,
  HSMul.hSMul (α := ℚ) (β := ℚ[X]) (∑ i ∈ range (n + 1 - x), (↑((n + 1 - x).choose i) : ℚ) * _root_.bernoulli i)
      ((monomial x : (a : ℚ) → ℚ[X]) (↑((n + 1).choose x) : ℚ)) =
    0
Tactic: refine sum_eq_zero ?_
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (hypothesis)
Goal:
n x : ℕ
hx : x ∈ range n
⊢ HSMul.hSMul (α := ℚ) (β := ℚ[X]) (∑ i ∈ range (n + 1 - x), (↑((n + 1 - x).choose i) : ℚ) * _root_.bernoulli i)
      ((monomial x : (a : ℚ) → ℚ[X]) (↑((n + 1).choose x) : ℚ)) =
    0
have hx1 : n + 1 - x ≠ 1
Tactic: have hx1 : n + 1 - x ≠ 1 := by grind
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n : ℕ
⊢ (n + 1) • bernoulli n = (n + 1) • HPow.hPow (α := ℚ[X]) X n - ∑ k ∈ range n, (n + 1).choose k • bernoulli k
have simp_rw : HSMul.hSMul (α := ℚ) (↑(n + 1) : ℚ) (bernoulli n) =
  HSMul.hSMul (α := ℚ) (↑(n + 1) : ℚ) (HPow.hPow (α := ℚ[X]) X n) -
    ∑ x ∈ range n, HSMul.hSMul (α := ℚ) (↑((n + 1).choose x) : ℚ) (bernoulli x)
Tactic: simp_rw [← cast_smul_eq_nsmul (R := ℚ), smul_X_eq_monomial,
    Nat.cast_succ, ← sum_bernoulli n, sum_range_succ_sub_sum, choose_succ_self_right,
    Nat.cast_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n : ℕ
simp_rw :
  HSMul.hSMul (α := ℚ) (↑(n + 1) : ℚ) (bernoulli n) =
    HSMul.hSMul (α := ℚ) (↑(n + 1) : ℚ) (HPow.hPow (α := ℚ[X]) X n) -
      ∑ x ∈ range n, HSMul.hSMul (α := ℚ) (↑((n + 1).choose x) : ℚ) (bernoulli x)
⊢ (n + 1) • bernoulli n = (n + 1) • HPow.hPow (α := ℚ[X]) X n - ∑ k ∈ range n, (n + 1).choose k • bernoulli k
have simp_rw₁ : HSMul.hSMul (α := ℚ) (↑(n + 1) : ℚ) (bernoulli n) =
  HSub.hSub (α := ℚ[X]) ((monomial n : (a : ℚ) → ℚ[X]) (↑(n + 1) : ℚ))
    (∑ x ∈ range n, HSMul.hSMul (α := ℚ) (↑((n + 1).choose x) : ℚ) (bernoulli x))
Tactic: simp_rw [← cast_smul_eq_nsmul (R := ℚ), smul_X_eq_monomial,
    Nat.cast_succ, ← sum_bernoulli n, sum_range_succ_sub_sum, choose_succ_self_right,
    Nat.cast_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n : ℕ
simp_rw :
  HSMul.hSMul (α := ℚ) (↑(n + 1) : ℚ) (bernoulli n) =
    HSMul.hSMul (α := ℚ) (↑(n + 1) : ℚ) (HPow.hPow (α := ℚ[X]) X n) -
      ∑ x ∈ range n, HSMul.hSMul (α := ℚ) (↑((n + 1).choose x) : ℚ) (bernoulli x)
simp_rw₁ :
  HSMul.hSMul (α := ℚ) (↑(n + 1) : ℚ) (bernoulli n) =
    HSub.hSub (α := ℚ[X]) ((monomial n : (a : ℚ) → ℚ[X]) (↑(n + 1) : ℚ))
      (∑ x ∈ range n, HSMul.hSMul (α := ℚ) (↑((n + 1).choose x) : ℚ) (bernoulli x))
⊢ (n + 1) • bernoulli n = (n + 1) • HPow.hPow (α := ℚ[X]) X n - ∑ k ∈ range n, (n + 1).choose k • bernoulli k
have simp_rw₂ : HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 • bernoulli n =
  HSub.hSub (α := ℚ[X]) (β := ℚ[X]) ((monomial n : (a : ℚ) → ℚ[X]) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1) : ℚ[X])
    (∑ x ∈ range n, HSMul.hSMul (α := ℚ) (↑((n + 1).choose x) : ℚ) (bernoulli x) : ℚ[X])
Tactic: simp_rw [← cast_smul_eq_nsmul (R := ℚ), smul_X_eq_monomial,
    Nat.cast_succ, ← sum_bernoulli n, sum_range_succ_sub_sum, choose_succ_self_right,
    Nat.cast_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n : ℕ
simp_rw :
  HSMul.hSMul (α := ℚ) (↑(n + 1) : ℚ) (bernoulli n) =
    HSMul.hSMul (α := ℚ) (↑(n + 1) : ℚ) (HPow.hPow (α := ℚ[X]) X n) -
      ∑ x ∈ range n, HSMul.hSMul (α := ℚ) (↑((n + 1).choose x) : ℚ) (bernoulli x)
simp_rw₁ :
  HSMul.hSMul (α := ℚ) (↑(n + 1) : ℚ) (bernoulli n) =
    HSub.hSub (α := ℚ[X]) ((monomial n : (a : ℚ) → ℚ[X]) (↑(n + 1) : ℚ))
      (∑ x ∈ range n, HSMul.hSMul (α := ℚ) (↑((n + 1).choose x) : ℚ) (bernoulli x))
simp_rw₂ :
  HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 • bernoulli n =
    HSub.hSub (α := ℚ[X]) (β := ℚ[X]) ((monomial n : (a : ℚ) → ℚ[X]) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1) : ℚ[X])
      (∑ x ∈ range n, HSMul.hSMul (α := ℚ) (↑((n + 1).choose x) : ℚ) (bernoulli x) : ℚ[X])
⊢ (n + 1) • bernoulli n = (n + 1) • HPow.hPow (α := ℚ[X]) X n - ∑ k ∈ range n, (n + 1).choose k • bernoulli k
have simp_rw₃ : HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 • bernoulli n =
  HSub.hSub (α := ℚ[X]) (∑ k ∈ range (n + 1), HSMul.hSMul (α := ℚ) (↑((n + 1).choose k) : ℚ) (bernoulli k))
    (∑ x ∈ range n, HSMul.hSMul (α := ℚ) (↑((n + 1).choose x) : ℚ) (bernoulli x))
Tactic: simp_rw [← cast_smul_eq_nsmul (R := ℚ), smul_X_eq_monomial,
    Nat.cast_succ, ← sum_bernoulli n, sum_range_succ_sub_sum, choose_succ_self_right,
    Nat.cast_succ]