-- Mathlib/NumberTheory/BernoulliPolynomials.lean
theorem bernoulli_generating_function (t : A) :
    (mk fun n => aeval t ((1 / n ! : ℚ) • bernoulli n)) * (exp A - 1) =
      PowerSeries.X * rescale t (exp A)

Proof state:
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
⊢ (PowerSeries.coeff A (n + 1)) ((PowerSeries.mk fun n => (aeval t) ((1 / ↑n !) • bernoulli n)) * (exp A - 1)) =
    (PowerSeries.coeff A (n + 1)) (PowerSeries.X * (rescale t) (exp 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]

Result:
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
⊢ ∑ x ∈ range (n + 1),
        (PowerSeries.coeff A (x, n + 1 - x).1) (PowerSeries.mk fun n => (aeval t) ((1 / ↑n !) • bernoulli n)) *
          (PowerSeries.coeff A (x, n + 1 - x).2) (exp A - 1) +
      (PowerSeries.coeff A (n + 1, n + 1 - (n + 1)).1) (PowerSeries.mk fun n => (aeval t) ((1 / ↑n !) • bernoulli n)) *
        (PowerSeries.coeff A (n + 1, n + 1 - (n + 1)).2) (exp A - 1) =
    t ^ n * (algebraMap ℚ A) (1 / ↑n !)

Proof state:
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
i : ℕ
hi : i ∈ range (n + 1)
⊢ (algebraMap ℚ A) ↑(n + 1)! *
      ((PowerSeries.coeff A i) (PowerSeries.mk fun n => (aeval t) ((1 / ↑n !) • bernoulli n)) *
        (PowerSeries.coeff A (n + 1 - i)) (exp A - 1)) =
    (aeval t) (↑((n + 1).choose i) • bernoulli i)

Tactic:
simp only [Nat.cast_choose ℚ (mem_range_le hi), coeff_mk, if_neg (mem_range_sub_ne_zero hi),
  one_div, map_smul, PowerSeries.coeff_one, coeff_exp, sub_zero, LinearMap.map_sub,
  Algebra.smul_mul_assoc, Algebra.smul_def, mul_right_comm _ ((aeval t) _), ← mul_assoc, ←
  RingHom.map_mul, succ_eq_add_one, ← Polynomial.C_eq_algebraMap, Polynomial.aeval_mul,
  Polynomial.aeval_C]

Result:
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
i : ℕ
hi : i ∈ range (n + 1)
⊢ (algebraMap ℚ A) (↑(n + 1)! * (↑i !)⁻¹ * (↑(n + 1 - i)!)⁻¹) * (aeval t) (bernoulli i) =
    (algebraMap ℚ A) (↑(n + 1)! / (↑i ! * ↑(n + 1 - i)!)) * (aeval t) (bernoulli i)

Proof state:
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
i : ℕ
hi : i ∈ range (n + 1)
⊢ (algebraMap ℚ A) (↑(n + 1)! * (↑i !)⁻¹ * (↑(n + 1 - i)!)⁻¹) * (aeval t) (bernoulli i) =
    (algebraMap ℚ A) (↑(n + 1)! / (↑i ! * ↑(n + 1 - i)!)) * (aeval t) (bernoulli i)

Tactic:
field_simp

Result:
no goals

Proof state:
case h.zero
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
⊢ (PowerSeries.coeff A 0) ((PowerSeries.mk fun n => (aeval t) ((1 / ↑n !) • bernoulli n)) * (exp A - 1)) =
    (PowerSeries.coeff A 0) (PowerSeries.X * (rescale t) (exp A))

Tactic:
simp

Result:
no goals

Proof state:
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
⊢ (algebraMap ℚ A) ↑(n + 1)! *
      ∑ x ∈ range (n + 1),
        (PowerSeries.coeff A x) (PowerSeries.mk fun n => (aeval t) ((1 / ↑n !) • bernoulli n)) *
          (PowerSeries.coeff A (n + 1 - x)) (exp A - 1) =
    (aeval t) ((monomial n) (↑n + 1))

Tactic:
rw [← sum_bernoulli, Finset.mul_sum, map_sum]

Result:
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
⊢ ∑ i ∈ range (n + 1),
      (algebraMap ℚ A) ↑(n + 1)! *
        ((PowerSeries.coeff A i) (PowerSeries.mk fun n => (aeval t) ((1 / ↑n !) • bernoulli n)) *
          (PowerSeries.coeff A (n + 1 - i)) (exp A - 1)) =
    ∑ x ∈ range (n + 1), (aeval t) (↑((n + 1).choose x) • bernoulli x)

Proof state:
case h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
⊢ (PowerSeries.coeff A n) ((PowerSeries.mk fun n => (aeval t) ((1 / ↑n !) • bernoulli n)) * (exp A - 1)) =
    (PowerSeries.coeff A n) (PowerSeries.X * (rescale t) (exp A))

Tactic:
cases n with | zero => simp | succ n =>
rw [coeff_succ_X_mul, coeff_rescale, coeff_exp, PowerSeries.coeff_mul,
  Nat.sum_antidiagonal_eq_sum_range_succ_mk, sum_range_succ]
simp only [RingHom.map_sub, tsub_self, constantCoeff_one, constantCoeff_exp,
  coeff_zero_eq_constantCoeff, mul_zero, sub_self, add_zero]
have hnp1 : IsUnit ((n + 1)! : ℚ) := IsUnit.mk0 _ (mod_cast factorial_ne_zero (n + 1))
rw [← (hnp1.map (algebraMap ℚ A)).mul_right_inj]
rw [mul_left_comm, ← RingHom.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]
rw [← sum_bernoulli, Finset.mul_sum, map_sum]
apply Finset.sum_congr rfl
intro i hi
simp only [Nat.cast_choose ℚ (mem_range_le hi), coeff_mk, if_neg (mem_range_sub_ne_zero hi),
  one_div, map_smul, PowerSeries.coeff_one, coeff_exp, sub_zero, LinearMap.map_sub,
  Algebra.smul_mul_assoc, Algebra.smul_def, mul_right_comm _ ((aeval t) _), ← mul_assoc, ←
  RingHom.map_mul, succ_eq_add_one, ← Polynomial.C_eq_algebraMap, Polynomial.aeval_mul,
  Polynomial.aeval_C]
field_simp

Result:
no goals

Proof state:
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
⊢ ∑ x ∈ range (n + 1),
        (PowerSeries.coeff A (x, n + 1 - x).1) (PowerSeries.mk fun n => (aeval t) ((1 / ↑n !) • bernoulli n)) *
          (PowerSeries.coeff A (x, n + 1 - x).2) (exp A - 1) +
      (PowerSeries.coeff A (n + 1, n + 1 - (n + 1)).1) (PowerSeries.mk fun n => (aeval t) ((1 / ↑n !) • bernoulli n)) *
        (PowerSeries.coeff A (n + 1, n + 1 - (n + 1)).2) (exp A - 1) =
    t ^ n * (algebraMap ℚ A) (1 / ↑n !)

Tactic:
simp only [RingHom.map_sub, tsub_self, constantCoeff_one, constantCoeff_exp,
  coeff_zero_eq_constantCoeff, mul_zero, sub_self, add_zero]

Result:
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
⊢ ∑ x ∈ range (n + 1),
      (PowerSeries.coeff A x) (PowerSeries.mk fun n => (aeval t) ((1 / ↑n !) • bernoulli n)) *
        (PowerSeries.coeff A (n + 1 - x)) (exp A - 1) =
    t ^ n * (algebraMap ℚ A) (1 / ↑n !)

Proof state:
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
⊢ (algebraMap ℚ A) ↑(n + 1)! *
      ∑ x ∈ range (n + 1),
        (PowerSeries.coeff A x) (PowerSeries.mk fun n => (aeval t) ((1 / ↑n !) • bernoulli n)) *
          (PowerSeries.coeff A (n + 1 - x)) (exp A - 1) =
    (algebraMap ℚ A) ↑(n + 1)! * (t ^ n * (algebraMap ℚ A) (1 / ↑n !))

Tactic:
rw [mul_left_comm, ← RingHom.map_mul]

Result:
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
⊢ (algebraMap ℚ A) ↑(n + 1)! *
      ∑ x ∈ range (n + 1),
        (PowerSeries.coeff A x) (PowerSeries.mk fun n => (aeval t) ((1 / ↑n !) • bernoulli n)) *
          (PowerSeries.coeff A (n + 1 - x)) (exp A - 1) =
    t ^ n * (algebraMap ℚ A) (↑(n + 1)! * (1 / ↑n !))

Proof state:
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
⊢ ∑ x ∈ range (n + 1),
      (PowerSeries.coeff A x) (PowerSeries.mk fun n => (aeval t) ((1 / ↑n !) • bernoulli n)) *
        (PowerSeries.coeff A (n + 1 - x)) (exp A - 1) =
    t ^ n * (algebraMap ℚ A) (1 / ↑n !)

Tactic:
have hnp1 : IsUnit ((n + 1)! : ℚ) := IsUnit.mk0 _ (mod_cast factorial_ne_zero (n + 1))

Result:
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
⊢ ∑ x ∈ range (n + 1),
      (PowerSeries.coeff A x) (PowerSeries.mk fun n => (aeval t) ((1 / ↑n !) • bernoulli n)) *
        (PowerSeries.coeff A (n + 1 - x)) (exp A - 1) =
    t ^ n * (algebraMap ℚ A) (1 / ↑n !)