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)
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ bernoulli'PowerSeries A * (exp A - 1) = X * exp A
ext n
case h.zero
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ ↑(coeff A zero) (bernoulli'PowerSeries A * (exp A - 1)) = ↑(coeff A zero) (X * exp A)

case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ↑(coeff A (succ n)) (bernoulli'PowerSeries A * (exp A - 1)) = ↑(coeff A (succ n)) (X * exp A)
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)
cases' n with n
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ↑(coeff A (n + 1, 0).fst) (PowerSeries.mk fun n => ↑(algebraMap ℚ A) (bernoulli' n / ↑n !)) *
        ↑(coeff A (n + 1, 0).snd) (exp A - 1) +
      ∑ p in antidiagonal n,
        ↑(coeff A (p.fst, p.snd + 1).fst) (PowerSeries.mk fun n => ↑(algebraMap ℚ A) (bernoulli' n / ↑n !)) *
          ↑(coeff A (p.fst, p.snd + 1).snd) (exp A - 1) =
    ↑(coeff A (succ n)) (exp A * X)
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ↑(coeff A (succ n)) (bernoulli'PowerSeries A * (exp A - 1)) = ↑(coeff A (succ n)) (X * exp A)
rw [bernoulli'PowerSeries, coeff_mul, mul_comm X, sum_antidiagonal_succ']
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ p in antidiagonal n, bernoulli' p.fst / ↑p.fst ! * ((↑p.snd + 1) * ↑p.snd !)⁻¹ = (↑n !)⁻¹
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ↑(coeff A (n + 1, 0).fst) (PowerSeries.mk fun n => ↑(algebraMap ℚ A) (bernoulli' n / ↑n !)) *
        ↑(coeff A (n + 1, 0).snd) (exp A - 1) +
      ∑ p in antidiagonal n,
        ↑(coeff A (p.fst, p.snd + 1).fst) (PowerSeries.mk fun n => ↑(algebraMap ℚ A) (bernoulli' n / ↑n !)) *
          ↑(coeff A (p.fst, p.snd + 1).snd) (exp A - 1) =
    ↑(coeff A (succ n)) (exp A * X)
suffices (∑ p in antidiagonal n,
    bernoulli' p.1 / p.1! * ((p.2 + 1) * p.2! : ℚ)⁻¹) = (n ! : ℚ)⁻¹ by
  simpa [map_sum] using congr_arg (algebraMap ℚ A) this
case h.succ.h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ (∑ p in antidiagonal n, bernoulli' p.fst / ↑p.fst ! * ((↑p.snd + 1) * ↑p.snd !)⁻¹) * ↑n ! = 1
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ p in antidiagonal n, bernoulli' p.fst / ↑p.fst ! * ((↑p.snd + 1) * ↑p.snd !)⁻¹ = (↑n !)⁻¹
apply eq_inv_of_mul_eq_one_left
case h.succ.h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ x in antidiagonal n, bernoulli' x.fst / ↑x.fst ! * ((↑x.snd + 1) * ↑x.snd !)⁻¹ * ↑n ! = 1
case h.succ.h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ (∑ p in antidiagonal n, bernoulli' p.fst / ↑p.fst ! * ((↑p.snd + 1) * ↑p.snd !)⁻¹) * ↑n ! = 1
rw [sum_mul]
case h.e'_2
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ x in antidiagonal n, bernoulli' x.fst / ↑x.fst ! * ((↑x.snd + 1) * ↑x.snd !)⁻¹ * ↑n ! =
    ∑ k in antidiagonal n, ↑(Nat.choose (k.fst + k.snd) k.snd) / (↑k.snd + 1) * bernoulli' k.fst
case h.succ.h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ x in antidiagonal n, bernoulli' x.fst / ↑x.fst ! * ((↑x.snd + 1) * ↑x.snd !)⁻¹ * ↑n ! = 1
convert bernoulli'_spec' n using 1
case h.e'_2
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∀ (x : ℕ × ℕ),
    x ∈ antidiagonal n →
      bernoulli' x.fst / ↑x.fst ! * ((↑x.snd + 1) * ↑x.snd !)⁻¹ * ↑n ! =
        ↑(Nat.choose (x.fst + x.snd) x.snd) / (↑x.snd + 1) * bernoulli' x.fst
case h.e'_2
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ x in antidiagonal n, bernoulli' x.fst / ↑x.fst ! * ((↑x.snd + 1) * ↑x.snd !)⁻¹ * ↑n ! =
    ∑ k in antidiagonal n, ↑(Nat.choose (k.fst + k.snd) k.snd) / (↑k.snd + 1) * bernoulli' k.fst
apply sum_congr rfl
case h.e'_2
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∀ (x : ℕ × ℕ),
    x.fst + x.snd = n →
      bernoulli' x.fst / ↑x.fst ! * ((↑x.snd + 1) * ↑x.snd !)⁻¹ * ↑n ! =
        ↑(Nat.choose (x.fst + x.snd) x.snd) / (↑x.snd + 1) * bernoulli' x.fst
case h.e'_2
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∀ (x : ℕ × ℕ),
    x ∈ antidiagonal n →
      bernoulli' x.fst / ↑x.fst ! * ((↑x.snd + 1) * ↑x.snd !)⁻¹ * ↑n ! =
        ↑(Nat.choose (x.fst + x.snd) x.snd) / (↑x.snd + 1) * bernoulli' x.fst
simp_rw [mem_antidiagonal]
case h.e'_2.mk
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
i j : ℕ
⊢ bernoulli' (i, j).fst / ↑(i, j).fst ! * ((↑(i, j).snd + 1) * ↑(i, j).snd !)⁻¹ * ↑((i, j).fst + (i, j).snd)! =
    ↑(Nat.choose ((i, j).fst + (i, j).snd) (i, j).snd) / (↑(i, j).snd + 1) * bernoulli' (i, j).fst
case h.e'_2
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∀ (x : ℕ × ℕ),
    x.fst + x.snd = n →
      bernoulli' x.fst / ↑x.fst ! * ((↑x.snd + 1) * ↑x.snd !)⁻¹ * ↑n ! =
        ↑(Nat.choose (x.fst + x.snd) x.snd) / (↑x.snd + 1) * bernoulli' x.fst
rintro ⟨i, j⟩ rfl
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).fst / ↑(i, j).fst ! * ((↑(i, j).snd + 1) * ↑(i, j).snd !)⁻¹ * ↑((i, j).fst + (i, j).snd)! =
    ↑(Nat.choose ((i, j).fst + (i, j).snd) (i, j).snd) / (↑(i, j).snd + 1) * bernoulli' (i, j).fst
case h.e'_2.mk
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
i j : ℕ
⊢ bernoulli' (i, j).fst / ↑(i, j).fst ! * ((↑(i, j).snd + 1) * ↑(i, j).snd !)⁻¹ * ↑((i, j).fst + (i, j).snd)! =
    ↑(Nat.choose ((i, j).fst + (i, j).snd) (i, j).snd) / (↑(i, j).snd + 1) * bernoulli' (i, j).fst
have := factorial_mul_factorial_dvd_factorial_add i j
case h.e'_2.mk
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
i j : ℕ
this : i ! * j ! ∣ (i + j)!
⊢ bernoulli' i * ↑(i + j)! / (↑i ! * ((↑j + 1) * ↑j !)) = bernoulli' i * ↑(i + j)! / (↑i ! * (↑j ! * (↑j + 1)))
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).fst / ↑(i, j).fst ! * ((↑(i, j).snd + 1) * ↑(i, j).snd !)⁻¹ * ↑((i, j).fst + (i, j).snd)! =
    ↑(Nat.choose ((i, j).fst + (i, j).snd) (i, j).snd) / (↑(i, j).snd + 1) * bernoulli' (i, j).fst
field_simp [mul_comm _ (bernoulli' i), mul_assoc, add_choose]
case h.e'_2.mk
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
i j : ℕ
this : i ! * j ! ∣ (i + j)!
⊢ bernoulli' i * ↑(i + j)! / ↑(i ! * ((j + 1) * j !)) = bernoulli' i * ↑(i + j)! / ↑(i ! * (j ! * (j + 1)))
case h.e'_2.mk
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
i j : ℕ
this : i ! * j ! ∣ (i + j)!
⊢ bernoulli' i * ↑(i + j)! / (↑i ! * ((↑j + 1) * ↑j !)) = bernoulli' i * ↑(i + j)! / (↑i ! * (↑j ! * (↑j + 1)))
norm_cast
no goals
case h.e'_2.mk
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
i j : ℕ
this : i ! * j ! ∣ (i + j)!
⊢ bernoulli' i * ↑(i + j)! / ↑(i ! * ((j + 1) * j !)) = bernoulli' i * ↑(i + j)! / ↑(i ! * (j ! * (j + 1)))
rw [mul_comm (j + 1), mul_div_assoc, ← mul_assoc]
no goals
case h.zero
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ ↑(coeff A zero) (bernoulli'PowerSeries A * (exp A - 1)) = ↑(coeff A zero) (X * exp A)
simp
no goals
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
this : ∑ p in antidiagonal n, bernoulli' p.fst / ↑p.fst ! * ((↑p.snd + 1) * ↑p.snd !)⁻¹ = (↑n !)⁻¹
⊢ ↑(coeff A (n + 1, 0).fst) (PowerSeries.mk fun n => ↑(algebraMap ℚ A) (bernoulli' n / ↑n !)) *
        ↑(coeff A (n + 1, 0).snd) (exp A - 1) +
      ∑ p in antidiagonal n,
        ↑(coeff A (p.fst, p.snd + 1).fst) (PowerSeries.mk fun n => ↑(algebraMap ℚ A) (bernoulli' n / ↑n !)) *
          ↑(coeff A (p.fst, p.snd + 1).snd) (exp A - 1) =
    ↑(coeff A (succ n)) (exp A * X)
simpa [map_sum] using congr_arg (algebraMap ℚ A) this