awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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])
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))
⊢ (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 = HSMul.hSMul (α := ℚ) (↑((n + 1).choose n) : ℚ) (bernoulli n)
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])
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)
⊢ (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 = HSMul.hSMul (α := ℚ) (↑(n + 1) : ℚ) (bernoulli n)
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 p : ℕ
⊢ HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 * ∑ k ∈ range n, HPow.hPow (α := ℚ) (↑k : ℚ) p =
    eval (↑n : ℚ) (bernoulli p.succ) - _root_.bernoulli p.succ
have 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
Tactic: rw [sum_range_pow, bernoulli_def, eval_finsetSum, ← sum_div, mul_div_cancel₀ _ _]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
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
⊢ HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 * ∑ k ∈ range n, HPow.hPow (α := ℚ) (↑k : ℚ) p =
    eval (↑n : ℚ) (bernoulli p.succ) - _root_.bernoulli p.succ
have rw₁ : HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 ≠ 0
Tactic: rw [sum_range_pow, bernoulli_def, eval_finsetSum, ← sum_div, mul_div_cancel₀ _ _]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n p : ℕ
⊢ ∑ 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
have 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
Tactic: simp_rw [eval_monomial]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n p : ℕ
⊢ ∑ 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
have 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)
Tactic: symm
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n p : ℕ
⊢ ∑ 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)
have 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)
Tactic: rw [← sum_flip _, sum_range_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n p : ℕ
⊢ ∑ 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)
have 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))
Tactic: simp only [tsub_self, tsub_zero, choose_zero_right, cast_one, mul_one, _root_.pow_zero,
      add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n p : ℕ
⊢ 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))
have 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)
Tactic: apply sum_congr rfl fun x hx => _
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n p 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)
have apply : _root_.bernoulli (p.succ - (p + 1 - x)) = _root_.bernoulli x
Tactic: apply congr_arg₂ _ (congr_arg₂ _ _ _) rfl
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n p x : ℕ
hx : x ∈ range (p + 1)
apply : _root_.bernoulli (p.succ - (p + 1 - x)) = _root_.bernoulli 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)
have apply₁ : Eq (α := ℚ) (↑(p.succ.choose (p + 1 - x)) : ℚ) (↑((p + 1).choose x) : ℚ)
Tactic: apply congr_arg₂ _ (congr_arg₂ _ _ _) rfl
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n p x : ℕ
hx : x ∈ range (p + 1)
⊢ _root_.bernoulli (p.succ - (p + 1 - x)) = _root_.bernoulli x
have rw : _root_.bernoulli x = _root_.bernoulli x
Tactic: rw [Nat.sub_sub_self (mem_range_le hx)]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n p x : ℕ
hx : x ∈ range (p + 1)
⊢ Eq (α := ℚ) (↑(p.succ.choose (p + 1 - x)) : ℚ) (↑((p + 1).choose x) : ℚ)
have rw : Eq (α := ℚ) (↑(p.succ.choose (p + 1 - x)) : ℚ) (↑((p + 1).choose (p + 1 - x)) : ℚ)
Tactic: rw [← choose_symm (mem_range_le hx)]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n p : ℕ
⊢ HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 ≠ 0
have norm_cast : ¬False
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n p : ℕ
⊢ eval (↑n : ℚ) (bernoulli p.succ) =
    _root_.bernoulli p.succ + HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 * ∑ k ∈ range n, HPow.hPow (α := ℚ) (↑k : ℚ) p
have h : 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'
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n p : ℕ
⊢ eval (↑n : ℚ) (bernoulli p.succ) - _root_.bernoulli p.succ =
    HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 * ∑ k ∈ range n, HPow.hPow (α := ℚ) (↑k : ℚ) p
have h : eval (↑n : ℚ) (bernoulli p.succ) - _root_.bernoulli p.succ = eval (↑n : ℚ) (bernoulli p.succ) - _root_.bernoulli p.succ
Tactic: rw [sum_range_pow_eq_bernoulli_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n : ℕ
⊢ (bernoulli n).comp (HAdd.hAdd (α := ℚ[X]) 1 X) = bernoulli n + n • HPow.hPow (α := ℚ[X]) X (n - 1)
have 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)
Tactic: refine Nat.strong_induction_on n fun d hd => ?_
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (HAdd.hAdd (α := ℚ[X]) 1 X) = bernoulli m + m • HPow.hPow (α := ℚ[X]) X (m - 1)
⊢ (bernoulli (d + 1)).comp (HAdd.hAdd (α := ℚ[X]) 1 X) =
    bernoulli (d + 1) + (d + 1) • HPow.hPow (α := ℚ[X]) X (d + 1 - 1)
have 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)
Tactic: rw [← smul_right_inj (show d + 2 ≠ 0 by positivity), ← smul_comp, smul_add]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
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) • 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)
have 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)
Tactic: simp only [bernoulli_eq_sub_sum, sub_comp, sum_comp, add_assoc, one_add_one_eq_two, smul_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
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) -
    ∑ i ∈ range (d + 1), ((d + 2).choose i • bernoulli i).comp (HAdd.hAdd (α := ℚ[X]) 1 X)
