awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n i : ℕ
h_1 : i ≤ n + 1
h' : ¬i = n + 1 - 1
h : Odd (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)
have 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)
Tactic: rw [bernoulli_eq_zero_of_odd]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
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)
⊢ _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)
have neg₂ : 1 < n + 1 - i
Tactic: rw [bernoulli_eq_zero_of_odd]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (hypothesis)
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) 0)
have x : 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
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n : ℕ
⊢ (bernoulli n).comp (-X) = HPow.hPow (α := ℤ) (-1) n • (bernoulli n + n • HPow.hPow (α := ℚ[X]) X (n - 1))
have zero : (bernoulli 0).comp (-X) =
  HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 •
    (bernoulli 0 + HSMul.hSMul (α := ℕ) 0 (HPow.hPow (α := ℚ[X]) X (HSub.hSub (α := ℕ) 0 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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n : ℕ
zero :
  (bernoulli 0).comp (-X) =
    HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 •
      (bernoulli 0 + HSMul.hSMul (α := ℕ) 0 (HPow.hPow (α := ℚ[X]) X (HSub.hSub (α := ℕ) 0 1)))
⊢ (bernoulli n).comp (-X) = HPow.hPow (α := ℤ) (-1) n • (bernoulli n + n • HPow.hPow (α := ℚ[X]) X (n - 1))
have succ : ∀ (n : ℕ),
  (bernoulli (n + 1)).comp (-X) =
    HPow.hPow (α := ℤ) (-1) (n + 1) • (bernoulli (n + 1) + (n + 1) • HPow.hPow (α := ℚ[X]) X (n + 1 - 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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n : ℕ
⊢ (bernoulli (n + 1)).comp (HSub.hSub (α := ℚ[X]) 1 X) = HPow.hPow (α := ℚ[X]) (-1) (n + 1) * bernoulli (n + 1)
have trans : (bernoulli (n + 1)).comp (HSub.hSub (α := ℚ[X]) 1 X) = ((bernoulli (n + 1)).comp (HAdd.hAdd (α := ℚ[X]) 1 X)).comp (-X)
Tactic: trans ((bernoulli (n + 1)).comp (1 + X)).comp (-X)
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n : ℕ
trans :
  (bernoulli (n + 1)).comp (HSub.hSub (α := ℚ[X]) 1 X) =
    ((bernoulli (n + 1)).comp (HAdd.hAdd (α := ℚ[X]) 1 X)).comp (-X)
⊢ (bernoulli (n + 1)).comp (HSub.hSub (α := ℚ[X]) 1 X) = HPow.hPow (α := ℚ[X]) (-1) (n + 1) * bernoulli (n + 1)
have trans₁ : ((bernoulli (n + 1)).comp (HAdd.hAdd (α := ℚ[X]) 1 X)).comp (-X) =
  HPow.hPow (α := ℚ[X]) (-1) (n + 1) * bernoulli (n + 1)
Tactic: trans ((bernoulli (n + 1)).comp (1 + X)).comp (-X)
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n : ℕ
⊢ ((bernoulli (n + 1)).comp (HAdd.hAdd (α := ℚ[X]) 1 X)).comp (-X) =
    HPow.hPow (α := ℚ[X]) (-1) (n + 1) * bernoulli (n + 1)
have 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)
Tactic: simp [bernoulli_comp_one_add_X, bernoulli_comp_neg_X, neg_pow (X : Polynomial ℚ)]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n : ℕ
⊢ (bernoulli n).comp (HSub.hSub (α := ℚ[X]) 1 X) = HPow.hPow (α := ℚ[X]) (-1) n * bernoulli n
have zero : (bernoulli 0).comp (HSub.hSub (α := ℚ[X]) 1 X) = HPow.hPow (α := ℚ[X]) (β := ℕ) (-1) 0 * bernoulli 0
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n : ℕ
zero : (bernoulli 0).comp (HSub.hSub (α := ℚ[X]) 1 X) = HPow.hPow (α := ℚ[X]) (β := ℕ) (-1) 0 * bernoulli 0
⊢ (bernoulli n).comp (HSub.hSub (α := ℚ[X]) 1 X) = HPow.hPow (α := ℚ[X]) (-1) n * bernoulli n
have succ : ∀ (n : ℕ), (bernoulli (n + 1)).comp (HSub.hSub (α := ℚ[X]) 1 X) = HPow.hPow (α := ℚ[X]) (-1) (n + 1) * bernoulli (n + 1)
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
t : 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⟧)
have 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)
Tactic: ext n
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
t : A
n : ℕ
⊢ Eq (α := A)
    ((PowerSeries.coeff (n + 1) : (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 + 1) : (a : A⟦X⟧) → A)
        (HMul.hMul (α := A⟦X⟧) (β := A⟦X⟧) PowerSeries.X ((rescale t : (a : A⟦X⟧) → A⟦X⟧) (exp A) : A⟦X⟧)) :
      A)
have h : ∑ x ∈ range (n + 1),
      HMul.hMul (α := A) (β := A)
        ((PowerSeries.coeff (x, n + 1 - x).1 : (a : A⟦X⟧) → A)
            (PowerSeries.mk fun (n : ℕ) ↦ (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
          A)
        ((PowerSeries.coeff (x, n + 1 - x).2 : (a : A⟦X⟧) → A) (exp A - 1) : A) +
    HMul.hMul (α := A) (β := A)
      ((PowerSeries.coeff (n + 1, n + 1 - (n + 1)).1 : (a : A⟦X⟧) → A)
          (PowerSeries.mk fun (n : ℕ) ↦ (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
        A)
      ((PowerSeries.coeff (n + 1, n + 1 - (n + 1)).2 : (a : A⟦X⟧) → A) (exp A - 1) : A) =
  HMul.hMul (β := A) (t ^ n) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A)
Tactic: rw [coeff_succ_X_mul, coeff_rescale, coeff_exp, PowerSeries.coeff_mul,
    Nat.sum_antidiagonal_eq_sum_range_succ_mk, sum_range_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
t : A
n : ℕ
⊢ ∑ x ∈ range (n + 1),
        HMul.hMul (α := A) (β := A)
          ((PowerSeries.coeff (x, n + 1 - x).1 : (a : A⟦X⟧) → A)
              (PowerSeries.mk fun (n : ℕ) ↦
                (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
            A)
          ((PowerSeries.coeff (x, n + 1 - x).2 : (a : A⟦X⟧) → A) (exp A - 1) : A) +
      HMul.hMul (α := A) (β := A)
        ((PowerSeries.coeff (n + 1, n + 1 - (n + 1)).1 : (a : A⟦X⟧) → A)
            (PowerSeries.mk fun (n : ℕ) ↦ (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
          A)
        ((PowerSeries.coeff (n + 1, n + 1 - (n + 1)).2 : (a : A⟦X⟧) → A) (exp A - 1) : A) =
    HMul.hMul (β := A) (t ^ n) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A)
have h : ∑ x ∈ range (n + 1),
    HMul.hMul (α := A)
      ((PowerSeries.coeff x : (a : A⟦X⟧) → A)
          (PowerSeries.mk fun (n : ℕ) ↦ (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
        A)
      (HSub.hSub (α := A) (β := A) ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) (exp A) : A)
        ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) 1 : A)) =
  HMul.hMul (β := A) (t ^ n) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A)
Tactic: simp only [map_sub, tsub_self, constantCoeff_one, constantCoeff_exp,
    coeff_zero_eq_constantCoeff, mul_zero, sub_self, add_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
t : A
n : ℕ
⊢ ∑ x ∈ range (n + 1),
      HMul.hMul (α := A)
        ((PowerSeries.coeff x : (a : A⟦X⟧) → A)
            (PowerSeries.mk fun (n : ℕ) ↦ (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
          A)
        (HSub.hSub (α := A) (β := A) ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) (exp A) : A)
          ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) 1 : A)) =
    HMul.hMul (β := A) (t ^ n) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A)
have hnp1 : IsUnit (M := ℚ) (↑(n + 1)! : ℚ)
Tactic: have hnp1 : IsUnit ((n + 1)! : ℚ) := IsUnit.mk0 _ (mod_cast factorial_ne_zero (n + 1))
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit (M := ℚ) (↑(n + 1)! : ℚ)
⊢ ∑ x ∈ range (n + 1),
      HMul.hMul (α := A)
        ((PowerSeries.coeff x : (a : A⟦X⟧) → A)
            (PowerSeries.mk fun (n : ℕ) ↦ (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
          A)
        (HSub.hSub (α := A) (β := A) ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) (exp A) : A)
          ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) 1 : A)) =
    HMul.hMul (β := A) (t ^ n) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A)
have h : HMul.hMul (α := A) (β := A) ((algebraMap ℚ A : (a : ℚ) → A) (↑(n + 1)! : ℚ) : A)
    (∑ x ∈ range (n + 1),
        HMul.hMul (α := A)
          ((PowerSeries.coeff x : (a : A⟦X⟧) → A)
              (PowerSeries.mk fun (n : ℕ) ↦
                (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
            A)
          (HSub.hSub (α := A) (β := A) ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) (exp A) : A)
            ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) 1 : A)) :
      A) =
  HMul.hMul (α := A) ((algebraMap ℚ A : (a : ℚ) → A) (↑(n + 1)! : ℚ) : A)
    (HMul.hMul (β := A) (t ^ n) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A))
