case h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ↑(coeff A n) (bernoulliPowerSeries A * (exp A - 1)) = ↑(coeff A n) X
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ bernoulliPowerSeries A * (exp A - 1) = X
ext n
case h.zero
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ ↑(coeff A zero) (bernoulliPowerSeries A * (exp A - 1)) = ↑(coeff A zero) X

case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ↑(coeff A (succ n)) (bernoulliPowerSeries A * (exp A - 1)) = ↑(coeff A (succ n)) X
case h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ↑(coeff A n) (bernoulliPowerSeries A * (exp A - 1)) = ↑(coeff A n) X
cases' n with n n
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ↑(algebraMap ℚ A) (bernoulli (n + 1) / ((↑n + 1) * ↑(Nat.add n 0)!)) * (↑(algebraMap ℚ A) (↑0 + 1)⁻¹ - 1) +
      ↑(algebraMap ℚ A) (∑ x in antidiagonal n, bernoulli x.fst / ↑x.fst ! * ((↑x.snd + 1) * ↑(Nat.add x.snd 0)!)⁻¹) =
    if succ n = 1 then 1 else 0
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ↑(coeff A (succ n)) (bernoulliPowerSeries A * (exp A - 1)) = ↑(coeff A (succ n)) X
simp only [bernoulliPowerSeries, coeff_mul, coeff_X, sum_antidiagonal_succ', one_div, coeff_mk,
  coeff_one, coeff_exp, LinearMap.map_sub, factorial, if_pos, cast_succ, cast_one, cast_mul,
  sub_zero, RingHom.map_one, add_eq_zero_iff, if_false, _root_.inv_one, zero_add, one_ne_zero,
  MulZeroClass.mul_zero, and_false_iff, sub_self, ← RingHom.map_mul, ← map_sum]
case h.succ.zero
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ ↑(algebraMap ℚ A) (bernoulli (zero + 1) / ((↑zero + 1) * ↑(Nat.add zero 0)!)) * (↑(algebraMap ℚ A) (↑0 + 1)⁻¹ - 1) +
      ↑(algebraMap ℚ A)
        (∑ x in antidiagonal zero, bernoulli x.fst / ↑x.fst ! * ((↑x.snd + 1) * ↑(Nat.add x.snd 0)!)⁻¹) =
    if succ zero = 1 then 1 else 0

case h.succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ↑(algebraMap ℚ A) (bernoulli (succ n + 1) / ((↑(succ n) + 1) * ↑(Nat.add (succ n) 0)!)) *
        (↑(algebraMap ℚ A) (↑0 + 1)⁻¹ - 1) +
      ↑(algebraMap ℚ A)
        (∑ x in antidiagonal (succ n), bernoulli x.fst / ↑x.fst ! * ((↑x.snd + 1) * ↑(Nat.add x.snd 0)!)⁻¹) =
    if succ (succ n) = 1 then 1 else 0
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ↑(algebraMap ℚ A) (bernoulli (n + 1) / ((↑n + 1) * ↑(Nat.add n 0)!)) * (↑(algebraMap ℚ A) (↑0 + 1)⁻¹ - 1) +
      ↑(algebraMap ℚ A) (∑ x in antidiagonal n, bernoulli x.fst / ↑x.fst ! * ((↑x.snd + 1) * ↑(Nat.add x.snd 0)!)⁻¹) =
    if succ n = 1 then 1 else 0
cases' n with n
case h.succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ↑(algebraMap ℚ A) (bernoulli (succ n + 1) / ((↑(succ n) + 1) * ↑(Nat.add (succ n) 0)!)) *
        (↑(algebraMap ℚ A) (↑0 + 1)⁻¹ - 1) +
      ↑(algebraMap ℚ A)
        (∑ x in antidiagonal (succ n), bernoulli x.fst / ↑x.fst ! * ((↑x.snd + 1) * ↑(Nat.add x.snd 0)!)⁻¹) =
    0
case h.succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ↑(algebraMap ℚ A) (bernoulli (succ n + 1) / ((↑(succ n) + 1) * ↑(Nat.add (succ n) 0)!)) *
        (↑(algebraMap ℚ A) (↑0 + 1)⁻¹ - 1) +
      ↑(algebraMap ℚ A)
        (∑ x in antidiagonal (succ n), bernoulli x.fst / ↑x.fst ! * ((↑x.snd + 1) * ↑(Nat.add x.snd 0)!)⁻¹) =
    if succ (succ n) = 1 then 1 else 0
