awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n : ℕ
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)
⊢ ∑ 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:
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]

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 : ℕ
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)
⊢ ∑ 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:
simp_rw [← sum_smul, Nat.sub_zero]

Premises used: Finset.sum_smul, Nat.sub_zero
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n : ℕ
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)
⊢ ∑ 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:
rw [sum_range_succ_comm]

Premises used: Finset.sum_range_succ_comm
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n : ℕ
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
⊢ 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:
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]

Premises used: Nat.choose_succ_self_right, add_tsub_cancel_left, map_add, bernoulli_zero, zero_add, one_smul, Finset.sum_singleton, Nat.cast_add, add_eq_left, Finset.range_one, mul_one, Nat.cast_one
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
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

Tactic:
sum_eq_zero ?_

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n : ℕ
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
⊢ 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:
refine sum_eq_zero ?_

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n x : ℕ
hx : x ∈ range n
⊢ n + 1 - x ≠ 1

Tactic:
grind
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n x : ℕ
hx : x ∈ range n
⊢ n + 1 - x ≠ 1

Tactic:
have hx1 : n + 1 - x ≠ 1 := by grind
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n x : ℕ
hx : x ∈ range n
hx1 : n + 1 - x ≠ 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) : ℚ)) =
    0

Tactic:
simp [_root_.sum_bernoulli, hx1]

Premises used: sum_bernoulli
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
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])
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))
simp_rw₄ : HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 • bernoulli n = HSMul.hSMul (α := ℚ) (↑((n + 1).choose n) : ℚ) (bernoulli n)
simp_rw₅ : HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 • bernoulli n = HSMul.hSMul (α := ℚ) (↑(n + 1) : ℚ) (bernoulli n)
⊢ (n + 1) • bernoulli n = (n + 1) • HPow.hPow (α := ℚ[X]) X n - ∑ k ∈ range n, (n + 1).choose k • bernoulli k

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]

Premises used: Nat.cast_succ, Polynomial.sum_bernoulli, Rat, Nat.choose_succ_self_right, Nat.cast_smul_eq_nsmul, Finset.sum_range_succ_sub_sum, Polynomial.smul_X_eq_monomial
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n p : ℕ
rw :
  ∑ i ∈ range (p + 1), _root_.bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) =
    ∑ i ∈ range (p.succ + 1),
        eval (↑n : ℚ) ((monomial i : (a : ℚ) → ℚ[X]) (_root_.bernoulli (p.succ - i) * (↑(p.succ.choose i) : ℚ))) -
      _root_.bernoulli p.succ
rw₁ : HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 ≠ 0
⊢ HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 * ∑ k ∈ range n, HPow.hPow (α := ℚ) (↑k : ℚ) p =
    eval (↑n : ℚ) (bernoulli p.succ) - _root_.bernoulli p.succ

Tactic:
rw [sum_range_pow, bernoulli_def, eval_finsetSum, ← sum_div, mul_div_cancel₀ _ _]

Premises used: Polynomial.eval_finsetSum, mul_div_cancel₀, Finset.sum_div, Polynomial.bernoulli_def, sum_range_pow
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n p : ℕ
simp_rw :
  ∑ i ∈ range (p + 1), _root_.bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) =
    ∑ x ∈ range (p.succ + 1), _root_.bernoulli (p.succ - x) * (↑(p.succ.choose x) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) x -
      _root_.bernoulli p.succ
⊢ ∑ i ∈ range (p + 1), _root_.bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) =
    ∑ i ∈ range (p.succ + 1),
        eval (↑n : ℚ) ((monomial i : (a : ℚ) → ℚ[X]) (_root_.bernoulli (p.succ - i) * (↑(p.succ.choose i) : ℚ))) -
      _root_.bernoulli p.succ

Tactic:
simp_rw [eval_monomial]

Premises used: Polynomial.eval_monomial
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n p : ℕ
symm :
  ∑ x ∈ range (p.succ + 1), _root_.bernoulli (p.succ - x) * (↑(p.succ.choose x) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) x -
      _root_.bernoulli p.succ =
    ∑ i ∈ range (p + 1), _root_.bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i)
