awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n : ℕ
simp : (if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n
⊢ ∑ i ∈ range (n + 1), eval 1 ((monomial (n - i) : (a : ℚ) → ℚ[X]) (_root_.bernoulli i * (↑(n.choose i) : ℚ))) =
    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]

Premises used: one_pow, Nat.succ_eq_add_one, bernoulli, Rat.mul_comm, mul_one, sum_bernoulli, Nat.cast_one, Finset.sum_range_succ, Nat.choose_self, one_mul, Polynomial.eval_monomial
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n : ℕ
pos : ∀ (h : n = 1), (if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n
neg : ∀ (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

Tactic:
by_cases h : n = 1
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n : ℕ
h : n = 1
⊢ (if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n

Tactic:
norm_num [h]
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n : ℕ
h : ¬n = 1
⊢ (if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n

Tactic:
simp [h, bernoulli_eq_bernoulli'_of_ne_one h]

Premises used: bernoulli_eq_bernoulli'_of_ne_one
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
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
⊢ eval (1 / 4) (bernoulli 3) = 3 / 64

Tactic:
simp_rw [Polynomial.bernoulli, Finset.sum_range_succ, Polynomial.eval_add,
    Polynomial.eval_monomial]

Premises used: Polynomial.bernoulli, Polynomial.eval_add, Finset.sum_range_succ, Polynomial.eval_monomial
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
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
⊢ 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:
rw [Finset.sum_range_zero, Polynomial.eval_zero, zero_add, _root_.bernoulli_one]

Premises used: Finset.sum_range_zero, Polynomial.eval_zero, zero_add, bernoulli_one
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
⊢ Ne (α := ℕ) 2 1

Tactic:
decide
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
⊢ Ne (α := ℕ) 3 1

Tactic:
decide
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
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
⊢ _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 [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]

Premises used: bernoulli'_two, zero_ne_one, bernoulli'_three, bernoulli_eq_bernoulli'_of_ne_one, bernoulli'_zero
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
⊢ 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:
norm_num
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
k : ℕ
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) : ℚ))
⊢ (derivative : (a : ℚ[X]) → ℚ[X]) (bernoulli (k + 1)) = HAdd.hAdd (α := ℚ[X]) (↑k : ℚ[X]) 1 * bernoulli k

Tactic:
simp_rw [bernoulli, derivative_sum, derivative_monomial, Nat.sub_sub, Nat.add_sub_add_right]

Premises used: Polynomial.derivative_sum, Polynomial.derivative_monomial, Polynomial.bernoulli, Nat.sub_sub, Nat.add_sub_add_right
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
k : ℕ
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]))
⊢ ∑ 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:
rw [range_add_one, sum_insert notMem_range_self, tsub_self, cast_zero, mul_zero,
    map_zero, zero_add, mul_sum]

Premises used: Finset.mul_sum, tsub_self, map_zero, Finset.range_add_one, zero_add, MulZeroClass.mul_zero, Finset.notMem_range_self, Nat.cast_zero, Finset.sum_insert
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
k : ℕ
⊢ range (k + 1) = range (k + 1)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
k : ℕ
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])
⊢ 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:
refine sum_congr (by rfl) fun m _ => ?_

Premises used: Finset.sum_congr
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
k m : ℕ
h : m ∈ range (k + 1)
rw : ((monomial (k - m) : (a : ℚ) → ℚ[X]) (_root_.bernoulli m * (↑(k.choose m) : ℚ) * (↑(k + 1) : ℚ)) : ℚ[X])
| HMul.hMul (β := ℚ[X]) (HAdd.hAdd (α := ℚ[X]) (↑k : ℚ[X]) 1)
    ((monomial (k - m) : (a : ℚ) → ℚ[X]) (_root_.bernoulli m * (↑(k.choose m) : ℚ)) : ℚ[X])

Tactic:
rw [← Nat.cast_one, ← Nat.cast_add, ← C_eq_natCast, C_mul_monomial, mul_comm]

Premises used: Polynomial.C_eq_natCast, Polynomial.C_mul_monomial, Nat.cast_add, mul_comm, Nat.cast_one
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
k m : ℕ
h : m ∈ range (k + 1)
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])
⊢ (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:
conv_rhs => rw [← Nat.cast_one, ← Nat.cast_add, ← C_eq_natCast, C_mul_monomial, mul_comm]

Premises used: Polynomial.C_eq_natCast, Polynomial.C_mul_monomial, Nat.cast_add, mul_comm, Nat.cast_one
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
k m : ℕ
h : m ∈ range (k + 1)
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])
⊢ 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]

Premises used: mul_assoc, Nat.cast_mul
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
k m : ℕ
h_1 : m ∈ range (k + 1)
h : (k + 1).choose m * (k + 1 - m) = k.choose m * (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])

Tactic:
congr 3
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
k m : ℕ
h_1 : m ∈ range (k + 1)
h h₁ : k.choose m * (k + 1) = k.choose m * (k + 1)
⊢ (k + 1).choose m * (k + 1 - m) = k.choose m * (k + 1)

Tactic:
rw [(choose_mul_succ_eq k m).symm]

Premises used: Nat.choose_mul_succ_eq, Eq.symm
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
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
zero₃ zero₄ : Eq (α := ℚ[X]) 0 0
⊢ (derivative : (a : ℚ[X]) → ℚ[X]) (bernoulli 0) = (↑0 : ℚ[X]) * bernoulli (HSub.hSub (α := ℕ) 0 1)

Tactic:
rw [Nat.cast_zero, zero_mul, bernoulli_zero, derivative_one]

Premises used: MulZeroClass.zero_mul, Polynomial.bernoulli_zero, Nat.cast_zero, Polynomial.derivative_one
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
k : ℕ
⊢ (derivative : (a : ℚ[X]) → ℚ[X]) (bernoulli (k + 1)) = (↑(k + 1) : ℚ[X]) * bernoulli (k + 1 - 1)