rw [if_neg n.succ_succ_ne_one]
case h.succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
⊢ ↑(algebraMap ℚ A) (bernoulli (succ n + 1) / ((↑(succ n) + 1) * ↑(Nat.add (succ n) 0)!)) *
        (↑(algebraMap ℚ A) (↑0 + 1)⁻¹ - 1) +
      ↑(algebraMap ℚ A)
        (∑ x in antidiagonal (succ n), bernoulli x.fst / ↑x.fst ! * ((↑x.snd + 1) * ↑(Nat.add x.snd 0)!)⁻¹) =
    0
case h.succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ↑(algebraMap ℚ A) (bernoulli (succ n + 1) / ((↑(succ n) + 1) * ↑(Nat.add (succ n) 0)!)) *
        (↑(algebraMap ℚ A) (↑0 + 1)⁻¹ - 1) +
      ↑(algebraMap ℚ A)
        (∑ x in antidiagonal (succ n), bernoulli x.fst / ↑x.fst ! * ((↑x.snd + 1) * ↑(Nat.add x.snd 0)!)⁻¹) =
    0
have hfact : ∀ m, (m ! : ℚ) ≠ 0 := fun m => by exact_mod_cast factorial_ne_zero m
case h.succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if succ n = 0 then 1 else 0) = 0
⊢ ↑(algebraMap ℚ A) (bernoulli (succ n + 1) / ((↑(succ n) + 1) * ↑(Nat.add (succ n) 0)!)) *
        (↑(algebraMap ℚ A) (↑0 + 1)⁻¹ - 1) +
      ↑(algebraMap ℚ A)
        (∑ x in antidiagonal (succ n), bernoulli x.fst / ↑x.fst ! * ((↑x.snd + 1) * ↑(Nat.add x.snd 0)!)⁻¹) =
    0
case h.succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
⊢ ↑(algebraMap ℚ A) (bernoulli (succ n + 1) / ((↑(succ n) + 1) * ↑(Nat.add (succ n) 0)!)) *
        (↑(algebraMap ℚ A) (↑0 + 1)⁻¹ - 1) +
      ↑(algebraMap ℚ A)
        (∑ x in antidiagonal (succ n), bernoulli x.fst / ↑x.fst ! * ((↑x.snd + 1) * ↑(Nat.add x.snd 0)!)⁻¹) =
    0
have hite2 : ite (n.succ = 0) 1 0 = (0 : ℚ) := if_neg n.succ_ne_zero
case h.succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if succ n = 0 then 1 else 0) = 0
⊢ ↑(algebraMap ℚ A) (∑ x in antidiagonal (succ n), bernoulli x.fst / ↑x.fst ! * ((↑x.snd + 1) * ↑(x.snd + 0)!)⁻¹) = 0
case h.succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if succ n = 0 then 1 else 0) = 0
⊢ ↑(algebraMap ℚ A) (bernoulli (succ n + 1) / ((↑(succ n) + 1) * ↑(Nat.add (succ n) 0)!)) *
        (↑(algebraMap ℚ A) (↑0 + 1)⁻¹ - 1) +
      ↑(algebraMap ℚ A)
        (∑ x in antidiagonal (succ n), bernoulli x.fst / ↑x.fst ! * ((↑x.snd + 1) * ↑(Nat.add x.snd 0)!)⁻¹) =
    0
simp only [CharP.cast_eq_zero, zero_add, inv_one, map_one, sub_self, mul_zero, add_eq]
case h.succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if succ n = 0 then 1 else 0) = 0
⊢ ↑(algebraMap ℚ A) (∑ x in antidiagonal (succ n), bernoulli x.fst / ↑x.fst ! * ((↑x.snd + 1) * ↑(x.snd + 0)!)⁻¹) =
    ↑(algebraMap ℚ A)
      (∑ x in antidiagonal (succ n), ↑(Nat.choose (x.fst + x.snd) x.snd) / (↑x.snd + 1) * bernoulli x.fst / ↑(succ n)!)