⊢ ∑ i ∈ range (p + 1), _root_.bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) =
    ∑ x ∈ range (p.succ + 1), _root_.bernoulli (p.succ - x) * (↑(p.succ.choose x) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) x -
      _root_.bernoulli p.succ

Tactic:
symm
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n p : ℕ
rw :
  ∑ x ∈ range (p + 1),
          _root_.bernoulli (p.succ - (p + 1 - x)) * (↑(p.succ.choose (p + 1 - x)) : ℚ) *
            HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - x) +
        _root_.bernoulli (p.succ - (p + 1 - (p + 1))) * (↑(p.succ.choose (p + 1 - (p + 1))) : ℚ) *
          HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - (p + 1)) -
      _root_.bernoulli p.succ =
    ∑ i ∈ range (p + 1), _root_.bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i)
⊢ ∑ x ∈ range (p.succ + 1), _root_.bernoulli (p.succ - x) * (↑(p.succ.choose x) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) x -
      _root_.bernoulli p.succ =
    ∑ i ∈ range (p + 1), _root_.bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i)

Tactic:
rw [← sum_flip _, sum_range_succ]

Premises used: Finset.sum_flip, Finset.sum_range_succ
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n p : ℕ
simp :
  Eq (α := ℚ)
    (∑ x ∈ range (p + 1),
      _root_.bernoulli (p.succ - (p + 1 - x)) * (↑(p.succ.choose (p + 1 - x)) : ℚ) *
        HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - x))
    (∑ i ∈ range (p + 1), _root_.bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i))
⊢ ∑ x ∈ range (p + 1),
          _root_.bernoulli (p.succ - (p + 1 - x)) * (↑(p.succ.choose (p + 1 - x)) : ℚ) *
            HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - x) +
        _root_.bernoulli (p.succ - (p + 1 - (p + 1))) * (↑(p.succ.choose (p + 1 - (p + 1))) : ℚ) *
          HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - (p + 1)) -
      _root_.bernoulli p.succ =
    ∑ i ∈ range (p + 1), _root_.bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i)

Tactic:
simp only [tsub_self, tsub_zero, choose_zero_right, cast_one, mul_one, _root_.pow_zero,
      add_tsub_cancel_right]

Premises used: tsub_self, pow_zero, tsub_zero, add_tsub_cancel_right, mul_one, Nat.cast_one, Nat.choose_zero_right
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n p : ℕ
apply :
  ∀ (x : ℕ) (hx : x ∈ range (p + 1)),
    _root_.bernoulli (p.succ - (p + 1 - x)) * (↑(p.succ.choose (p + 1 - x)) : ℚ) *
        HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - x) =
      _root_.bernoulli x * (↑((p + 1).choose x) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - x)
⊢ Eq (α := ℚ)
    (∑ x ∈ range (p + 1),
      _root_.bernoulli (p.succ - (p + 1 - x)) * (↑(p.succ.choose (p + 1 - x)) : ℚ) *
        HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - x))
    (∑ i ∈ range (p + 1), _root_.bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i))

Tactic:
apply sum_congr rfl fun x hx => _

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n p x : ℕ
hx : x ∈ range (p + 1)
apply : _root_.bernoulli (p.succ - (p + 1 - x)) = _root_.bernoulli x
apply₁ : Eq (α := ℚ) (↑(p.succ.choose (p + 1 - x)) : ℚ) (↑((p + 1).choose x) : ℚ)
⊢ _root_.bernoulli (p.succ - (p + 1 - x)) * (↑(p.succ.choose (p + 1 - x)) : ℚ) *
      HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - x) =
    _root_.bernoulli x * (↑((p + 1).choose x) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - x)

Tactic:
apply congr_arg₂ _ (congr_arg₂ _ _ _) rfl

Premises used: rfl, congr_arg₂
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n p x : ℕ
hx : x ∈ range (p + 1)
rw rw₁ : _root_.bernoulli x = _root_.bernoulli x
⊢ _root_.bernoulli (p.succ - (p + 1 - x)) = _root_.bernoulli x

