-- Mathlib/NumberTheory/Bernoulli.lean
theorem bernoulli'_odd_eq_zero {n : ℕ} (h_odd : Odd n) (hlt : 1 < n) : bernoulli' n = 0

Proof state:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n => bernoulli' n / ↑n !
this : (B - evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
⊢ bernoulli' n = 0

Tactic:
rcases mul_eq_mul_right_iff.mp this with h | h <;>
  simp only [PowerSeries.ext_iff, evalNegHom, coeff_X] at h

Result:
case inl
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n => bernoulli' n / ↑n !
this : (B - evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
h : ∀ (n : ℕ), (coeff ℚ n) (B - (rescale (-1)) B) = if n = 1 then 1 else 0
⊢ bernoulli' n = 0

case inr
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n => bernoulli' n / ↑n !
this : (B - evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
h : ∀ (n : ℕ), (coeff ℚ n) (exp ℚ - 1) = (coeff ℚ n) 0
⊢ bernoulli' n = 0

Proof state:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n => bernoulli' n / ↑n !
⊢ B * (exp ℚ - 1) = X * exp ℚ

Tactic:
simpa [bernoulli'PowerSeries] using bernoulli'PowerSeries_mul_exp_sub_one ℚ

Result:
no goals

Proof state:
case inl
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n => bernoulli' n / ↑n !
this : (B - evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
h : ∀ (n : ℕ), (coeff ℚ n) (B - (rescale (-1)) B) = if n = 1 then 1 else 0
⊢ bernoulli' n = 0

Tactic:
apply eq_zero_of_neg_eq

Result:
case inl.h
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n => bernoulli' n / ↑n !
this : (B - evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
h : ∀ (n : ℕ), (coeff ℚ n) (B - (rescale (-1)) B) = if n = 1 then 1 else 0
⊢ -bernoulli' n = bernoulli' n

Proof state:
case inl.h
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n => bernoulli' n / ↑n !
this : (B - evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
h : ∀ (n : ℕ), (coeff ℚ n) (B - (rescale (-1)) B) = if n = 1 then 1 else 0
⊢ -bernoulli' n = bernoulli' n

Tactic:
specialize h n

Result:
case inl.h
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n => bernoulli' n / ↑n !
this : (B - evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
h : (coeff ℚ n) (B - (rescale (-1)) B) = if n = 1 then 1 else 0
⊢ -bernoulli' n = bernoulli' n

Proof state:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n => bernoulli' n / ↑n !
h : B * (exp ℚ - 1) = X * exp ℚ
⊢ evalNegHom B * (1 - exp ℚ) = -(X * 1)

Tactic:
suffices evalNegHom (B * (exp ℚ - 1)) * exp ℚ = evalNegHom (X * exp ℚ) * exp ℚ by
  rw [map_mul, map_mul] at this simpa [mul_assoc, sub_mul, mul_comm (evalNegHom (exp ℚ)), exp_mul_exp_neg_eq_one]

Result:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n => bernoulli' n / ↑n !
h : B * (exp ℚ - 1) = X * exp ℚ
⊢ evalNegHom (B * (exp ℚ - 1)) * exp ℚ = evalNegHom (X * exp ℚ) * exp ℚ

Proof state:
case inl.h
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n => bernoulli' n / ↑n !
this : (B - evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
h : (coeff ℚ n) (B - (rescale (-1)) B) = if n = 1 then 1 else 0
⊢ -bernoulli' n = bernoulli' n

Tactic:
split_ifs at h <;> simp_all [B, h_odd.neg_one_pow, factorial_ne_zero]

Result:
no goals

Proof state:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n => bernoulli' n / ↑n !
h : B * (exp ℚ - 1) = X * exp ℚ
this : evalNegHom (B * (exp ℚ - 1)) * exp ℚ = evalNegHom (X * exp ℚ) * exp ℚ
⊢ evalNegHom B * (1 - exp ℚ) = -(X * 1)

Tactic:
rw [map_mul, map_mul] at this

Result:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n => bernoulli' n / ↑n !
h : B * (exp ℚ - 1) = X * exp ℚ
this : evalNegHom B * evalNegHom (exp ℚ - 1) * exp ℚ = evalNegHom X * evalNegHom (exp ℚ) * exp ℚ
⊢ evalNegHom B * (1 - exp ℚ) = -(X * 1)

Proof state:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n => bernoulli' n / ↑n !
⊢ (B - evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)

Tactic:
have h : B * (exp ℚ - 1) = X * exp ℚ := by
  simpa [bernoulli'PowerSeries] using bernoulli'PowerSeries_mul_exp_sub_one ℚ

Result:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n => bernoulli' n / ↑n !
h : B * (exp ℚ - 1) = X * exp ℚ
⊢ (B - evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)

Proof state:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n => bernoulli' n / ↑n !
h : B * (exp ℚ - 1) = X * exp ℚ
⊢ (B - evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)

Tactic:
rw [sub_mul, h, mul_sub X, sub_right_inj, ← neg_sub, mul_neg, neg_eq_iff_eq_neg]

Result:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n => bernoulli' n / ↑n !
h : B * (exp ℚ - 1) = X * exp ℚ
⊢ evalNegHom B * (1 - exp ℚ) = -(X * 1)

Proof state:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n => bernoulli' n / ↑n !
h : B * (exp ℚ - 1) = X * exp ℚ
this : evalNegHom B * evalNegHom (exp ℚ - 1) * exp ℚ = evalNegHom X * evalNegHom (exp ℚ) * exp ℚ
⊢ evalNegHom B * (1 - exp ℚ) = -(X * 1)

Tactic:
simpa [mul_assoc, sub_mul, mul_comm (evalNegHom (exp ℚ)), exp_mul_exp_neg_eq_one]

Result:
no goals

Proof state:
case inr
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n => bernoulli' n / ↑n !
this : (B - evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
h : ∀ (n : ℕ), (coeff ℚ n) (exp ℚ - 1) = (coeff ℚ n) 0
⊢ bernoulli' n = 0

Tactic:
simpa +decide [Nat.factorial] using h 1

Result:
no goals

Proof state:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n => bernoulli' n / ↑n !
h : B * (exp ℚ - 1) = X * exp ℚ
⊢ evalNegHom (B * (exp ℚ - 1)) * exp ℚ = evalNegHom (X * exp ℚ) * exp ℚ

Tactic:
congr

Result:
no goals

Proof state:
n : ℕ
h_odd : Odd n
hlt : 1 < n
⊢ bernoulli' n = 0

Tactic:
let B := mk fun n => bernoulli' n / (n ! : ℚ)

Result:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n => bernoulli' n / ↑n !
⊢ bernoulli' n = 0