case h.succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if succ n = 0 then 1 else 0) = 0
⊢ ↑(algebraMap ℚ A) (∑ x in antidiagonal (succ n), bernoulli x.fst / ↑x.fst ! * ((↑x.snd + 1) * ↑(x.snd + 0)!)⁻¹) = 0
rw [← map_zero (algebraMap ℚ A), ← zero_div (n.succ ! : ℚ), ← hite2, ← bernoulli_spec', sum_div]
case h.succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if succ n = 0 then 1 else 0) = 0
x : ℕ × ℕ
h : x ∈ antidiagonal (succ n)
⊢ bernoulli x.fst / ↑x.fst ! * ((↑x.snd + 1) * ↑(x.snd + 0)!)⁻¹ * ↑(succ n)! =
    ↑(Nat.choose (x.fst + x.snd) x.snd) / (↑x.snd + 1) * bernoulli x.fst
case h.succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if succ n = 0 then 1 else 0) = 0
⊢ ↑(algebraMap ℚ A) (∑ x in antidiagonal (succ n), bernoulli x.fst / ↑x.fst ! * ((↑x.snd + 1) * ↑(x.snd + 0)!)⁻¹) =
    ↑(algebraMap ℚ A)
      (∑ x in antidiagonal (succ n), ↑(Nat.choose (x.fst + x.snd) x.snd) / (↑x.snd + 1) * bernoulli x.fst / ↑(succ n)!)
refine' congr_arg (algebraMap ℚ A) (sum_congr rfl fun x h => eq_div_of_mul_eq (hfact n.succ) _)
case h.succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if succ n = 0 then 1 else 0) = 0
x : ℕ × ℕ
h : x.fst + x.snd = succ n
⊢ bernoulli x.fst / ↑x.fst ! * ((↑x.snd + 1) * ↑(x.snd + 0)!)⁻¹ * ↑(succ n)! =
    ↑(Nat.choose (x.fst + x.snd) x.snd) / (↑x.snd + 1) * bernoulli x.fst
case h.succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if succ n = 0 then 1 else 0) = 0
x : ℕ × ℕ
h : x ∈ antidiagonal (succ n)
⊢ bernoulli x.fst / ↑x.fst ! * ((↑x.snd + 1) * ↑(x.snd + 0)!)⁻¹ * ↑(succ n)! =
    ↑(Nat.choose (x.fst + x.snd) x.snd) / (↑x.snd + 1) * bernoulli x.fst
rw [mem_antidiagonal] at h
case h.succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if succ n = 0 then 1 else 0) = 0
x : ℕ × ℕ
h : x.fst + x.snd = succ n
hj : ↑x.snd + 1 ≠ 0
⊢ bernoulli x.fst / ↑x.fst ! * ((↑x.snd + 1) * ↑(x.snd + 0)!)⁻¹ * ↑(succ n)! =
    ↑(Nat.choose (x.fst + x.snd) x.snd) / (↑x.snd + 1) * bernoulli x.fst
case h.succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if succ n = 0 then 1 else 0) = 0
x : ℕ × ℕ
h : x.fst + x.snd = succ n
⊢ bernoulli x.fst / ↑x.fst ! * ((↑x.snd + 1) * ↑(x.snd + 0)!)⁻¹ * ↑(succ n)! =
    ↑(Nat.choose (x.fst + x.snd) x.snd) / (↑x.snd + 1) * bernoulli x.fst
have hj : (x.2 + 1 : ℚ) ≠ 0 := by norm_cast; exact succ_ne_zero _
case h.succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if succ n = 0 then 1 else 0) = 0
x : ℕ × ℕ
h : x.fst + x.snd = succ n
hj : ↑x.snd + 1 ≠ 0
⊢ bernoulli x.fst / ↑x.fst ! * ((↑x.snd + 1) * ↑(x.snd + 0)!)⁻¹ * ↑(x.fst + x.snd)! =
    ↑(x.fst + x.snd)! / ↑(x.fst ! * x.snd !) / (↑x.snd + 1) * bernoulli x.fst
case h.succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if succ n = 0 then 1 else 0) = 0
x : ℕ × ℕ
h : x.fst + x.snd = succ n
hj : ↑x.snd + 1 ≠ 0
⊢ bernoulli x.fst / ↑x.fst ! * ((↑x.snd + 1) * ↑(x.snd + 0)!)⁻¹ * ↑(succ n)! =
    ↑(Nat.choose (x.fst + x.snd) x.snd) / (↑x.snd + 1) * bernoulli x.fst