have a : ((d + 2) • HPow.hPow (α := ℚ[X]) X (d + 1)).comp (HAdd.hAdd (α := ℚ[X]) 1 X)
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
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)
| ((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)
have a₁ : ∑ i ∈ range (d + 1), ((d + 2).choose i • bernoulli i).comp (HAdd.hAdd (α := ℚ[X]) 1 X)
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (HAdd.hAdd (α := ℚ[X]) 1 X) = bernoulli m + m • HPow.hPow (α := ℚ[X]) X (m - 1)
| ∑ i ∈ range (d + 1), ((d + 2).choose i • bernoulli i).comp (HAdd.hAdd (α := ℚ[X]) 1 X)
have a : range (d + 1) = range (d + 1)
Tactic: apply_congr
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
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)
| ∑ i ∈ range (d + 1), ((d + 2).choose i • bernoulli i).comp (HAdd.hAdd (α := ℚ[X]) 1 X)
have 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))
Tactic: apply_congr
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
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)
⊢ ((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))
have a : (d + 2).choose x • (bernoulli x + x • HPow.hPow (α := ℚ[X]) X (x - 1))
Tactic: rw [smul_comp, hd _ (mem_range.1 (by assumption))]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
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)
⊢ ((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))
have a : (d + 2).choose x • (bernoulli x).comp (HAdd.hAdd (α := ℚ[X]) 1 X)
Tactic: · rw [smul_comp, hd _ (mem_range.1 (by assumption))]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
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)
⊢ ((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))
have a₁ : (d + 2).choose x • (bernoulli x + x • HPow.hPow (α := ℚ[X]) X (x - 1))
Tactic: · rw [smul_comp, hd _ (mem_range.1 (by assumption))]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (HAdd.hAdd (α := ℚ[X]) 1 X) = bernoulli m + m • HPow.hPow (α := ℚ[X]) X (m - 1)
| ∑ i ∈ range (d + 1), ((d + 2).choose i • bernoulli i).comp (HAdd.hAdd (α := ℚ[X]) 1 X)
have a : range (d + 1) = range (d + 1)
Tactic: apply_congr
      · skip
      · rw [smul_comp, hd _ (mem_range.1 (by assumption))]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
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)
| ∑ i ∈ range (d + 1), ((d + 2).choose i • bernoulli i).comp (HAdd.hAdd (α := ℚ[X]) 1 X)
have 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))
Tactic: apply_congr
      · skip
      · rw [smul_comp, hd _ (mem_range.1 (by assumption))]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (HAdd.hAdd (α := ℚ[X]) 1 X) = bernoulli m + m • HPow.hPow (α := ℚ[X]) X (m - 1)
| ∑ i ∈ range (d + 1), ((d + 2).choose i • bernoulli i).comp (HAdd.hAdd (α := ℚ[X]) 1 X)
have a : range (d + 1) = range (d + 1)
Tactic: · apply_congr
      · skip
      · rw [smul_comp, hd _ (mem_range.1 (by assumption))]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
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)
| ∑ i ∈ range (d + 1), ((d + 2).choose i • bernoulli i).comp (HAdd.hAdd (α := ℚ[X]) 1 X)
have 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))
Tactic: · apply_congr
      · skip
      · rw [smul_comp, hd _ (mem_range.1 (by assumption))]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
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) -
    ∑ i ∈ range (d + 1), ((d + 2).choose i • bernoulli i).comp (HAdd.hAdd (α := ℚ[X]) 1 X)
have a : ((d + 2) • HPow.hPow (α := ℚ[X]) X (d + 1)).comp (HAdd.hAdd (α := ℚ[X]) 1 X)
Tactic: congr
    · skip
    · apply_congr
      · skip
      · rw [smul_comp, hd _ (mem_range.1 (by assumption))]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
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)
| ((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)
have a₁ : ∑ 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))]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
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) -
      ∑ 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)
have 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)
Tactic: conv_lhs =>
    congr
    · skip
    · apply_congr
      · skip
      · rw [smul_comp, hd _ (mem_range.1 (by assumption))]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
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) -
      ∑ 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)
have 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
Tactic: simp_rw [smul_add, sum_add_distrib, sub_add, sub_add_eq_sub_sub_swap, sub_sub_eq_add_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
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) -
        ∑ 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
have 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) =
  (d + 2) • HPow.hPow (α := ℚ[X]) X (d + 1) + ((d + 2) * (d + 1)) • HPow.hPow (α := ℚ[X]) X (d + 1 - 1)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
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) -
      ∑ x ∈ range (d + 1), (d + 2).choose x • x • HPow.hPow (α := ℚ[X]) X (x - 1) =
    (d + 2) • HPow.hPow (α := ℚ[X]) X (d + 1) + ((d + 2) * (d + 1)) • HPow.hPow (α := ℚ[X]) X (d + 1 - 1)
have succ : ((d + 2) • HPow.hPow (α := ℚ[X]) X (d + 1)).comp (HAdd.hAdd (α := ℚ[X]) 1 X) -
    (d + 2) • HPow.hPow (α := ℚ[X]) X (d + 1) =
  ∑ x ∈ range (d + 1), (d + 2).choose x • x • HPow.hPow (α := ℚ[X]) X (x - 1) +
    ((d + 2) * (d + 1)) • HPow.hPow (α := ℚ[X]) X (d + 1 - 1)
Tactic: rw [show ∀ a b c d : ℚ[X], a - b = c + d ↔ a - c = b + d by grind]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
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) -
      (d + 2) • HPow.hPow (α := ℚ[X]) X (d + 1) =
    HSMul.hSMul (β := ℚ[X]) (d + 2) (∑ i ∈ range (d + 1), (d + 1).choose i • HPow.hPow (α := ℚ[X]) X i)
have rw : (d + 2) • (HPow.hPow (α := ℚ[X]) X (d + 1)).comp (HAdd.hAdd (α := ℚ[X]) 1 X) -
    (d + 2) • HPow.hPow (α := ℚ[X]) X (d + 1) =
  HSMul.hSMul (β := ℚ[X]) (d + 2) (∑ i ∈ range (d + 1), (d + 1).choose i • HPow.hPow (α := ℚ[X]) X i)
Tactic: rw [smul_comp, ← smul_sub, X_pow_comp, one_add_X_pow_sub_X_pow]