awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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)
⊢ ((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) - 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]
-- 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)
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)
rw₁ :
  (d + 2) • ((HPow.hPow (α := ℚ[X]) X (d + 1)).comp (HAdd.hAdd (α := ℚ[X]) 1 X) - HPow.hPow (α := ℚ[X]) X (d + 1)) =
    HSMul.hSMul (β := ℚ[X]) (d + 2) (∑ i ∈ range (d + 1), (d + 1).choose i • HPow.hPow (α := ℚ[X]) X i)
⊢ ((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) • (HAdd.hAdd (α := ℚ[X]) 1 X ^ (d + 1) - 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]
-- 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)
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)
rw₁ :
  (d + 2) • ((HPow.hPow (α := ℚ[X]) X (d + 1)).comp (HAdd.hAdd (α := ℚ[X]) 1 X) - HPow.hPow (α := ℚ[X]) X (d + 1)) =
    HSMul.hSMul (β := ℚ[X]) (d + 2) (∑ i ∈ range (d + 1), (d + 1).choose i • HPow.hPow (α := ℚ[X]) X i)
rw₂ :
  (d + 2) • (HAdd.hAdd (α := ℚ[X]) 1 X ^ (d + 1) - HPow.hPow (α := ℚ[X]) X (d + 1)) =
    HSMul.hSMul (β := ℚ[X]) (d + 2) (∑ i ∈ range (d + 1), (d + 1).choose i • HPow.hPow (α := ℚ[X]) X i)
⊢ ((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₃ : HSMul.hSMul (β := ℚ[X]) (d + 2) (∑ i ∈ range (d + 1), (d + 1).choose i • HPow.hPow (α := ℚ[X]) X i) =
  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]
-- 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)
⊢ HSMul.hSMul (β := ℚ[X]) (d + 2) (∑ i ∈ range (d + 1), (d + 1).choose i • HPow.hPow (α := ℚ[X]) X i) =
    ∑ i ∈ range (d + 1), ((d + 2).choose (i + 1) * (i + 1)) • HPow.hPow (α := ℚ[X]) X i
have simp_rw : Eq (α := ℚ[X]) (∑ x ∈ range (d + 1), (d + 2) • (d + 1).choose x • HPow.hPow (α := ℚ[X]) X x)
  (∑ i ∈ range (d + 1), ((d + 2).choose (i + 1) * (i + 1)) • HPow.hPow (α := ℚ[X]) X i)