Tactic: rw [← (hnp1.map (algebraMap ℚ A)).mul_right_inj]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit (M := ℚ) (↑(n + 1)! : ℚ)
⊢ HMul.hMul (α := A) (β := A) ((algebraMap ℚ A : (a : ℚ) → A) (↑(n + 1)! : ℚ) : A)
      (∑ x ∈ range (n + 1),
          HMul.hMul (α := A)
            ((PowerSeries.coeff x : (a : A⟦X⟧) → A)
                (PowerSeries.mk fun (n : ℕ) ↦
                  (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
              A)
            (HSub.hSub (α := A) (β := A) ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) (exp A) : A)
              ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) 1 : A)) :
        A) =
    HMul.hMul (α := A) ((algebraMap ℚ A : (a : ℚ) → A) (↑(n + 1)! : ℚ) : A)
      (HMul.hMul (β := A) (t ^ n) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A))
have h : HMul.hMul (α := A) (β := A) ((algebraMap ℚ A : (a : ℚ) → A) (↑(n + 1)! : ℚ) : A)
    (∑ x ∈ range (n + 1),
        HMul.hMul (α := A)
          ((PowerSeries.coeff x : (a : A⟦X⟧) → A)
              (PowerSeries.mk fun (n : ℕ) ↦
                (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
            A)
          (HSub.hSub (α := A) (β := A) ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) (exp A) : A)
            ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) 1 : A)) :
      A) =
  HMul.hMul (β := A) (t ^ n) ((algebraMap ℚ A : (a : ℚ) → A) ((↑(n + 1)! : ℚ) * HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A)
Tactic: rw [mul_left_comm, ← map_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit (M := ℚ) (↑(n + 1)! : ℚ)
⊢ HMul.hMul (α := A) (β := A) ((algebraMap ℚ A : (a : ℚ) → A) (↑(n + 1)! : ℚ) : A)
      (∑ x ∈ range (n + 1),
          HMul.hMul (α := A)
            ((PowerSeries.coeff x : (a : A⟦X⟧) → A)
                (PowerSeries.mk fun (n : ℕ) ↦
                  (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
              A)
            (HSub.hSub (α := A) (β := A) ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) (exp A) : A)
              ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) 1 : A)) :
        A) =
    HMul.hMul (β := A) (t ^ n) ((algebraMap ℚ A : (a : ℚ) → A) ((↑(n + 1)! : ℚ) * HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A)
have h : HMul.hMul (α := A) (β := A) ((algebraMap ℚ A : (a : ℚ) → A) (↑(n + 1)! : ℚ) : A)
    (∑ x ∈ range (n + 1),
        HMul.hMul (α := A)
          ((PowerSeries.coeff x : (a : A⟦X⟧) → A)
              (PowerSeries.mk fun (n : ℕ) ↦
                (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
            A)
          (HSub.hSub (α := A) (β := A) ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) (exp A) : A)
            ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) 1 : A)) :
      A) =
  HMul.hMul (β := A) (t ^ n)
    ((algebraMap ℚ A : (a : ℚ) → A) ((↑((n + 1) * n !) : ℚ) * HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A)
Tactic: change _ = t ^ n * algebraMap ℚ A (((n + 1) * n ! : ℕ) * (1 / n !))
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit (M := ℚ) (↑(n + 1)! : ℚ)
⊢ HMul.hMul (α := A) (β := A) ((algebraMap ℚ A : (a : ℚ) → A) (↑(n + 1)! : ℚ) : A)
      (∑ x ∈ range (n + 1),
          HMul.hMul (α := A)
            ((PowerSeries.coeff x : (a : A⟦X⟧) → A)
                (PowerSeries.mk fun (n : ℕ) ↦
                  (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
              A)
            (HSub.hSub (α := A) (β := A) ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) (exp A) : A)
              ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) 1 : A)) :
        A) =
    HMul.hMul (β := A) (t ^ n)
      ((algebraMap ℚ A : (a : ℚ) → A) ((↑((n + 1) * n !) : ℚ) * HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A)
have h : HMul.hMul (α := A) (β := A) ((algebraMap ℚ A : (a : ℚ) → A) (↑(n + 1)! : ℚ) : A)
    (∑ x ∈ range (n + 1),
        HMul.hMul (α := A)
          ((PowerSeries.coeff x : (a : A⟦X⟧) → A)
              (PowerSeries.mk fun (n : ℕ) ↦
                (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
            A)
          (HSub.hSub (α := A) (β := A) ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) (exp A) : A)
            ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) 1 : A)) :
      A) =
  (aeval t : (a : ℚ[X]) → A) ((monomial n : (a : ℚ) → ℚ[X]) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1) : ℚ[X])
