A : Type ?u.188932
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
this : Nat.choose 4 2 = 6
⊢ bernoulli' 4 = -1 / 30
A : Type ?u.188932
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ bernoulli' 4 = -1 / 30
have : Nat.choose 4 2 = 6 := by decide
A : Type ?u.188932
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
this : Nat.choose 4 2 = 6
⊢ 1 -
      (0 + ↑(Nat.choose 4 0) / (↑4 - ↑0 + 1) * bernoulli' 0 + ↑(Nat.choose 4 1) / (↑4 - ↑1 + 1) * bernoulli' 1 +
          ↑6 / (↑4 - ↑2 + 1) * bernoulli' 2 +
        ↑(Nat.choose 4 3) / (↑4 - ↑3 + 1) * bernoulli' 3) =
    -1 / 30
A : Type ?u.188932
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
this : Nat.choose 4 2 = 6
⊢ bernoulli' 4 = -1 / 30
rw [bernoulli'_def, sum_range_succ, sum_range_succ, sum_range_succ,
  sum_range_succ, sum_range_zero, this]
no goals
A : Type ?u.188932
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
this : Nat.choose 4 2 = 6
⊢ 1 -
      (0 + ↑(Nat.choose 4 0) / (↑4 - ↑0 + 1) * bernoulli' 0 + ↑(Nat.choose 4 1) / (↑4 - ↑1 + 1) * bernoulli' 1 +
          ↑6 / (↑4 - ↑2 + 1) * bernoulli' 2 +
        ↑(Nat.choose 4 3) / (↑4 - ↑3 + 1) * bernoulli' 3) =
    -1 / 30
norm_num
no goals
A : Type ?u.188932
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ Nat.choose 4 2 = 6
decide