A : Type ?u.176715
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ x in range n,
      (↑(Nat.choose n x) / (↑n - ↑x + 1) * bernoulli' x - ↑(Nat.choose n (n - x)) / (↑n - ↑x + 1) * bernoulli' x) =
    0
A : Type ?u.176715
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ k in range (succ n), ↑(Nat.choose n (n - k)) / (↑n - ↑k + 1) * bernoulli' k = 1
rw [sum_range_succ_comm, bernoulli'_def n, tsub_self, choose_zero_right, sub_self, zero_add,
  div_one, cast_one, one_mul, sub_add, ← sum_sub_distrib, ← sub_eq_zero, sub_sub_cancel_left,
  neg_eq_zero]
no goals
A : Type ?u.176715
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ x in range n,
      (↑(Nat.choose n x) / (↑n - ↑x + 1) * bernoulli' x - ↑(Nat.choose n (n - x)) / (↑n - ↑x + 1) * bernoulli' x) =
    0
exact Finset.sum_eq_zero (fun x hx => by rw [choose_symm (le_of_lt (mem_range.1 hx)), sub_self])
no goals
A : Type ?u.176715
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n x : ℕ
hx : x ∈ range n
⊢ ↑(Nat.choose n x) / (↑n - ↑x + 1) * bernoulli' x - ↑(Nat.choose n (n - x)) / (↑n - ↑x + 1) * bernoulli' x = 0
rw [choose_symm (le_of_lt (mem_range.1 hx)), sub_self]