-- Mathlib/NumberTheory/Bernoulli.lean
theorem bernoulliPowerSeries_mul_exp_sub_one : bernoulliPowerSeries A * (exp A - 1) = X

Proof state:
case h.succ.succ.h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if n.succ = 0 then 1 else 0) = 0
x : ℕ × ℕ
h : x.1 + x.2 = n.succ
⊢ ↑x.2! * (↑x.2 + 1) = (↑x.2 + 1) * ↑x.2! ∨ (x.1 + x.2)! = 0

Tactic:
left

Result:
case h.succ.succ.h.h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if n.succ = 0 then 1 else 0) = 0
x : ℕ × ℕ
h : x.1 + x.2 = n.succ
⊢ ↑x.2! * (↑x.2 + 1) = (↑x.2 + 1) * ↑x.2!

Proof state:
case h.succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if n.succ = 0 then 1 else 0) = 0
⊢ (algebraMap ℚ A) (∑ x ∈ antidiagonal (n + 1), bernoulli x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹) =
    (algebraMap ℚ A) (∑ i ∈ antidiagonal n.succ, ↑((i.1 + i.2).choose i.2) / (↑i.2 + 1) * bernoulli i.1 / ↑n.succ !)

Tactic:
refine congr_arg (algebraMap ℚ A) (sum_congr rfl fun x h => eq_div_of_mul_eq (hfact n.succ) ?_)

Result:
case h.succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if n.succ = 0 then 1 else 0) = 0
x : ℕ × ℕ
h : x ∈ antidiagonal n.succ
⊢ bernoulli x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹ * ↑n.succ ! = ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli x.1

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

Tactic:
cases n with | zero => simp | succ n =>
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, if_false, _root_.inv_one, zero_add, one_ne_zero,
  mul_zero, and_false, sub_self, ← RingHom.map_mul, ← map_sum]
cases n with | zero => simp | succ n =>
rw [if_neg n.succ_succ_ne_one]
have hfact : ∀ m, (m ! : ℚ) ≠ 0 := fun m => mod_cast factorial_ne_zero m
have hite2 : ite (n.succ = 0) 1 0 = (0 : ℚ) := if_neg n.succ_ne_zero
simp only [CharP.cast_eq_zero, zero_add, inv_one, map_one, sub_self, mul_zero, add_eq]
rw [← map_zero (algebraMap ℚ A), ← zero_div (n.succ ! : ℚ), ← hite2, ← bernoulli_spec', sum_div]
refine congr_arg (algebraMap ℚ A) (sum_congr rfl fun x h => eq_div_of_mul_eq (hfact n.succ) ?_)
rw [mem_antidiagonal] at h
rw [← h, add_choose, cast_div_charZero (factorial_mul_factorial_dvd_factorial_add _ _)]
field_simp [hfact x.1, mul_comm _ (bernoulli x.1), mul_assoc]
left; left; ring

Result:
no goals

Proof state:
case h.succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if n.succ = 0 then 1 else 0) = 0
⊢ (algebraMap ℚ A) (∑ x ∈ antidiagonal (n + 1), bernoulli x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹) = 0

Tactic:
rw [← map_zero (algebraMap ℚ A), ← zero_div (n.succ ! : ℚ), ← hite2, ← bernoulli_spec', sum_div]

Result:
case h.succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if n.succ = 0 then 1 else 0) = 0
⊢ (algebraMap ℚ A) (∑ x ∈ antidiagonal (n + 1), bernoulli x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹) =
    (algebraMap ℚ A) (∑ i ∈ antidiagonal n.succ, ↑((i.1 + i.2).choose i.2) / (↑i.2 + 1) * bernoulli i.1 / ↑n.succ !)

Proof state:
case h.succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if n.succ = 0 then 1 else 0) = 0
x : ℕ × ℕ
h : x.1 + x.2 = n.succ
⊢ bernoulli x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹ * ↑n.succ ! = ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli x.1

Tactic:
rw [← h, add_choose, cast_div_charZero (factorial_mul_factorial_dvd_factorial_add _ _)]

Result:
case h.succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if n.succ = 0 then 1 else 0) = 0
x : ℕ × ℕ
h : x.1 + x.2 = n.succ
⊢ bernoulli x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹ * ↑(x.1 + x.2)! =
    ↑(x.1 + x.2)! / ↑(x.1! * x.2!) / (↑x.2 + 1) * bernoulli x.1

Proof state:
case h.succ.zero
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ (algebraMap ℚ A) (bernoulli (0 + 1) / ((↑0 + 1) * ↑0!)) * ((algebraMap ℚ A) (↑0 + 1)⁻¹ - 1) +
      (algebraMap ℚ A) (∑ x ∈ antidiagonal 0, bernoulli x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹) =
    if 0 + 1 = 1 then 1 else 0

Tactic:
simp

Result:
no goals

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

Tactic:
ext n

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

Proof state:
case h.zero
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ (coeff A 0) (bernoulliPowerSeries A * (exp A - 1)) = (coeff A 0) X

Tactic:
simp

Result:
no goals

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

Tactic:
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, if_false, _root_.inv_one, zero_add, one_ne_zero,
  mul_zero, and_false, sub_self, ← RingHom.map_mul, ← map_sum]

Result:
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ (algebraMap ℚ A) (bernoulli (n + 1) / ((↑n + 1) * ↑n !)) * ((algebraMap ℚ A) (↑0 + 1)⁻¹ - 1) +
      (algebraMap ℚ A) (∑ x ∈ antidiagonal n, bernoulli x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹) =
    if n + 1 = 1 then 1 else 0

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

Tactic:
have hfact : ∀ m, (m ! : ℚ) ≠ 0 := fun m => mod_cast factorial_ne_zero m

Result:
case h.succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
⊢ (algebraMap ℚ A) (bernoulli (n + 1 + 1) / ((↑(n + 1) + 1) * ↑(n + 1)!)) * ((algebraMap ℚ A) (↑0 + 1)⁻¹ - 1) +
      (algebraMap ℚ A) (∑ x ∈ antidiagonal (n + 1), bernoulli x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹) =
    0

Proof state:
case h.succ.succ.h.h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if n.succ = 0 then 1 else 0) = 0
x : ℕ × ℕ
h : x.1 + x.2 = n.succ
⊢ ↑x.2! * (↑x.2 + 1) = (↑x.2 + 1) * ↑x.2!

Tactic:
ring

Result:
no goals

Proof state:
case h.succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if n.succ = 0 then 1 else 0) = 0
x : ℕ × ℕ
h : x ∈ antidiagonal n.succ
⊢ bernoulli x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹ * ↑n.succ ! = ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli x.1

Tactic:
rw [mem_antidiagonal] at h

Result:
case h.succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if n.succ = 0 then 1 else 0) = 0
x : ℕ × ℕ
h : x.1 + x.2 = n.succ
⊢ bernoulli x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹ * ↑n.succ ! = ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli x.1