Tactic:
rw [Nat.sub_sub_self (mem_range_le hx)]

Premises used: Nat.sub_sub_self, Finset.mem_range_le
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n p x : ℕ
hx : x ∈ range (p + 1)
rw rw₁ : Eq (α := ℚ) (↑(p.succ.choose (p + 1 - x)) : ℚ) (↑((p + 1).choose (p + 1 - x)) : ℚ)
⊢ Eq (α := ℚ) (↑(p.succ.choose (p + 1 - x)) : ℚ) (↑((p + 1).choose x) : ℚ)

Tactic:
rw [← choose_symm (mem_range_le hx)]

Premises used: Nat.choose_symm, Finset.mem_range_le
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n p : ℕ
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : ¬False
⊢ HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 ≠ 0

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n p : ℕ
h :
  eval (↑n : ℚ) (bernoulli p.succ) - _root_.bernoulli p.succ =
    HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 * ∑ k ∈ range n, HPow.hPow (α := ℚ) (↑k : ℚ) p
⊢ eval (↑n : ℚ) (bernoulli p.succ) =
    _root_.bernoulli p.succ + HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 * ∑ k ∈ range n, HPow.hPow (α := ℚ) (↑k : ℚ) p

Tactic:
apply eq_add_of_sub_eq'

Premises used: eq_add_of_sub_eq'
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n p : ℕ
h h₁ :
  eval (↑n : ℚ) (bernoulli p.succ) - _root_.bernoulli p.succ =
    eval (↑n : ℚ) (bernoulli p.succ) - _root_.bernoulli p.succ
⊢ eval (↑n : ℚ) (bernoulli p.succ) - _root_.bernoulli p.succ =
    HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 * ∑ k ∈ range n, HPow.hPow (α := ℚ) (↑k : ℚ) p

Tactic:
rw [sum_range_pow_eq_bernoulli_sub]

Premises used: Polynomial.sum_range_pow_eq_bernoulli_sub
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n : ℕ
⊢ (bernoulli n).comp (HAdd.hAdd (α := ℚ[X]) 1 X) = bernoulli n + n • HPow.hPow (α := ℚ[X]) X (n - 1)

Tactic:
Nat.strong_induction_on n fun d hd => ?_

Premises used: Nat.strong_induction_on
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n : ℕ
refine :
  ∀ (d : ℕ)
    (hd : ∀ m < d, (bernoulli m).comp (HAdd.hAdd (α := ℚ[X]) 1 X) = bernoulli m + m • HPow.hPow (α := ℚ[X]) X (m - 1)),
    (bernoulli d).comp (HAdd.hAdd (α := ℚ[X]) 1 X) = bernoulli d + d • HPow.hPow (α := ℚ[X]) X (d - 1)
⊢ (bernoulli n).comp (HAdd.hAdd (α := ℚ[X]) 1 X) = bernoulli n + n • HPow.hPow (α := ℚ[X]) X (n - 1)

Tactic:
refine Nat.strong_induction_on n fun d hd => ?_
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n : ℕ
hd : ∀ m < 0, (bernoulli m).comp (HAdd.hAdd (α := ℚ[X]) 1 X) = bernoulli m + m • HPow.hPow (α := ℚ[X]) X (m - 1)
⊢ (bernoulli 0).comp (HAdd.hAdd (α := ℚ[X]) 1 X) =
    bernoulli 0 + HSMul.hSMul (α := ℕ) 0 (HPow.hPow (α := ℚ[X]) X (HSub.hSub (α := ℕ) 0 1))

Tactic:
simp
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (HAdd.hAdd (α := ℚ[X]) 1 X) = bernoulli m + m • HPow.hPow (α := ℚ[X]) X (m - 1)
⊢ d + 2 ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (HAdd.hAdd (α := ℚ[X]) 1 X) = bernoulli m + m • HPow.hPow (α := ℚ[X]) X (m - 1)
succ :
  ((d + 2) • bernoulli (d + 1)).comp (HAdd.hAdd (α := ℚ[X]) 1 X) =
    (d + 2) • bernoulli (d + 1) + (d + 2) • (d + 1) • HPow.hPow (α := ℚ[X]) X (d + 1 - 1)