Tactic: rw [cast_mul, mul_assoc,
    mul_one_div_cancel (show (n ! : ℚ) ≠ 0 from cast_ne_zero.2 (factorial_ne_zero n)), mul_one,
    mul_comm (t ^ n), ← aeval_monomial, cast_add, cast_one]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit (M := ℚ) (↑(n + 1)! : ℚ)
⊢ HMul.hMul (α := A) (β := A) ((algebraMap ℚ A : (a : ℚ) → A) (↑(n + 1)! : ℚ) : A)
      (∑ x ∈ range (n + 1),
          HMul.hMul (α := A)
            ((PowerSeries.coeff x : (a : A⟦X⟧) → A)
                (PowerSeries.mk fun (n : ℕ) ↦
                  (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
              A)
            (HSub.hSub (α := A) (β := A) ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) (exp A) : A)
              ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) 1 : A)) :
        A) =
    (aeval t : (a : ℚ[X]) → A) ((monomial n : (a : ℚ) → ℚ[X]) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1) : ℚ[X])
have h : Eq.{u_1 + 1} (α := A)
  (∑ i ∈ range (n + 1),
    HMul.hMul (α := A) ((algebraMap ℚ A : (a : ℚ) → A) (↑(n + 1)! : ℚ) : A)
      (HMul.hMul (α := A)
        ((PowerSeries.coeff i : (a : A⟦X⟧) → A)
            (PowerSeries.mk fun (n : ℕ) ↦ (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
          A)
        (HSub.hSub (α := A) (β := A) ((PowerSeries.coeff (n + 1 - i) : (a : A⟦X⟧) → A) (exp A) : A)
          ((PowerSeries.coeff (n + 1 - i) : (a : A⟦X⟧) → A) 1 : A))))
  (∑ x ∈ range (n + 1), (aeval t : (a : ℚ[X]) → A) (HSMul.hSMul (α := ℚ) (↑((n + 1).choose x) : ℚ) (bernoulli x)))
Tactic: rw [← sum_bernoulli, Finset.mul_sum, map_sum]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit (M := ℚ) (↑(n + 1)! : ℚ)
⊢ Eq.{u_1 + 1} (α := A)
    (∑ i ∈ range (n + 1),
      HMul.hMul (α := A) ((algebraMap ℚ A : (a : ℚ) → A) (↑(n + 1)! : ℚ) : A)
        (HMul.hMul (α := A)
          ((PowerSeries.coeff i : (a : A⟦X⟧) → A)
              (PowerSeries.mk fun (n : ℕ) ↦
                (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
            A)
          (HSub.hSub (α := A) (β := A) ((PowerSeries.coeff (n + 1 - i) : (a : A⟦X⟧) → A) (exp A) : A)
            ((PowerSeries.coeff (n + 1 - i) : (a : A⟦X⟧) → A) 1 : A))))
    (∑ x ∈ range (n + 1), (aeval t : (a : ℚ[X]) → A) (HSMul.hSMul (α := ℚ) (↑((n + 1).choose x) : ℚ) (bernoulli x)))
have h : ∀ x ∈ range (n + 1),
  HMul.hMul (α := A) ((algebraMap ℚ A : (a : ℚ) → A) (↑(n + 1)! : ℚ) : A)
      (HMul.hMul (α := A)
        ((PowerSeries.coeff x : (a : A⟦X⟧) → A)
            (PowerSeries.mk fun (n : ℕ) ↦ (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
          A)
        (HSub.hSub (α := A) (β := A) ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) (exp A) : A)
          ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) 1 : A))) =
    (aeval t : (a : ℚ[X]) → A) (HSMul.hSMul (α := ℚ) (↑((n + 1).choose x) : ℚ) (bernoulli x))
Tactic: apply Finset.sum_congr rfl
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit (M := ℚ) (↑(n + 1)! : ℚ)
i : ℕ
hi : i ∈ range (n + 1)
⊢ HMul.hMul (α := A) ((algebraMap ℚ A : (a : ℚ) → A) (↑(n + 1)! : ℚ) : A)
      (HMul.hMul (α := A)
        ((PowerSeries.coeff i : (a : A⟦X⟧) → A)
            (PowerSeries.mk fun (n : ℕ) ↦ (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
          A)
        (HSub.hSub (α := A) (β := A) ((PowerSeries.coeff (n + 1 - i) : (a : A⟦X⟧) → A) (exp A) : A)
          ((PowerSeries.coeff (n + 1 - i) : (a : A⟦X⟧) → A) 1 : A))) =
    (aeval t : (a : ℚ[X]) → A) (HSMul.hSMul (α := ℚ) (↑((n + 1).choose i) : ℚ) (bernoulli i))
have h : HMul.hMul (α := A) (β := A)
    ((algebraMap ℚ A : (a : ℚ) → A)
        ((↑(n + 1)! : ℚ) * HDiv.hDiv (α := ℚ) 1 (↑i ! : ℚ) * HDiv.hDiv (α := ℚ) 1 (↑(n + 1 - i)! : ℚ)) :
      A)
    ((aeval t : (a : ℚ[X]) → A) (bernoulli i) : A) =
  HMul.hMul (α := A) (β := A)
    ((algebraMap ℚ A : (a : ℚ) → A) ((↑(n + 1)! : ℚ) / HMul.hMul (α := ℚ) (↑i ! : ℚ) (↑(n + 1 - i)! : ℚ)) : A)
    ((aeval t : (a : ℚ[X]) → A) (bernoulli i) : A)
Tactic: simp only [Nat.cast_choose ℚ (mem_range_le hi), coeff_mk, if_neg (mem_range_sub_ne_zero hi),
    PowerSeries.coeff_one, coeff_exp, sub_zero, Algebra.smul_def,
    mul_right_comm _ ((aeval t) _), ← mul_assoc, ← map_mul, ← Polynomial.C_eq_algebraMap,
    Polynomial.aeval_mul, Polynomial.aeval_C]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
t : A
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)
have h : Eq (α := A)
  ((PowerSeries.coeff 0 : (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 0 : (a : A⟦X⟧) → A)
      (HMul.hMul (α := A⟦X⟧) (β := A⟦X⟧) PowerSeries.X ((rescale t : (a : A⟦X⟧) → A⟦X⟧) (exp A) : A⟦X⟧)) :
    A)
Tactic: cases n with | zero => simp | succ n =>
  -- n ≥ 1, the coefficients is a sum to n+2, so use `sum_range_succ` to write as
  -- last term plus sum to n+1
  rw [coeff_succ_X_mul, coeff_rescale, coeff_exp, PowerSeries.coeff_mul,
    Nat.sum_antidiagonal_eq_sum_range_succ_mk, sum_range_succ]
  -- last term is zero so kill with `add_zero`
  simp only [map_sub, tsub_self, constantCoeff_one, constantCoeff_exp,
    coeff_zero_eq_constantCoeff, mul_zero, sub_self, add_zero]
  -- Let's multiply both sides by (n+1)! (OK because it's a unit)
  have hnp1 : IsUnit ((n + 1)! : ℚ) := IsUnit.mk0 _ (mod_cast factorial_ne_zero (n + 1))
  rw [← (hnp1.map (algebraMap ℚ A)).mul_right_inj]
  -- do trivial rearrangements to make RHS (n+1)*t^n
  rw [mul_left_comm, ← map_mul]
  change _ = t ^ n * algebraMap ℚ A (((n + 1) * n ! : ℕ) * (1 / n !))
  rw [cast_mul, mul_assoc,
    mul_one_div_cancel (show (n ! : ℚ) ≠ 0 from cast_ne_zero.2 (factorial_ne_zero n)), mul_one,
    mul_comm (t ^ n), ← aeval_monomial, cast_add, cast_one]
  -- But this is the RHS of `Polynomial.sum_bernoulli`
  rw [← sum_bernoulli, Finset.mul_sum, map_sum]
  -- and now we have to prove a sum is a sum, but all the terms are equal.
  apply Finset.sum_congr rfl
  -- The rest is just trivialities, hampered by the fact that we're coercing
  -- factorials and binomial coefficients between ℕ and ℚ and A.
  intro i hi
  -- deal with coefficients of e^X-1
  simp only [Nat.cast_choose ℚ (mem_range_le hi), coeff_mk, if_neg (mem_range_sub_ne_zero hi),
    PowerSeries.coeff_one, coeff_exp, sub_zero, Algebra.smul_def,
    mul_right_comm _ ((aeval t) _), ← mul_assoc, ← map_mul, ← Polynomial.C_eq_algebraMap,
    Polynomial.aeval_mul, Polynomial.aeval_C]
  -- finally cancel the Bernoulli polynomial and the algebra_map
  field_simp
Cleared hypotheses: n