Tactic:
mod_cast derivative_bernoulli_add_one k

Premises used: Polynomial.derivative, HMul.hMul, congrArg, Polynomial.bernoulli, Nat.cast_add._simp_1, cast, Nat.cast, HAdd.hAdd, Polynomial.derivative_bernoulli_add_one, congrFun', OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, DFunLike.coe, Nat.pred, Eq.trans
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
k : ℕ
⊢ (derivative : (a : ℚ[X]) → ℚ[X]) (bernoulli (k + 1)) = (↑(k + 1) : ℚ[X]) * bernoulli (k + 1 - 1)

Tactic:
exact mod_cast derivative_bernoulli_add_one k

Premises used: Polynomial.derivative_bernoulli_add_one
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
k : ℕ
zero : (derivative : (a : ℚ[X]) → ℚ[X]) (bernoulli 0) = (↑0 : ℚ[X]) * bernoulli (HSub.hSub (α := ℕ) 0 1)
succ : ∀ (k : ℕ), (derivative : (a : ℚ[X]) → ℚ[X]) (bernoulli (k + 1)) = (↑(k + 1) : ℚ[X]) * bernoulli (k + 1 - 1)
⊢ (derivative : (a : ℚ[X]) → ℚ[X]) (bernoulli k) = (↑k : ℚ[X]) * bernoulli (k - 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

Premises used: MulZeroClass.zero_mul, Polynomial.bernoulli_zero, Polynomial.derivative_bernoulli_add_one, Nat.zero, Nat.cast_zero, Nat.succ, Polynomial.derivative_one
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n : ℕ
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])
⊢ Eq (α := ℚ[X]) (∑ k ∈ range (n + 1), HSMul.hSMul (α := ℚ) (↑((n + 1).choose k) : ℚ) (bernoulli k) : ℚ[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]

Premises used: Finset.sum_Ico_Ico_comm, Finset.sum_Ico_eq_sum_range, Polynomial.bernoulli_def, Finset.smul_sum, Finset.range_eq_Ico
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n : ℕ
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)
⊢ 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 only [add_tsub_cancel_left, zero_add, map_add]

Premises used: add_tsub_cancel_left, map_add, zero_add
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n : ℕ
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)
⊢ ∑ 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_rw [smul_monomial, mul_comm (_root_.bernoulli _) _, smul_eq_mul, ← mul_assoc]

Premises used: Polynomial.smul_monomial, bernoulli, mul_assoc, mul_comm, smul_eq_mul
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n : ℕ
h : range (n + 1 - 0) = range (n + 1 - 0)
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) : ℚ)))
| ∑ 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)

Tactic:
apply_congr
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n : ℕ
⊢ range (n + 1 - 0) = range (n + 1 - 0)

Tactic:
· skip
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n x : ℕ
h_1 : x ∈ range (n + 1 - 0)
h : range (n + 1 - x) = range (n + 1 - x)
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) : ℚ))
| ∑ 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)

Tactic:
apply_congr
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n x : ℕ
h : x ∈ range (n + 1 - 0)
⊢ range (n + 1 - x) = range (n + 1 - x)

Tactic:
· skip
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n x : ℕ
h : x ∈ range (n + 1 - 0)
x_1 : ℕ
h_1 : x_1 ∈ range (n + 1 - x)
a :
  HSMul.hSMul (β := ℚ[X]) ((↑((n + 1 - x).choose x_1) : ℚ) * _root_.bernoulli x_1)
    ((monomial x : (a : ℚ) → ℚ[X]) (↑((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) : ℚ))

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]

Premises used: Nat.choose_mul, Polynomial.smul_monomial, mul_assoc, Nat.le_add_right, add_tsub_cancel_left, Nat.cast_mul, mul_comm, smul_eq_mul
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
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) : ℚ))
a₇ :
  HSMul.hSMul (β := ℚ[X]) ((↑((n + 1 - x).choose x_1) : ℚ) * _root_.bernoulli x_1)
    ((monomial x : (a : ℚ) → ℚ[X]) (↑((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) : ℚ))

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]

Premises used: Nat.choose_mul, Polynomial.smul_monomial, mul_assoc, Nat.le_add_right, add_tsub_cancel_left, Nat.cast_mul, mul_comm, smul_eq_mul
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n x : ℕ
h_1 : x ∈ range (n + 1 - 0)
h : range (n + 1 - x) = range (n + 1 - x)
a 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) : ℚ))
| ∑ 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)

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]

Premises used: Nat.choose_mul, Polynomial.smul_monomial, mul_assoc, Nat.le_add_right, add_tsub_cancel_left, Nat.cast_mul, mul_comm, smul_eq_mul
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n x : ℕ
h : x ∈ range (n + 1 - 0)
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) : ℚ))
⊢ 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:
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]

Premises used: Nat.choose_mul, Polynomial.smul_monomial, mul_assoc, Nat.le_add_right, add_tsub_cancel_left, Nat.cast_mul, mul_comm, smul_eq_mul
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
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)
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) : ℚ))
⊢ 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:
· 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]

Premises used: Nat.choose_mul, Polynomial.smul_monomial, mul_assoc, Nat.le_add_right, add_tsub_cancel_left, Nat.cast_mul, mul_comm, smul_eq_mul
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n : ℕ
h : range (n + 1 - 0) = range (n + 1 - 0)
a 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) : ℚ)))
| ∑ 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)

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]

Premises used: Nat.choose_mul, Polynomial.smul_monomial, mul_assoc, Nat.le_add_right, add_tsub_cancel_left, Nat.cast_mul, mul_comm, smul_eq_mul