⊢ (bernoulli (d + 1)).comp (HAdd.hAdd (α := ℚ[X]) 1 X) =
    bernoulli (d + 1) + (d + 1) • HPow.hPow (α := ℚ[X]) X (d + 1 - 1)

Tactic:
rw [← smul_right_inj (show d + 2 ≠ 0 by positivity), ← smul_comp, smul_add]

Premises used: smul_add, smul_right_inj, Polynomial.smul_comp
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (HAdd.hAdd (α := ℚ[X]) 1 X) = bernoulli m + m • HPow.hPow (α := ℚ[X]) X (m - 1)
succ :
  ((d + 2) • HPow.hPow (α := ℚ[X]) X (d + 1)).comp (HAdd.hAdd (α := ℚ[X]) 1 X) -
      ∑ i ∈ range (d + 1), ((d + 2).choose i • bernoulli i).comp (HAdd.hAdd (α := ℚ[X]) 1 X) =
    (d + 2) • HPow.hPow (α := ℚ[X]) X (d + 1) - ∑ x ∈ range (d + 1), (d + 2).choose x • bernoulli x +
      ((d + 2) * (d + 1)) • HPow.hPow (α := ℚ[X]) X (d + 1 - 1)
⊢ ((d + 2) • bernoulli (d + 1)).comp (HAdd.hAdd (α := ℚ[X]) 1 X) =
    (d + 2) • bernoulli (d + 1) + (d + 2) • (d + 1) • HPow.hPow (α := ℚ[X]) X (d + 1 - 1)

Tactic:
simp only [bernoulli_eq_sub_sum, sub_comp, sum_comp, add_assoc, one_add_one_eq_two, smul_smul]

Premises used: add_assoc, smul_smul, Polynomial.sum_comp, Polynomial.bernoulli_eq_sub_sum, one_add_one_eq_two, Polynomial.sub_comp
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (HAdd.hAdd (α := ℚ[X]) 1 X) = bernoulli m + m • HPow.hPow (α := ℚ[X]) X (m - 1)
a : ((d + 2) • HPow.hPow (α := ℚ[X]) X (d + 1)).comp (HAdd.hAdd (α := ℚ[X]) 1 X)
a₁ : ∑ i ∈ range (d + 1), ((d + 2).choose i • bernoulli i).comp (HAdd.hAdd (α := ℚ[X]) 1 X)
| ((d + 2) • HPow.hPow (α := ℚ[X]) X (d + 1)).comp (HAdd.hAdd (α := ℚ[X]) 1 X) -
    ∑ i ∈ range (d + 1), ((d + 2).choose i • bernoulli i).comp (HAdd.hAdd (α := ℚ[X]) 1 X)

Tactic:
congr
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (HAdd.hAdd (α := ℚ[X]) 1 X) = bernoulli m + m • HPow.hPow (α := ℚ[X]) X (m - 1)
| ((d + 2) • HPow.hPow (α := ℚ[X]) X (d + 1)).comp (HAdd.hAdd (α := ℚ[X]) 1 X)

Tactic:
· skip
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (HAdd.hAdd (α := ℚ[X]) 1 X) = bernoulli m + m • HPow.hPow (α := ℚ[X]) X (m - 1)
a : range (d + 1) = range (d + 1)
a₁ :
  ∀ x ∈ range (d + 1),
    ((d + 2).choose x • bernoulli x).comp (HAdd.hAdd (α := ℚ[X]) 1 X) =
      (d + 2).choose x • (bernoulli x + x • HPow.hPow (α := ℚ[X]) X (x - 1))
| ∑ i ∈ range (d + 1), ((d + 2).choose i • bernoulli i).comp (HAdd.hAdd (α := ℚ[X]) 1 X)

Tactic:
apply_congr
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (HAdd.hAdd (α := ℚ[X]) 1 X) = bernoulli m + m • HPow.hPow (α := ℚ[X]) X (m - 1)
⊢ range (d + 1) = range (d + 1)

