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

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

Tactic:
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 : ℕ
⊢ (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!)⁻¹) =
    if n + 1 + 1 = 1 then 1 else 0

Tactic:
rw [if_neg n.succ_succ_ne_one]

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

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!)⁻¹ * ↑(x.1 + x.2)! =
    ↑(x.1 + x.2)! / ↑(x.1! * x.2!) / (↑x.2 + 1) * bernoulli x.1

Tactic:
field_simp [hfact x.1, mul_comm _ (bernoulli x.1), mul_assoc]

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
⊢ (↑x.2! * (↑x.2 + 1) = (↑x.2 + 1) * ↑x.2! ∨ (x.1 + x.2)! = 0) ∨ bernoulli x.1 = 0

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) (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:
simp only [CharP.cast_eq_zero, zero_add, inv_one, map_one, sub_self, mul_zero, add_eq]

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!)⁻¹) = 0

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

Tactic:
have hite2 : ite (n.succ = 0) 1 0 = (0 : ℚ) := if_neg n.succ_ne_zero

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) (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
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) ∨ bernoulli x.1 = 0

Tactic:
left

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