-- Mathlib/NumberTheory/Bernoulli.lean
theorem bernoulli'PowerSeries_mul_exp_sub_one :
    bernoulli'PowerSeries A * (exp A - 1) = X * exp A

Proof state:
case h.e'_2
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ i ∈ antidiagonal n, bernoulli' i.1 / ↑i.1! * ((↑i.2 + 1) * ↑i.2!)⁻¹ * ↑n ! =
    ∑ k ∈ antidiagonal n, ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli' k.1

Tactic:
apply sum_congr rfl

Result:
case h.e'_2
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∀ x ∈ antidiagonal n,
    bernoulli' x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹ * ↑n ! = ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli' x.1

Proof state:
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ (coeff A (n + 1, 0).1) (PowerSeries.mk fun n => (algebraMap ℚ A) (bernoulli' n / ↑n !)) *
        (coeff A (n + 1, 0).2) (exp A - 1) +
      ∑ p ∈ antidiagonal n,
        (coeff A (p.1, p.2 + 1).1) (PowerSeries.mk fun n => (algebraMap ℚ A) (bernoulli' n / ↑n !)) *
          (coeff A (p.1, p.2 + 1).2) (exp A - 1) =
    (coeff A (n + 1)) (exp A * X)

Tactic:
suffices (∑ p ∈ antidiagonal n,
    bernoulli' p.1 / p.1! * ((p.2 + 1) * p.2! : ℚ)⁻¹) = (n ! : ℚ)⁻¹ by
  simpa [map_sum, Nat.factorial] using congr_arg (algebraMap ℚ A) this

Result:
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ p ∈ antidiagonal n, bernoulli' p.1 / ↑p.1! * ((↑p.2 + 1) * ↑p.2!)⁻¹ = (↑n !)⁻¹

Proof state:
case h.succ.h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ i ∈ antidiagonal n, bernoulli' i.1 / ↑i.1! * ((↑i.2 + 1) * ↑i.2!)⁻¹ * ↑n ! = 1

Tactic:
convert bernoulli'_spec' n using 1

Result:
case h.e'_2
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ i ∈ antidiagonal n, bernoulli' i.1 / ↑i.1! * ((↑i.2 + 1) * ↑i.2!)⁻¹ * ↑n ! =
    ∑ k ∈ antidiagonal n, ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli' k.1

Proof state:
case h.e'_2.mk
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
i j : ℕ
this : i ! * j ! ∣ (i + j)!
⊢ bernoulli' (i, j).1 / ↑(i, j).1! * ((↑(i, j).2 + 1) * ↑(i, j).2!)⁻¹ * ↑((i, j).1 + (i, j).2)! =
    ↑(((i, j).1 + (i, j).2).choose (i, j).2) / (↑(i, j).2 + 1) * bernoulli' (i, j).1

Tactic:
field_simp [mul_comm _ (bernoulli' i), mul_assoc, add_choose]

Result:
case h.e'_2.mk
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
i j : ℕ
this : i ! * j ! ∣ (i + j)!
⊢ ((↑j ! * (↑j + 1) = (↑j + 1) * ↑j ! ∨ i ! = 0) ∨ (i + j)! = 0) ∨ bernoulli' i = 0

Proof state:
case h.e'_2.mk
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
i j : ℕ
⊢ bernoulli' (i, j).1 / ↑(i, j).1! * ((↑(i, j).2 + 1) * ↑(i, j).2!)⁻¹ * ↑((i, j).1 + (i, j).2)! =
    ↑(((i, j).1 + (i, j).2).choose (i, j).2) / (↑(i, j).2 + 1) * bernoulli' (i, j).1

Tactic:
have := factorial_mul_factorial_dvd_factorial_add i j

Result:
case h.e'_2.mk
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
i j : ℕ
this : i ! * j ! ∣ (i + j)!
⊢ bernoulli' (i, j).1 / ↑(i, j).1! * ((↑(i, j).2 + 1) * ↑(i, j).2!)⁻¹ * ↑((i, j).1 + (i, j).2)! =
    ↑(((i, j).1 + (i, j).2).choose (i, j).2) / (↑(i, j).2 + 1) * bernoulli' (i, j).1

Proof state:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
this : ∑ p ∈ antidiagonal n, bernoulli' p.1 / ↑p.1! * ((↑p.2 + 1) * ↑p.2!)⁻¹ = (↑n !)⁻¹
⊢ (coeff A (n + 1, 0).1) (PowerSeries.mk fun n => (algebraMap ℚ A) (bernoulli' n / ↑n !)) *
        (coeff A (n + 1, 0).2) (exp A - 1) +
      ∑ p ∈ antidiagonal n,
        (coeff A (p.1, p.2 + 1).1) (PowerSeries.mk fun n => (algebraMap ℚ A) (bernoulli' n / ↑n !)) *
          (coeff A (p.1, p.2 + 1).2) (exp A - 1) =
    (coeff A (n + 1)) (exp A * X)

Tactic:
simpa [map_sum, Nat.factorial] using congr_arg (algebraMap ℚ A) this

Result:
no goals

Proof state:
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ (coeff A (n + 1)) (bernoulli'PowerSeries A * (exp A - 1)) = (coeff A (n + 1)) (X * exp A)

Tactic:
rw [bernoulli'PowerSeries, coeff_mul, mul_comm X, sum_antidiagonal_succ']

Result:
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ (coeff A (n + 1, 0).1) (PowerSeries.mk fun n => (algebraMap ℚ A) (bernoulli' n / ↑n !)) *
        (coeff A (n + 1, 0).2) (exp A - 1) +
      ∑ p ∈ antidiagonal n,
        (coeff A (p.1, p.2 + 1).1) (PowerSeries.mk fun n => (algebraMap ℚ A) (bernoulli' n / ↑n !)) *
          (coeff A (p.1, p.2 + 1).2) (exp A - 1) =
    (coeff A (n + 1)) (exp A * X)

Proof state:
case h.succ.h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ (∑ p ∈ antidiagonal n, bernoulli' p.1 / ↑p.1! * ((↑p.2 + 1) * ↑p.2!)⁻¹) * ↑n ! = 1

Tactic:
rw [sum_mul]

Result:
case h.succ.h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ i ∈ antidiagonal n, bernoulli' i.1 / ↑i.1! * ((↑i.2 + 1) * ↑i.2!)⁻¹ * ↑n ! = 1

Proof state:
case h.e'_2
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∀ x ∈ antidiagonal n,
    bernoulli' x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹ * ↑n ! = ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli' x.1

Tactic:
simp_rw [mem_antidiagonal]

Result:
case h.e'_2
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∀ (x : ℕ × ℕ),
    x.1 + x.2 = n →
      bernoulli' x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹ * ↑n ! = ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli' x.1

Proof state:
case h.e'_2
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∀ (x : ℕ × ℕ),
    x.1 + x.2 = n →
      bernoulli' x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹ * ↑n ! = ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli' x.1

Tactic:
rintro ⟨i, j⟩ rfl

Result:
case h.e'_2.mk
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
i j : ℕ
⊢ bernoulli' (i, j).1 / ↑(i, j).1! * ((↑(i, j).2 + 1) * ↑(i, j).2!)⁻¹ * ↑((i, j).1 + (i, j).2)! =
    ↑(((i, j).1 + (i, j).2).choose (i, j).2) / (↑(i, j).2 + 1) * bernoulli' (i, j).1

Proof state:
case h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ (coeff A n) (bernoulli'PowerSeries A * (exp A - 1)) = (coeff A n) (X * exp A)

Tactic:
cases n with | zero => simp | succ n =>
rw [bernoulli'PowerSeries, coeff_mul, mul_comm X, sum_antidiagonal_succ']
suffices (∑ p ∈ antidiagonal n,
    bernoulli' p.1 / p.1! * ((p.2 + 1) * p.2! : ℚ)⁻¹) = (n ! : ℚ)⁻¹ by
  simpa [map_sum, Nat.factorial] using congr_arg (algebraMap ℚ A) this
apply eq_inv_of_mul_eq_one_left
rw [sum_mul]
convert bernoulli'_spec' n using 1
apply sum_congr rfl
simp_rw [mem_antidiagonal]
rintro ⟨i, j⟩ rfl
have := factorial_mul_factorial_dvd_factorial_add i j
field_simp [mul_comm _ (bernoulli' i), mul_assoc, add_choose]
norm_cast
simp [mul_comm (j + 1)]

Result:
no goals

Proof state:
case h.e'_2.mk
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
i j : ℕ
this : i ! * j ! ∣ (i + j)!
⊢ ((j ! * (j + 1) = (j + 1) * j ! ∨ i ! = 0) ∨ (i + j)! = 0) ∨ bernoulli' i = 0

Tactic:
simp [mul_comm (j + 1)]

Result:
no goals

Proof state:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ bernoulli'PowerSeries A * (exp A - 1) = X * exp A

Tactic:
ext n

Result:
case h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ (coeff A n) (bernoulli'PowerSeries A * (exp A - 1)) = (coeff A n) (X * exp A)

Proof state:
case h.e'_2.mk
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
i j : ℕ
this : i ! * j ! ∣ (i + j)!
⊢ ((↑j ! * (↑j + 1) = (↑j + 1) * ↑j ! ∨ i ! = 0) ∨ (i + j)! = 0) ∨ bernoulli' i = 0

Tactic:
norm_cast

Result:
case h.e'_2.mk
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
i j : ℕ
this : i ! * j ! ∣ (i + j)!
⊢ ((j ! * (j + 1) = (j + 1) * j ! ∨ i ! = 0) ∨ (i + j)! = 0) ∨ bernoulli' i = 0

Proof state:
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ p ∈ antidiagonal n, bernoulli' p.1 / ↑p.1! * ((↑p.2 + 1) * ↑p.2!)⁻¹ = (↑n !)⁻¹

Tactic:
apply eq_inv_of_mul_eq_one_left

Result:
case h.succ.h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ (∑ p ∈ antidiagonal n, bernoulli' p.1 / ↑p.1! * ((↑p.2 + 1) * ↑p.2!)⁻¹) * ↑n ! = 1