Tactic:
· skip
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (HAdd.hAdd (α := ℚ[X]) 1 X) = bernoulli m + m • HPow.hPow (α := ℚ[X]) X (m - 1)
x : ℕ
h : x ∈ range (d + 1)
⊢ x ∈ range (d + 1)

Tactic:
assumption
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (HAdd.hAdd (α := ℚ[X]) 1 X) = bernoulli m + m • HPow.hPow (α := ℚ[X]) X (m - 1)
x : ℕ
h : x ∈ range (d + 1)
a : (d + 2).choose x • (bernoulli x + x • HPow.hPow (α := ℚ[X]) X (x - 1))
⊢ ((d + 2).choose x • bernoulli x).comp (HAdd.hAdd (α := ℚ[X]) 1 X) =
    (d + 2).choose x • (bernoulli x + x • HPow.hPow (α := ℚ[X]) X (x - 1))

Tactic:
rw [smul_comp, hd _ (mem_range.1 (by assumption))]

Premises used: Finset.mem_range, Iff.mp, Polynomial.smul_comp
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (HAdd.hAdd (α := ℚ[X]) 1 X) = bernoulli m + m • HPow.hPow (α := ℚ[X]) X (m - 1)
x : ℕ
h : x ∈ range (d + 1)
a : (d + 2).choose x • (bernoulli x).comp (HAdd.hAdd (α := ℚ[X]) 1 X)
a₁ : (d + 2).choose x • (bernoulli x + x • HPow.hPow (α := ℚ[X]) X (x - 1))
⊢ ((d + 2).choose x • bernoulli x).comp (HAdd.hAdd (α := ℚ[X]) 1 X) =
    (d + 2).choose x • (bernoulli x + x • HPow.hPow (α := ℚ[X]) X (x - 1))

Tactic:
· rw [smul_comp, hd _ (mem_range.1 (by assumption))]

Premises used: Finset.mem_range, Iff.mp, Polynomial.smul_comp
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (HAdd.hAdd (α := ℚ[X]) 1 X) = bernoulli m + m • HPow.hPow (α := ℚ[X]) X (m - 1)
a : range (d + 1) = range (d + 1)
a₁ a₂ :
  ∀ x ∈ range (d + 1),
    ((d + 2).choose x • bernoulli x).comp (HAdd.hAdd (α := ℚ[X]) 1 X) =
      (d + 2).choose x • (bernoulli x + x • HPow.hPow (α := ℚ[X]) X (x - 1))
| ∑ i ∈ range (d + 1), ((d + 2).choose i • bernoulli i).comp (HAdd.hAdd (α := ℚ[X]) 1 X)

Tactic:
apply_congr
      · skip
      · rw [smul_comp, hd _ (mem_range.1 (by assumption))]

Premises used: Finset.mem_range, Iff.mp, Polynomial.smul_comp
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (HAdd.hAdd (α := ℚ[X]) 1 X) = bernoulli m + m • HPow.hPow (α := ℚ[X]) X (m - 1)
a : range (d + 1) = range (d + 1)
a₁ a₂ :
  ∀ x ∈ range (d + 1),
    ((d + 2).choose x • bernoulli x).comp (HAdd.hAdd (α := ℚ[X]) 1 X) =
      (d + 2).choose x • (bernoulli x + x • HPow.hPow (α := ℚ[X]) X (x - 1))
| ∑ i ∈ range (d + 1), ((d + 2).choose i • bernoulli i).comp (HAdd.hAdd (α := ℚ[X]) 1 X)

Tactic:
· apply_congr
      · skip
      · rw [smul_comp, hd _ (mem_range.1 (by assumption))]

Premises used: Finset.mem_range, Iff.mp, Polynomial.smul_comp
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (HAdd.hAdd (α := ℚ[X]) 1 X) = bernoulli m + m • HPow.hPow (α := ℚ[X]) X (m - 1)
a : ((d + 2) • HPow.hPow (α := ℚ[X]) X (d + 1)).comp (HAdd.hAdd (α := ℚ[X]) 1 X)
a₁ a₂ : ∑ i ∈ range (d + 1), ((d + 2).choose i • bernoulli i).comp (HAdd.hAdd (α := ℚ[X]) 1 X)
| ((d + 2) • HPow.hPow (α := ℚ[X]) X (d + 1)).comp (HAdd.hAdd (α := ℚ[X]) 1 X) -
    ∑ i ∈ range (d + 1), ((d + 2).choose i • bernoulli i).comp (HAdd.hAdd (α := ℚ[X]) 1 X)

