A : Type ?u.179006
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ k in range (succ n),
      ↑(Nat.choose ((k, n - k).fst + (k, n - k).snd) (k, n - k).snd) / (↑(k, n - k).snd + 1) *
        bernoulli' (k, n - k).fst =
    ∑ k in range (succ n), ↑(Nat.choose n (n - k)) / (↑n - ↑k + 1) * bernoulli' k
A : Type ?u.179006
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ k in antidiagonal n, ↑(Nat.choose (k.fst + k.snd) k.snd) / (↑k.snd + 1) * bernoulli' k.fst = 1
refine' ((sum_antidiagonal_eq_sum_range_succ_mk _ n).trans _).trans (bernoulli'_spec n)
A : Type ?u.179006
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n x : ℕ
hx : x ∈ range (succ n)
⊢ ↑(Nat.choose ((x, n - x).fst + (x, n - x).snd) (x, n - x).snd) / (↑(x, n - x).snd + 1) * bernoulli' (x, n - x).fst =
    ↑(Nat.choose n (n - x)) / (↑n - ↑x + 1) * bernoulli' x
A : Type ?u.179006
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ k in range (succ n),
      ↑(Nat.choose ((k, n - k).fst + (k, n - k).snd) (k, n - k).snd) / (↑(k, n - k).snd + 1) *
        bernoulli' (k, n - k).fst =
    ∑ k in range (succ n), ↑(Nat.choose n (n - k)) / (↑n - ↑k + 1) * bernoulli' k
refine' sum_congr rfl fun x hx => _
no goals
A : Type ?u.179006
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n x : ℕ
hx : x ∈ range (succ n)
⊢ ↑(Nat.choose ((x, n - x).fst + (x, n - x).snd) (x, n - x).snd) / (↑(x, n - x).snd + 1) * bernoulli' (x, n - x).fst =
    ↑(Nat.choose n (n - x)) / (↑n - ↑x + 1) * bernoulli' x
simp only [add_tsub_cancel_of_le, mem_range_succ_iff.mp hx, cast_sub]