Tactic: simp_rw [smul_sum, smul_smul, ← add_one_mul_choose_eq (d + 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)
simp_rw :
  Eq (α := ℚ[X]) (∑ x ∈ range (d + 1), (d + 2) • (d + 1).choose x • HPow.hPow (α := ℚ[X]) X x)
    (∑ i ∈ range (d + 1), ((d + 2).choose (i + 1) * (i + 1)) • HPow.hPow (α := ℚ[X]) X i)
⊢ HSMul.hSMul (β := ℚ[X]) (d + 2) (∑ i ∈ range (d + 1), (d + 1).choose i • HPow.hPow (α := ℚ[X]) X i) =
    ∑ i ∈ range (d + 1), ((d + 2).choose (i + 1) * (i + 1)) • HPow.hPow (α := ℚ[X]) X i
have simp_rw₁ : Eq (α := ℚ[X]) (∑ x ∈ range (d + 1), ((d + 2) * (d + 1).choose x) • HPow.hPow (α := ℚ[X]) X x)
  (∑ i ∈ range (d + 1), ((d + 2).choose (i + 1) * (i + 1)) • HPow.hPow (α := ℚ[X]) X i)
Tactic: simp_rw [smul_sum, smul_smul, ← add_one_mul_choose_eq (d + 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)
⊢ ∑ i ∈ range (d + 1), ((d + 2).choose (i + 1) * (i + 1)) • HPow.hPow (α := ℚ[X]) X i =
    ∑ i ∈ range (d + 1), ((d + 2).choose i * i) • HPow.hPow (α := ℚ[X]) X (i - 1) +
      ((d + 2).choose (d + 1) * (d + 1)) • HPow.hPow (α := ℚ[X]) X (d + 1 - 1)
have rw : Eq (α := ℚ[X]) (∑ i ∈ range (d + 1), ((d + 2).choose (i + 1) * (i + 1)) • HPow.hPow (α := ℚ[X]) X i)
  (∑ x ∈ range (d + 1 + 1), ((d + 2).choose x * x) • HPow.hPow (α := ℚ[X]) X (x - 1))
Tactic: rw [← sum_range_succ _ (d + 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) -
      (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)
have calc : ((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: calc ((d + 2) • X ^ (d + 1)).comp (1 + X) - (d + 2) • X ^ (d + 1)
    _ = (d + 2) • ∑ i ∈ range (d + 1), (d + 1).choose i • X ^ i := by
      rw [smul_comp, ← smul_sub, X_pow_comp, one_add_X_pow_sub_X_pow]
    _ = ∑ i ∈ range (d + 1), ((d + 2).choose (i + 1) * (i + 1)) • X ^ i := by
      simp_rw [smul_sum, smul_smul, ← add_one_mul_choose_eq (d + 1)]
    _ = ∑ i ∈ range (d + 1), ((d + 2).choose i * i) • X ^ (i - 1) +
          (((d + 2).choose (d + 1)) * (d + 1)) • X ^ (d + 1 - 1) := by
      rw [← sum_range_succ _ (d + 1)]; simp [sum_range_succ']
    _ = ∑ i ∈ range (d + 1), (d + 2).choose i • i • X ^ (i - 1) +
          ((d + 2) * (d + 1)) • X ^ (d + 1 - 1) := by
      simp [choose_succ_self_right, add_assoc, mul_assoc]
-- 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)
calc :
  ((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)
⊢ ((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)
have calc₁ : HSMul.hSMul (β := ℚ[X]) (d + 2) (∑ i ∈ range (d + 1), (d + 1).choose i • HPow.hPow (α := ℚ[X]) X i) =
  ∑ i ∈ range (d + 1), ((d + 2).choose (i + 1) * (i + 1)) • HPow.hPow (α := ℚ[X]) X i
Tactic: calc ((d + 2) • X ^ (d + 1)).comp (1 + X) - (d + 2) • X ^ (d + 1)
    _ = (d + 2) • ∑ i ∈ range (d + 1), (d + 1).choose i • X ^ i := by
      rw [smul_comp, ← smul_sub, X_pow_comp, one_add_X_pow_sub_X_pow]
    _ = ∑ i ∈ range (d + 1), ((d + 2).choose (i + 1) * (i + 1)) • X ^ i := by
      simp_rw [smul_sum, smul_smul, ← add_one_mul_choose_eq (d + 1)]
    _ = ∑ i ∈ range (d + 1), ((d + 2).choose i * i) • X ^ (i - 1) +
          (((d + 2).choose (d + 1)) * (d + 1)) • X ^ (d + 1 - 1) := by
      rw [← sum_range_succ _ (d + 1)]; simp [sum_range_succ']
    _ = ∑ i ∈ range (d + 1), (d + 2).choose i • i • X ^ (i - 1) +
          ((d + 2) * (d + 1)) • X ^ (d + 1 - 1) := by
      simp [choose_succ_self_right, add_assoc, mul_assoc]
-- 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)
calc :
  ((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)
calc₁ :
  HSMul.hSMul (β := ℚ[X]) (d + 2) (∑ i ∈ range (d + 1), (d + 1).choose i • HPow.hPow (α := ℚ[X]) X i) =
    ∑ i ∈ range (d + 1), ((d + 2).choose (i + 1) * (i + 1)) • HPow.hPow (α := ℚ[X]) X i
⊢ ((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)
have calc₂ : ∑ i ∈ range (d + 1), ((d + 2).choose (i + 1) * (i + 1)) • HPow.hPow (α := ℚ[X]) X i =
  ∑ i ∈ range (d + 1), ((d + 2).choose i * i) • HPow.hPow (α := ℚ[X]) X (i - 1) +
    ((d + 2).choose (d + 1) * (d + 1)) • HPow.hPow (α := ℚ[X]) X (d + 1 - 1)
Tactic: calc ((d + 2) • X ^ (d + 1)).comp (1 + X) - (d + 2) • X ^ (d + 1)
    _ = (d + 2) • ∑ i ∈ range (d + 1), (d + 1).choose i • X ^ i := by
      rw [smul_comp, ← smul_sub, X_pow_comp, one_add_X_pow_sub_X_pow]
    _ = ∑ i ∈ range (d + 1), ((d + 2).choose (i + 1) * (i + 1)) • X ^ i := by
      simp_rw [smul_sum, smul_smul, ← add_one_mul_choose_eq (d + 1)]
    _ = ∑ i ∈ range (d + 1), ((d + 2).choose i * i) • X ^ (i - 1) +
          (((d + 2).choose (d + 1)) * (d + 1)) • X ^ (d + 1 - 1) := by
      rw [← sum_range_succ _ (d + 1)]; simp [sum_range_succ']
    _ = ∑ i ∈ range (d + 1), (d + 2).choose i • i • X ^ (i - 1) +
          ((d + 2) * (d + 1)) • X ^ (d + 1 - 1) := by
      simp [choose_succ_self_right, add_assoc, mul_assoc]
-- 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)
calc :
  ((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)
calc₁ :
  HSMul.hSMul (β := ℚ[X]) (d + 2) (∑ i ∈ range (d + 1), (d + 1).choose i • HPow.hPow (α := ℚ[X]) X i) =
    ∑ i ∈ range (d + 1), ((d + 2).choose (i + 1) * (i + 1)) • HPow.hPow (α := ℚ[X]) X i
calc₂ :
  ∑ i ∈ range (d + 1), ((d + 2).choose (i + 1) * (i + 1)) • HPow.hPow (α := ℚ[X]) X i =
    ∑ i ∈ range (d + 1), ((d + 2).choose i * i) • HPow.hPow (α := ℚ[X]) X (i - 1) +
      ((d + 2).choose (d + 1) * (d + 1)) • HPow.hPow (α := ℚ[X]) X (d + 1 - 1)
⊢ ((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)
have calc₃ : ∑ i ∈ range (d + 1), ((d + 2).choose i * i) • HPow.hPow (α := ℚ[X]) X (i - 1) +
    ((d + 2).choose (d + 1) * (d + 1)) • HPow.hPow (α := ℚ[X]) X (d + 1 - 1) =
  ∑ i ∈ range (d + 1), (d + 2).choose i • i • HPow.hPow (α := ℚ[X]) X (i - 1) +
    ((d + 2) * (d + 1)) • HPow.hPow (α := ℚ[X]) X (d + 1 - 1)
Tactic: calc ((d + 2) • X ^ (d + 1)).comp (1 + X) - (d + 2) • X ^ (d + 1)
    _ = (d + 2) • ∑ i ∈ range (d + 1), (d + 1).choose i • X ^ i := by
      rw [smul_comp, ← smul_sub, X_pow_comp, one_add_X_pow_sub_X_pow]
    _ = ∑ i ∈ range (d + 1), ((d + 2).choose (i + 1) * (i + 1)) • X ^ i := by
      simp_rw [smul_sum, smul_smul, ← add_one_mul_choose_eq (d + 1)]
    _ = ∑ i ∈ range (d + 1), ((d + 2).choose i * i) • X ^ (i - 1) +
          (((d + 2).choose (d + 1)) * (d + 1)) • X ^ (d + 1 - 1) := by
      rw [← sum_range_succ _ (d + 1)]; simp [sum_range_succ']
    _ = ∑ i ∈ range (d + 1), (d + 2).choose i • i • X ^ (i - 1) +
          ((d + 2) * (d + 1)) • X ^ (d + 1 - 1) := by
      simp [choose_succ_self_right, add_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n 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)
have zero : ∀ (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: cases d with
  | zero => simp
  | succ d =>
  rw [← smul_right_inj (show d + 2 ≠ 0 by positivity), ← smul_comp, smul_add]
  simp only [bernoulli_eq_sub_sum, sub_comp, sum_comp, add_assoc, one_add_one_eq_two, smul_smul]
  conv_lhs =>
    congr
    · skip
    · apply_congr
      · skip
      · rw [smul_comp, hd _ (mem_range.1 (by assumption))]
  simp_rw [smul_add, sum_add_distrib, sub_add, sub_add_eq_sub_sub_swap, sub_sub_eq_add_sub]
  congr 1
  rw [show ∀ a b c d : ℚ[X], a - b = c + d ↔ a - c = b + d by grind]
  calc ((d + 2) • X ^ (d + 1)).comp (1 + X) - (d + 2) • X ^ (d + 1)
    _ = (d + 2) • ∑ i ∈ range (d + 1), (d + 1).choose i • X ^ i := by
      rw [smul_comp, ← smul_sub, X_pow_comp, one_add_X_pow_sub_X_pow]
    _ = ∑ i ∈ range (d + 1), ((d + 2).choose (i + 1) * (i + 1)) • X ^ i := by
      simp_rw [smul_sum, smul_smul, ← add_one_mul_choose_eq (d + 1)]
    _ = ∑ i ∈ range (d + 1), ((d + 2).choose i * i) • X ^ (i - 1) +
          (((d + 2).choose (d + 1)) * (d + 1)) • X ^ (d + 1 - 1) := by
      rw [← sum_range_succ _ (d + 1)]; simp [sum_range_succ']
    _ = ∑ i ∈ range (d + 1), (d + 2).choose i • i • X ^ (i - 1) +
          ((d + 2) * (d + 1)) • X ^ (d + 1 - 1) := by
      simp [choose_succ_self_right, add_assoc, mul_assoc]
Cleared hypotheses: d, hd
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n d : ℕ
hd : ∀ m < d, (bernoulli m).comp (HAdd.hAdd (α := ℚ[X]) 1 X) = bernoulli m + m • HPow.hPow (α := ℚ[X]) X (m - 1)
zero :
  ∀ (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))
⊢ (bernoulli d).comp (HAdd.hAdd (α := ℚ[X]) 1 X) = bernoulli d + d • HPow.hPow (α := ℚ[X]) X (d - 1)
have succ : ∀ (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)
Tactic: cases d with
  | zero => simp
  | succ d =>
  rw [← smul_right_inj (show d + 2 ≠ 0 by positivity), ← smul_comp, smul_add]
  simp only [bernoulli_eq_sub_sum, sub_comp, sum_comp, add_assoc, one_add_one_eq_two, smul_smul]
  conv_lhs =>
    congr
    · skip
    · apply_congr
      · skip
      · rw [smul_comp, hd _ (mem_range.1 (by assumption))]
  simp_rw [smul_add, sum_add_distrib, sub_add, sub_add_eq_sub_sub_swap, sub_sub_eq_add_sub]
  congr 1
  rw [show ∀ a b c d : ℚ[X], a - b = c + d ↔ a - c = b + d by grind]
  calc ((d + 2) • X ^ (d + 1)).comp (1 + X) - (d + 2) • X ^ (d + 1)
    _ = (d + 2) • ∑ i ∈ range (d + 1), (d + 1).choose i • X ^ i := by
      rw [smul_comp, ← smul_sub, X_pow_comp, one_add_X_pow_sub_X_pow]
    _ = ∑ i ∈ range (d + 1), ((d + 2).choose (i + 1) * (i + 1)) • X ^ i := by
      simp_rw [smul_sum, smul_smul, ← add_one_mul_choose_eq (d + 1)]
    _ = ∑ i ∈ range (d + 1), ((d + 2).choose i * i) • X ^ (i - 1) +
          (((d + 2).choose (d + 1)) * (d + 1)) • X ^ (d + 1 - 1) := by
      rw [← sum_range_succ _ (d + 1)]; simp [sum_range_succ']
    _ = ∑ i ∈ range (d + 1), (d + 2).choose i • i • X ^ (i - 1) +
          ((d + 2) * (d + 1)) • X ^ (d + 1 - 1) := by
      simp [choose_succ_self_right, add_assoc, mul_assoc]
Cleared hypotheses: d, hd
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (hypothesis)
Goal:
n : ℕ
x : ℚ
⊢ eval (1 + x) (bernoulli n) = eval x (bernoulli n) + (↑n : ℚ) * x ^ (n - 1)
have this : (bernoulli n).comp (HAdd.hAdd (α := ℚ[X]) 1 X) = bernoulli n + n • HPow.hPow (α := ℚ[X]) X (n - 1)
Tactic: have := bernoulli_comp_one_add_X n
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n : ℕ
⊢ (bernoulli (n + 1)).comp (-X) =
    HPow.hPow (α := ℤ) (-1) (n + 1) • (bernoulli (n + 1) + (n + 1) • HPow.hPow (α := ℚ[X]) X (n + 1 - 1))
have succ : ∀ (i : ℕ),
  ((bernoulli (n + 1)).comp (-X)).coeff i =
    (HPow.hPow (α := ℤ) (-1) (n + 1) • (bernoulli (n + 1) + (n + 1) • HPow.hPow (α := ℚ[X]) X (n + 1 - 1))).coeff i
Tactic: ext i
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n i : ℕ
⊢ ((bernoulli (n + 1)).comp (-X)).coeff i =
    (HPow.hPow (α := ℤ) (-1) (n + 1) • (bernoulli (n + 1) + (n + 1) • HPow.hPow (α := ℚ[X]) X (n + 1 - 1))).coeff i
have succ : (if i ≤ n + 1 then _root_.bernoulli (n + 1 - i) * (↑((n + 1).choose i) : ℚ) else 0) * HPow.hPow (α := ℚ) (-1) i =
  HPow.hPow (α := ℤ) (-1) (n + 1) •
    ((if i ≤ n + 1 then _root_.bernoulli (n + 1 - i) * (↑((n + 1).choose i) : ℚ) else 0) +
      HSMul.hSMul (β := ℚ) (n + 1) (if i = n + 1 - 1 then 1 else 0))
Tactic: rw [← neg_one_mul, ← C_1, ← C_neg, Polynomial.comp_C_mul_X_coeff, coeff_smul, coeff_add,
    coeff_smul, coeff_bernoulli, coeff_X_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n i : ℕ
⊢ (if i ≤ n + 1 then _root_.bernoulli (n + 1 - i) * (↑((n + 1).choose i) : ℚ) else 0) * HPow.hPow (α := ℚ) (-1) i =
    HPow.hPow (α := ℤ) (-1) (n + 1) •
      ((if i ≤ n + 1 then _root_.bernoulli (n + 1 - i) * (↑((n + 1).choose i) : ℚ) else 0) +
        HSMul.hSMul (β := ℚ) (n + 1) (if i = n + 1 - 1 then 1 else 0))
have pos : ∀ (h : i ≤ n + 1) (h' : i = n + 1 - 1),
  _root_.bernoulli (n + 1 - i) * (↑((n + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (-1) i =
    HPow.hPow (α := ℤ) (-1) (n + 1) •
      (_root_.bernoulli (n + 1 - i) * (↑((n + 1).choose i) : ℚ) + HSMul.hSMul (β := ℚ) (n + 1) 1)
Tactic: split_ifs with h h'
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n i : ℕ
pos :
  ∀ (h : i ≤ n + 1) (h' : i = n + 1 - 1),
    _root_.bernoulli (n + 1 - i) * (↑((n + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (-1) i =
      HPow.hPow (α := ℤ) (-1) (n + 1) •
        (_root_.bernoulli (n + 1 - i) * (↑((n + 1).choose i) : ℚ) + HSMul.hSMul (β := ℚ) (n + 1) 1)
⊢ (if i ≤ n + 1 then _root_.bernoulli (n + 1 - i) * (↑((n + 1).choose i) : ℚ) else 0) * HPow.hPow (α := ℚ) (-1) i =
    HPow.hPow (α := ℤ) (-1) (n + 1) •
      ((if i ≤ n + 1 then _root_.bernoulli (n + 1 - i) * (↑((n + 1).choose i) : ℚ) else 0) +
        HSMul.hSMul (β := ℚ) (n + 1) (if i = n + 1 - 1 then 1 else 0))
have neg : ∀ (h : i ≤ n + 1) (h' : ¬i = n + 1 - 1),
  _root_.bernoulli (n + 1 - i) * (↑((n + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (-1) i =
    HPow.hPow (α := ℤ) (-1) (n + 1) •
      (_root_.bernoulli (n + 1 - i) * (↑((n + 1).choose i) : ℚ) + HSMul.hSMul (β := ℚ) (n + 1) 0)
Tactic: split_ifs with h h'
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n i : ℕ
pos :
  ∀ (h : i ≤ n + 1) (h' : i = n + 1 - 1),
    _root_.bernoulli (n + 1 - i) * (↑((n + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (-1) i =
      HPow.hPow (α := ℤ) (-1) (n + 1) •
        (_root_.bernoulli (n + 1 - i) * (↑((n + 1).choose i) : ℚ) + HSMul.hSMul (β := ℚ) (n + 1) 1)
neg :
  ∀ (h : i ≤ n + 1) (h' : ¬i = n + 1 - 1),
    _root_.bernoulli (n + 1 - i) * (↑((n + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (-1) i =
      HPow.hPow (α := ℤ) (-1) (n + 1) •
        (_root_.bernoulli (n + 1 - i) * (↑((n + 1).choose i) : ℚ) + HSMul.hSMul (β := ℚ) (n + 1) 0)
⊢ (if i ≤ n + 1 then _root_.bernoulli (n + 1 - i) * (↑((n + 1).choose i) : ℚ) else 0) * HPow.hPow (α := ℚ) (-1) i =
    HPow.hPow (α := ℤ) (-1) (n + 1) •
      ((if i ≤ n + 1 then _root_.bernoulli (n + 1 - i) * (↑((n + 1).choose i) : ℚ) else 0) +
        HSMul.hSMul (β := ℚ) (n + 1) (if i = n + 1 - 1 then 1 else 0))
have pos₁ : ∀ (h : ¬i ≤ n + 1),
  i = n + 1 - 1 → 0 * HPow.hPow (α := ℚ) (-1) i = HPow.hPow (α := ℤ) (-1) (n + 1) • (0 + HSMul.hSMul (β := ℚ) (n + 1) 1)
Tactic: split_ifs with h h'
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n i : ℕ
pos :
  ∀ (h : i ≤ n + 1) (h' : i = n + 1 - 1),
    _root_.bernoulli (n + 1 - i) * (↑((n + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (-1) i =
      HPow.hPow (α := ℤ) (-1) (n + 1) •
        (_root_.bernoulli (n + 1 - i) * (↑((n + 1).choose i) : ℚ) + HSMul.hSMul (β := ℚ) (n + 1) 1)
neg :
  ∀ (h : i ≤ n + 1) (h' : ¬i = n + 1 - 1),
    _root_.bernoulli (n + 1 - i) * (↑((n + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (-1) i =
      HPow.hPow (α := ℤ) (-1) (n + 1) •
        (_root_.bernoulli (n + 1 - i) * (↑((n + 1).choose i) : ℚ) + HSMul.hSMul (β := ℚ) (n + 1) 0)
pos₁ :
  ∀ (h : ¬i ≤ n + 1),
    i = n + 1 - 1 →
      0 * HPow.hPow (α := ℚ) (-1) i = HPow.hPow (α := ℤ) (-1) (n + 1) • (0 + HSMul.hSMul (β := ℚ) (n + 1) 1)
⊢ (if i ≤ n + 1 then _root_.bernoulli (n + 1 - i) * (↑((n + 1).choose i) : ℚ) else 0) * HPow.hPow (α := ℚ) (-1) i =
    HPow.hPow (α := ℤ) (-1) (n + 1) •
      ((if i ≤ n + 1 then _root_.bernoulli (n + 1 - i) * (↑((n + 1).choose i) : ℚ) else 0) +
        HSMul.hSMul (β := ℚ) (n + 1) (if i = n + 1 - 1 then 1 else 0))
have neg₁ : ∀ (h : ¬i ≤ n + 1),
  ¬i = n + 1 - 1 →
    0 * HPow.hPow (α := ℚ) (-1) i = HPow.hPow (α := ℤ) (-1) (n + 1) • (0 + HSMul.hSMul (β := ℚ) (n + 1) 0)
Tactic: split_ifs with h h'
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n i : ℕ
h : i ≤ n + 1
h' : i = n + 1 - 1
⊢ _root_.bernoulli (n + 1 - i) * (↑((n + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (-1) i =
    HPow.hPow (α := ℤ) (-1) (n + 1) •
      (_root_.bernoulli (n + 1 - i) * (↑((n + 1).choose i) : ℚ) + HSMul.hSMul (β := ℚ) (n + 1) 1)
have pos : ∀ (h : i ≤ i + 1),
  _root_.bernoulli (i + 1 - i) * (↑((i + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (-1) i =
    HPow.hPow (α := ℤ) (-1) (i + 1) •
      (_root_.bernoulli (i + 1 - i) * (↑((i + 1).choose i) : ℚ) + HSMul.hSMul (β := ℚ) (i + 1) 1)
Tactic: subst h'
Cleared hypotheses: n, h, h'
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
i : ℕ
h : i ≤ i + 1
⊢ _root_.bernoulli (i + 1 - i) * (↑((i + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (-1) i =
    HPow.hPow (α := ℤ) (-1) (i + 1) •
      (_root_.bernoulli (i + 1 - i) * (↑((i + 1).choose i) : ℚ) + HSMul.hSMul (β := ℚ) (i + 1) 1)
have pos : -1 / 2 * HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 * HPow.hPow (α := ℚ) (-1) i =
  HPow.hPow (α := ℚ) (-1) (i + 1) * (-1 / 2 * HAdd.hAdd (α := ℚ) (↑i : ℚ) 1) +
    (HPow.hPow (α := ℚ) (-1) (i + 1) * (↑i : ℚ) + HPow.hPow (α := ℚ) (-1) (i + 1))
Tactic: simp