A : Type ?u.472720
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : PowerSeries ℚ := PowerSeries.mk fun n => bernoulli' n / ↑n !
⊢ bernoulli' n = 0
A : Type ?u.472720
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h_odd : Odd n
hlt : 1 < n
⊢ bernoulli' n = 0
let B := mk fun n => bernoulli' n / (n ! : ℚ)
A : Type ?u.472720
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : PowerSeries ℚ := PowerSeries.mk fun n => bernoulli' n / ↑n !
h : B * (exp ℚ - 1) = X * exp ℚ
⊢ (B - ↑evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
A : Type ?u.472720
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : PowerSeries ℚ := PowerSeries.mk fun n => bernoulli' n / ↑n !
⊢ (B - ↑evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
have h : B * (exp ℚ - 1) = X * exp ℚ := by
  simpa [bernoulli'PowerSeries] using bernoulli'PowerSeries_mul_exp_sub_one ℚ
A : Type ?u.472720
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : PowerSeries ℚ := PowerSeries.mk fun n => bernoulli' n / ↑n !
h : B * (exp ℚ - 1) = X * exp ℚ
⊢ ↑evalNegHom B * (1 - exp ℚ) = -(X * 1)
A : Type ?u.472720
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : PowerSeries ℚ := PowerSeries.mk fun n => bernoulli' n / ↑n !
h : B * (exp ℚ - 1) = X * exp ℚ
⊢ (B - ↑evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
rw [sub_mul, h, mul_sub X, sub_right_inj, ← neg_sub, mul_neg, neg_eq_iff_eq_neg]
A : Type ?u.472720
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : PowerSeries ℚ := PowerSeries.mk fun n => bernoulli' n / ↑n !
h : B * (exp ℚ - 1) = X * exp ℚ
⊢ ↑evalNegHom (B * (exp ℚ - 1)) * exp ℚ = ↑evalNegHom (X * exp ℚ) * exp ℚ
A : Type ?u.472720
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : PowerSeries ℚ := PowerSeries.mk fun n => bernoulli' n / ↑n !
h : B * (exp ℚ - 1) = X * exp ℚ
⊢ ↑evalNegHom B * (1 - exp ℚ) = -(X * 1)
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]
no goals
A : Type ?u.472720
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : PowerSeries ℚ := PowerSeries.mk fun n => bernoulli' n / ↑n !
h : B * (exp ℚ - 1) = X * exp ℚ
⊢ ↑evalNegHom (B * (exp ℚ - 1)) * exp ℚ = ↑evalNegHom (X * exp ℚ) * exp ℚ
congr
case inl
A : Type ?u.472720
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : PowerSeries ℚ := PowerSeries.mk fun n => bernoulli' n / ↑n !
this : (B - ↑evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
h :
  ∀ (n : ℕ),
    ↑(coeff ℚ n)
        ((PowerSeries.mk fun n => bernoulli' n / ↑n !) -
          ↑(rescale (-1)) (PowerSeries.mk fun n => bernoulli' n / ↑n !)) =
      if n = 1 then 1 else 0
⊢ bernoulli' n = 0

case inr
A : Type ?u.472720
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : PowerSeries ℚ := 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
A : Type ?u.472720
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : PowerSeries ℚ := PowerSeries.mk fun n => bernoulli' n / ↑n !
this : (B - ↑evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
⊢ bernoulli' n = 0
cases' mul_eq_mul_right_iff.mp this with h h <;>
  simp only [PowerSeries.ext_iff, evalNegHom, coeff_X] at h
case inl.h
A : Type ?u.472720
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : PowerSeries ℚ := PowerSeries.mk fun n => bernoulli' n / ↑n !
this : (B - ↑evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
h :
  ∀ (n : ℕ),
    ↑(coeff ℚ n)
        ((PowerSeries.mk fun n => bernoulli' n / ↑n !) -
          ↑(rescale (-1)) (PowerSeries.mk fun n => bernoulli' n / ↑n !)) =
      if n = 1 then 1 else 0
⊢ -bernoulli' n = bernoulli' n
case inl
A : Type ?u.472720
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : PowerSeries ℚ := PowerSeries.mk fun n => bernoulli' n / ↑n !
this : (B - ↑evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
h :
  ∀ (n : ℕ),
    ↑(coeff ℚ n)
        ((PowerSeries.mk fun n => bernoulli' n / ↑n !) -
          ↑(rescale (-1)) (PowerSeries.mk fun n => bernoulli' n / ↑n !)) =
      if n = 1 then 1 else 0
⊢ bernoulli' n = 0
apply eq_zero_of_neg_eq
case inl.h
A : Type ?u.472720
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : PowerSeries ℚ := PowerSeries.mk fun n => bernoulli' n / ↑n !
this : (B - ↑evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
h :
  ↑(coeff ℚ n)
      ((PowerSeries.mk fun n => bernoulli' n / ↑n !) - ↑(rescale (-1)) (PowerSeries.mk fun n => bernoulli' n / ↑n !)) =
    if n = 1 then 1 else 0
⊢ -bernoulli' n = bernoulli' n
case inl.h
A : Type ?u.472720
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : PowerSeries ℚ := PowerSeries.mk fun n => bernoulli' n / ↑n !
this : (B - ↑evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
h :
  ∀ (n : ℕ),
    ↑(coeff ℚ n)
        ((PowerSeries.mk fun n => bernoulli' n / ↑n !) -
          ↑(rescale (-1)) (PowerSeries.mk fun n => bernoulli' n / ↑n !)) =
      if n = 1 then 1 else 0
⊢ -bernoulli' n = bernoulli' n
specialize h n
no goals
case inl.h
A : Type ?u.472720
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : PowerSeries ℚ := PowerSeries.mk fun n => bernoulli' n / ↑n !
this : (B - ↑evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
h :
  ↑(coeff ℚ n)
      ((PowerSeries.mk fun n => bernoulli' n / ↑n !) - ↑(rescale (-1)) (PowerSeries.mk fun n => bernoulli' n / ↑n !)) =
    if n = 1 then 1 else 0
⊢ -bernoulli' n = bernoulli' n
split_ifs  at h <;> simp_all [h_odd.neg_one_pow, factorial_ne_zero]
no goals
case inr
A : Type ?u.472720
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : PowerSeries ℚ := 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
simpa using h 1
no goals
A : Type ?u.472720
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : PowerSeries ℚ := PowerSeries.mk fun n => bernoulli' n / ↑n !
⊢ B * (exp ℚ - 1) = X * exp ℚ
simpa [bernoulli'PowerSeries] using bernoulli'PowerSeries_mul_exp_sub_one ℚ
A : Type ?u.472720
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : PowerSeries ℚ := 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)
A : Type ?u.472720
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : PowerSeries ℚ := 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)
rw [map_mul, map_mul] at this
no goals
A : Type ?u.472720
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : PowerSeries ℚ := 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)
simpa [mul_assoc, sub_mul, mul_comm (evalNegHom (exp ℚ)), exp_mul_exp_neg_eq_one]