awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) =
    (d + 2) • HPow.hPow (α := ℚ[X]) X (d + 1) + ((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) -
        ∑ 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:
congr 1
-- 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 b c d : ℚ[X]), a - b = c + d ↔ a - c = b + d

Tactic:
grind
-- 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) -
      (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)
⊢ ((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:
rw [show ∀ a b c d : ℚ[X], a - b = c + d ↔ a - c = b + d by grind]
-- 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)
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)
rw₃ 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)
⊢ ((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]

Premises used: Polynomial.one_add_X_pow_sub_X_pow, smul_sub, Polynomial.X_pow_comp, 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)
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)
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

Tactic:
simp_rw [smul_sum, smul_smul, ← add_one_mul_choose_eq (d + 1)]

Premises used: smul_smul, HAdd.hAdd, Nat.add_one_mul_choose_eq, Finset.smul_sum, OfNat.ofNat
-- 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)
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))
⊢ ∑ 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:
rw [← sum_range_succ _ (d + 1)]

Premises used: HAdd.hAdd, OfNat.ofNat, Finset.sum_range_succ
-- 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)
⊢ 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:
simp [sum_range_succ']

Premises used: Finset.sum_range_succ'
-- 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)
⊢ ∑ 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:
simp [choose_succ_self_right, add_assoc, mul_assoc]

Premises used: add_assoc, mul_assoc, Nat.choose_succ_self_right
-- 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)
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)
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)
⊢ ((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:
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]

Premises used: Nat.choose, HMul.hMul, HSub.hSub, Finset.range, HPow.hPow, HAdd.hAdd, HSMul.hSMul, OfNat.ofNat, Polynomial.X, Polynomial.comp
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
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))
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)
⊢ (bernoulli d).comp (HAdd.hAdd (α := ℚ[X]) 1 X) = bernoulli d + d • HPow.hPow (α := ℚ[X]) X (d - 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]

Premises used: sub_add, Nat.choose, HMul.hMul, Finset.sum_add_distrib, add_assoc, HSub.hSub, smul_smul, Polynomial.sum_comp, sub_sub_eq_add_sub, Finset.mem_range, Polynomial.bernoulli_eq_sub_sum, one_add_one_eq_two, Finset.range, HPow.hPow, HAdd.hAdd, Iff.mp, Nat.zero, HSMul.hSMul, OfNat.ofNat, Polynomial.X, Nat.succ, Polynomial.comp, smul_add, smul_right_inj, Polynomial.smul_comp, Polynomial.sub_comp, sub_add_eq_sub_sub_swap
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n : ℕ
x : ℚ
⊢ (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
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n : ℕ
x : ℚ
this : (bernoulli n).comp (HAdd.hAdd (α := ℚ[X]) 1 X) = bernoulli n + n • HPow.hPow (α := ℚ[X]) X (n - 1)
⊢ eval (1 + x) (bernoulli n) = eval x (bernoulli n) + (↑n : ℚ) * x ^ (n - 1)

Tactic:
simpa using congr(Polynomial.eval x $this)
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
⊢ (bernoulli 0).comp (-X) =
    HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 •
      (bernoulli 0 + HSMul.hSMul (α := ℕ) 0 (HPow.hPow (α := ℚ[X]) X (HSub.hSub (α := ℕ) 0 1)))

Tactic:
simp
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n : ℕ
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
⊢ (bernoulli (n + 1)).comp (-X) =
    HPow.hPow (α := ℤ) (-1) (n + 1) • (bernoulli (n + 1) + (n + 1) • HPow.hPow (α := ℚ[X]) X (n + 1 - 1))

Tactic:
ext i
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n i : ℕ
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))
⊢ ((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:
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]

Premises used: Polynomial.C_1, Polynomial.coeff_X_pow, neg_one_mul, Polynomial.comp_C_mul_X_coeff, Polynomial.coeff_add, Polynomial.coeff_smul, Polynomial.C_neg, Polynomial.coeff_bernoulli
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
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)
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)
⊢ (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:
split_ifs with h h'
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n i : ℕ
h : i ≤ n + 1
h' : i = n + 1 - 1
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)
⊢ _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:
subst h'
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
i : ℕ
h : i ≤ i + 1
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))
⊢ _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:
simp
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
i : ℕ
h : i ≤ i + 1
⊢ -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:
grind
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n i : ℕ
h_1 : i ≤ n + 1
h' : ¬i = n + 1 - 1
h : Even (n + 1 - i)
⊢ _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:
grind [neg_one_pow_eq_ite]