Tactic:
congr
    · skip
    · apply_congr
      · skip
      · rw [smul_comp, hd _ (mem_range.1 (by assumption))]

Premises used: Finset.mem_range, Iff.mp, Polynomial.smul_comp
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (HAdd.hAdd (α := ℚ[X]) 1 X) = bernoulli m + m • HPow.hPow (α := ℚ[X]) X (m - 1)
succ :
  ((d + 2) • HPow.hPow (α := ℚ[X]) X (d + 1)).comp (HAdd.hAdd (α := ℚ[X]) 1 X) -
      ∑ x ∈ range (d + 1), (d + 2).choose x • (bernoulli x + x • HPow.hPow (α := ℚ[X]) X (x - 1)) =
    (d + 2) • HPow.hPow (α := ℚ[X]) X (d + 1) - ∑ x ∈ range (d + 1), (d + 2).choose x • bernoulli x +
      ((d + 2) * (d + 1)) • HPow.hPow (α := ℚ[X]) X (d + 1 - 1)
⊢ ((d + 2) • HPow.hPow (α := ℚ[X]) X (d + 1)).comp (HAdd.hAdd (α := ℚ[X]) 1 X) -
      ∑ i ∈ range (d + 1), ((d + 2).choose i • bernoulli i).comp (HAdd.hAdd (α := ℚ[X]) 1 X) =
    (d + 2) • HPow.hPow (α := ℚ[X]) X (d + 1) - ∑ x ∈ range (d + 1), (d + 2).choose x • bernoulli x +
      ((d + 2) * (d + 1)) • HPow.hPow (α := ℚ[X]) X (d + 1 - 1)

Tactic:
conv_lhs =>
    congr
    · skip
    · apply_congr
      · skip
      · rw [smul_comp, hd _ (mem_range.1 (by assumption))]

Premises used: Finset.mem_range, Iff.mp, Polynomial.smul_comp
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (HAdd.hAdd (α := ℚ[X]) 1 X) = bernoulli m + m • HPow.hPow (α := ℚ[X]) X (m - 1)
succ :
  ((d + 2) • HPow.hPow (α := ℚ[X]) X (d + 1)).comp (HAdd.hAdd (α := ℚ[X]) 1 X) -
        ∑ x ∈ range (d + 1), (d + 2).choose x • x • HPow.hPow (α := ℚ[X]) X (x - 1) -
      ∑ x ∈ range (d + 1), (d + 2).choose x • bernoulli x =
    (d + 2) • HPow.hPow (α := ℚ[X]) X (d + 1) + ((d + 2) * (d + 1)) • HPow.hPow (α := ℚ[X]) X (d + 1 - 1) -
      ∑ x ∈ range (d + 1), (d + 2).choose x • bernoulli x
⊢ ((d + 2) • HPow.hPow (α := ℚ[X]) X (d + 1)).comp (HAdd.hAdd (α := ℚ[X]) 1 X) -
      ∑ x ∈ range (d + 1), (d + 2).choose x • (bernoulli x + x • HPow.hPow (α := ℚ[X]) X (x - 1)) =
    (d + 2) • HPow.hPow (α := ℚ[X]) X (d + 1) - ∑ x ∈ range (d + 1), (d + 2).choose x • bernoulli x +
      ((d + 2) * (d + 1)) • HPow.hPow (α := ℚ[X]) X (d + 1 - 1)

Tactic:
simp_rw [smul_add, sum_add_distrib, sub_add, sub_add_eq_sub_sub_swap, sub_sub_eq_add_sub]

Premises used: sub_add, Finset.sum_add_distrib, sub_sub_eq_add_sub, smul_add, sub_add_eq_sub_sub_swap