rw [← h, add_choose, cast_div_charZero (factorial_mul_factorial_dvd_factorial_add _ _)]
case h.succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if succ n = 0 then 1 else 0) = 0
x : ℕ × ℕ
h : x.fst + x.snd = succ n
hj : ↑x.snd + 1 ≠ 0
⊢ ↑x.snd ! * (↑x.snd + 1) = (↑x.snd + 1) * ↑x.snd ! ∨ bernoulli x.fst = 0
case h.succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if succ n = 0 then 1 else 0) = 0
x : ℕ × ℕ
h : x.fst + x.snd = succ n
hj : ↑x.snd + 1 ≠ 0
⊢ bernoulli x.fst / ↑x.fst ! * ((↑x.snd + 1) * ↑(x.snd + 0)!)⁻¹ * ↑(x.fst + x.snd)! =
    ↑(x.fst + x.snd)! / ↑(x.fst ! * x.snd !) / (↑x.snd + 1) * bernoulli x.fst
field_simp [mul_ne_zero hj (hfact x.2), hfact x.1, mul_comm _ (bernoulli x.1), mul_assoc,
  Nat.factorial_ne_zero, hj]
case h.succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if succ n = 0 then 1 else 0) = 0
x : ℕ × ℕ
h : x.fst + x.snd = succ n
hj : ↑x.snd + 1 ≠ 0
⊢ ↑x.snd ! * (↑x.snd + 1) = (↑x.snd + 1) * ↑x.snd ! ∨ bernoulli x.fst = 0
case h.succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if succ n = 0 then 1 else 0) = 0
x : ℕ × ℕ
h : x.fst + x.snd = succ n
hj : ↑x.snd + 1 ≠ 0
⊢ ↑x.snd ! * (↑x.snd + 1) = (↑x.snd + 1) * ↑x.snd ! ∨ bernoulli x.fst = 0
simp only
case h.succ.succ.h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if succ n = 0 then 1 else 0) = 0
x : ℕ × ℕ
h : x.fst + x.snd = succ n
hj : ↑x.snd + 1 ≠ 0
⊢ ↑x.snd ! * (↑x.snd + 1) = (↑x.snd + 1) * ↑x.snd !
case h.succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if succ n = 0 then 1 else 0) = 0
x : ℕ × ℕ
h : x.fst + x.snd = succ n
hj : ↑x.snd + 1 ≠ 0
⊢ ↑x.snd ! * (↑x.snd + 1) = (↑x.snd + 1) * ↑x.snd ! ∨ bernoulli x.fst = 0
left
no goals
case h.succ.succ.h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if succ n = 0 then 1 else 0) = 0
x : ℕ × ℕ
h : x.fst + x.snd = succ n
hj : ↑x.snd + 1 ≠ 0
⊢ ↑x.snd ! * (↑x.snd + 1) = (↑x.snd + 1) * ↑x.snd !
ring
no goals
case h.zero
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ ↑(coeff A zero) (bernoulliPowerSeries A * (exp A - 1)) = ↑(coeff A zero) X
simp
no goals
case h.succ.zero
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ ↑(algebraMap ℚ A) (bernoulli (zero + 1) / ((↑zero + 1) * ↑(Nat.add zero 0)!)) * (↑(algebraMap ℚ A) (↑0 + 1)⁻¹ - 1) +
      ↑(algebraMap ℚ A)
        (∑ x in antidiagonal zero, bernoulli x.fst / ↑x.fst ! * ((↑x.snd + 1) * ↑(Nat.add x.snd 0)!)⁻¹) =
    if succ zero = 1 then 1 else 0
simp
no goals
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n m : ℕ
⊢ ↑m ! ≠ 0
exact_mod_cast factorial_ne_zero m
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if succ n = 0 then 1 else 0) = 0
x : ℕ × ℕ
h : x.fst + x.snd = succ n
⊢ ¬x.snd + 1 = 0
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if succ n = 0 then 1 else 0) = 0
x : ℕ × ℕ
h : x.fst + x.snd = succ n
⊢ ↑x.snd + 1 ≠ 0
norm_cast
no goals
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if succ n = 0 then 1 else 0) = 0
x : ℕ × ℕ
h : x.fst + x.snd = succ n
⊢ ¬x.snd + 1 = 0
exact succ_ne_zero _