Premises used: neg_one_pow_eq_ite
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n i : ℕ
h_1 : i ≤ n + 1
h' : ¬i = n + 1 - 1
h : Odd (n + 1 - i)
neg :
  HMul.hMul (α := ℚ) 0 (↑((n + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (-1) i =
    HPow.hPow (α := ℤ) (-1) (n + 1) • (HMul.hMul (α := ℚ) 0 (↑((n + 1).choose i) : ℚ) + HSMul.hSMul (β := ℚ) (n + 1) 0)
neg₁ : Odd (n + 1 - i)
neg₂ : 1 < n + 1 - i
⊢ _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:
rw [bernoulli_eq_zero_of_odd]

Premises used: bernoulli_eq_zero_of_odd
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n i : ℕ
h_1 : i ≤ n + 1
h' : ¬i = n + 1 - 1
h : Odd (n + 1 - i)
⊢ HMul.hMul (α := ℚ) 0 (↑((n + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (-1) i =
    HPow.hPow (α := ℤ) (-1) (n + 1) • (HMul.hMul (α := ℚ) 0 (↑((n + 1).choose i) : ℚ) + HSMul.hSMul (β := ℚ) (n + 1) 0)

Tactic:
grind
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n i : ℕ
h_1 : i ≤ n + 1
h' : ¬i = n + 1 - 1
h : Odd (n + 1 - i)
⊢ Odd (n + 1 - i)

Tactic:
grind
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n i : ℕ
h_1 : i ≤ n + 1
h' : ¬i = n + 1 - 1
h : Odd (n + 1 - i)
⊢ 1 < n + 1 - i

Tactic:
grind
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n i : ℕ
h : i ≤ n + 1
h' : ¬i = n + 1 - 1
⊢ Even (n + 1 - i) ∨ Odd (n + 1 - i)

Tactic:
cases (n + 1 - i).even_or_odd with
    | inl h => grind [neg_one_pow_eq_ite]
    | inr h => rw [bernoulli_eq_zero_of_odd] <;> grind

Premises used: neg_one_pow_eq_ite, HSub.hSub, bernoulli_eq_zero_of_odd, HAdd.hAdd, OfNat.ofNat, Nat.even_or_odd
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n i : ℕ
h : ¬i ≤ n + 1
h_1 : i = n + 1 - 1
⊢ 0 * HPow.hPow (α := ℚ) (-1) i = HPow.hPow (α := ℤ) (-1) (n + 1) • (0 + HSMul.hSMul (β := ℚ) (n + 1) 1)

Tactic:
grind
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n i : ℕ
h : ¬i ≤ n + 1
h_1 : ¬i = n + 1 - 1
⊢ 0 * HPow.hPow (α := ℚ) (-1) i = HPow.hPow (α := ℤ) (-1) (n + 1) • (0 + HSMul.hSMul (β := ℚ) (n + 1) 0)

Tactic:
simp
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n : ℕ
zero :
  (bernoulli 0).comp (-X) =
    HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 •
      (bernoulli 0 + HSMul.hSMul (α := ℕ) 0 (HPow.hPow (α := ℚ[X]) X (HSub.hSub (α := ℕ) 0 1)))
succ :
  ∀ (n : ℕ),
    (bernoulli (n + 1)).comp (-X) =
      HPow.hPow (α := ℤ) (-1) (n + 1) • (bernoulli (n + 1) + (n + 1) • HPow.hPow (α := ℚ[X]) X (n + 1 - 1))
⊢ (bernoulli n).comp (-X) = HPow.hPow (α := ℤ) (-1) n • (bernoulli n + n • HPow.hPow (α := ℚ[X]) X (n - 1))

Tactic:
cases n with
  | zero => simp
  | succ n =>
  ext i
  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]
  split_ifs with h h'
  · subst h'
    simp
    grind
  · cases (n + 1 - i).even_or_odd with
    | inl h => grind [neg_one_pow_eq_ite]
    | inr h => rw [bernoulli_eq_zero_of_odd] <;> grind
  · grind
  · simp

Premises used: neg_one_pow_eq_ite, Polynomial.C_1, Polynomial.coeff_X_pow, neg_one_mul, Polynomial.comp_C_mul_X_coeff, Polynomial.coeff_add, bernoulli_eq_zero_of_odd, Polynomial.coeff_smul, Nat.zero, Polynomial.C_neg, Polynomial.coeff_bernoulli, Nat.succ
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n : ℕ
x : ℚ
⊢ eval (-x) (bernoulli n) = HPow.hPow (α := ℚ) (-1) n * (eval x (bernoulli n) + (↑n : ℚ) * x ^ (n - 1))

Tactic:
simpa [mul_add] using congr_arg (Polynomial.eval x) (bernoulli_comp_neg_X n)

Premises used: Polynomial.eval, congr_arg, mul_add, Polynomial.bernoulli_comp_neg_X
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
⊢ (bernoulli 0).comp (HSub.hSub (α := ℚ[X]) 1 X) = HPow.hPow (α := ℚ[X]) (β := ℕ) (-1) 0 * bernoulli 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n : ℕ
trans :
  (bernoulli (n + 1)).comp (HSub.hSub (α := ℚ[X]) 1 X) =
    ((bernoulli (n + 1)).comp (HAdd.hAdd (α := ℚ[X]) 1 X)).comp (-X)
trans₁ :
  ((bernoulli (n + 1)).comp (HAdd.hAdd (α := ℚ[X]) 1 X)).comp (-X) =
    HPow.hPow (α := ℚ[X]) (-1) (n + 1) * bernoulli (n + 1)
⊢ (bernoulli (n + 1)).comp (HSub.hSub (α := ℚ[X]) 1 X) = HPow.hPow (α := ℚ[X]) (-1) (n + 1) * bernoulli (n + 1)

Tactic:
trans ((bernoulli (n + 1)).comp (1 + X)).comp (-X)

Premises used: Polynomial.bernoulli, HAdd.hAdd, OfNat.ofNat, Polynomial.X, Polynomial.comp, Neg.neg
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n : ℕ
⊢ (bernoulli (n + 1)).comp (HSub.hSub (α := ℚ[X]) 1 X) =
    ((bernoulli (n + 1)).comp (HAdd.hAdd (α := ℚ[X]) 1 X)).comp (-X)

Tactic:
simp [comp_assoc, sub_eq_add_neg]

Premises used: Polynomial.comp_assoc, sub_eq_add_neg
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n : ℕ
simp :
  HPow.hPow (α := ℚ[X]) (-1) (n + 1) *
        (bernoulli (n + 1) + HAdd.hAdd (α := ℚ[X]) (↑n : ℚ[X]) 1 * HPow.hPow (α := ℚ[X]) X n) +
      HAdd.hAdd (α := ℚ[X]) (↑n : ℚ[X]) 1 * (HPow.hPow (α := ℚ[X]) (-1) n * HPow.hPow (α := ℚ[X]) X n) =
    HPow.hPow (α := ℚ[X]) (-1) (n + 1) * bernoulli (n + 1)
⊢ ((bernoulli (n + 1)).comp (HAdd.hAdd (α := ℚ[X]) 1 X)).comp (-X) =
    HPow.hPow (α := ℚ[X]) (-1) (n + 1) * bernoulli (n + 1)

Tactic:
simp [bernoulli_comp_one_add_X, bernoulli_comp_neg_X, neg_pow (X : Polynomial ℚ)]

Premises used: Polynomial.bernoulli_comp_one_add_X, neg_pow, Polynomial.X, Polynomial.bernoulli_comp_neg_X
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n : ℕ
⊢ HPow.hPow (α := ℚ[X]) (-1) (n + 1) *
        (bernoulli (n + 1) + HAdd.hAdd (α := ℚ[X]) (↑n : ℚ[X]) 1 * HPow.hPow (α := ℚ[X]) X n) +
      HAdd.hAdd (α := ℚ[X]) (↑n : ℚ[X]) 1 * (HPow.hPow (α := ℚ[X]) (-1) n * HPow.hPow (α := ℚ[X]) X n) =
    HPow.hPow (α := ℚ[X]) (-1) (n + 1) * bernoulli (n + 1)

Tactic:
ring
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n : ℕ
zero : (bernoulli 0).comp (HSub.hSub (α := ℚ[X]) 1 X) = HPow.hPow (α := ℚ[X]) (β := ℕ) (-1) 0 * bernoulli 0
succ :
  ∀ (n : ℕ),
    (bernoulli (n + 1)).comp (HSub.hSub (α := ℚ[X]) 1 X) = HPow.hPow (α := ℚ[X]) (-1) (n + 1) * bernoulli (n + 1)
⊢ (bernoulli n).comp (HSub.hSub (α := ℚ[X]) 1 X) = HPow.hPow (α := ℚ[X]) (-1) n * bernoulli n

Tactic:
cases n with
  | zero => simp
  | succ n =>
    trans ((bernoulli (n + 1)).comp (1 + X)).comp (-X)
    · simp [comp_assoc, sub_eq_add_neg]
    simp [bernoulli_comp_one_add_X, bernoulli_comp_neg_X, neg_pow (X : Polynomial ℚ)]
    ring

Premises used: Polynomial.comp_assoc, Polynomial.bernoulli, sub_eq_add_neg, Polynomial.bernoulli_comp_one_add_X, HAdd.hAdd, neg_pow, Nat.zero, OfNat.ofNat, Polynomial.X, Nat.succ, Polynomial.comp, Polynomial.bernoulli_comp_neg_X, Neg.neg
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n : ℕ
x : ℚ
⊢ eval (1 - x) (bernoulli n) = HPow.hPow (α := ℚ) (-1) n * eval x (bernoulli n)

Tactic:
simpa using congr_arg (Polynomial.eval x) (bernoulli_comp_one_sub_X n)

Premises used: Polynomial.eval, congr_arg, Polynomial.bernoulli_comp_one_sub_X
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
t : A
h :
  ∀ (n : ℕ),
    Eq (α := A)
      ((PowerSeries.coeff n : (a : A⟦X⟧) → A)
          ((PowerSeries.mk fun (n : ℕ) ↦ (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) *
            (exp A - 1)) :
        A)
      ((PowerSeries.coeff n : (a : A⟦X⟧) → A)
          (HMul.hMul (α := A⟦X⟧) (β := A⟦X⟧) PowerSeries.X ((rescale t : (a : A⟦X⟧) → A⟦X⟧) (exp A) : A⟦X⟧)) :
        A)
⊢ (PowerSeries.mk fun (n : ℕ) ↦ (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) *
      (exp A - 1) =
    HMul.hMul (α := A⟦X⟧) (β := A⟦X⟧) PowerSeries.X ((rescale t : (a : A⟦X⟧) → A⟦X⟧) (exp A) : A⟦X⟧)

Tactic:
ext n