-- 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 : ℕ
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)

Tactic:
apply Finset.sum_congr rfl

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),
    (algebraMap ℚ A) ↑(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) (↑((n + 1).choose x) • bernoulli x)

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) =
    t ^ n * (algebraMap ℚ A) (↑(n + 1)! * (1 / ↑n !))

Tactic:
change _ = t ^ n * algebraMap ℚ A (((n + 1) * n ! : ℕ) * (1 / n !))

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) * n !) * (1 / ↑n !))

Proof state:
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 !)

Tactic:
rw [← (hnp1.map (algebraMap ℚ A)).mul_right_inj]

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) =
    (algebraMap ℚ A) ↑(n + 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)!
⊢ ∀ x ∈ range (n + 1),
    (algebraMap ℚ A) ↑(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) (↑((n + 1).choose x) • bernoulli x)

Tactic:
intro i hi

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)! *
      ((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)

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

Tactic:
ext n

Result:
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))

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) =
    t ^ n * (algebraMap ℚ A) (↑((n + 1) * n !) * (1 / ↑n !))

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]

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) =
    (aeval t) ((monomial n) (↑n + 1))