no goals
n : ℕ
⊢ ↑(succ n) • bernoulli n = ↑(monomial n) ↑(succ n) - ∑ k in range n, ↑(Nat.choose (n + 1) k) • bernoulli k
rw [Nat.cast_succ, ← sum_bernoulli n, sum_range_succ, add_sub_cancel', choose_succ_self_right,
  Nat.cast_succ]