case zero
A : Type ?u.191355
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ ∑ k in range zero, ↑(Nat.choose zero k) * bernoulli' k = ↑zero

case succ
A : Type ?u.191355
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ k in range (succ n), ↑(Nat.choose (succ n) k) * bernoulli' k = ↑(succ n)
A : Type ?u.191355
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ k in range n, ↑(Nat.choose n k) * bernoulli' k = ↑n
cases' n with n
case succ
A : Type ?u.191355
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ (↑n + 1) * ∑ k in range n, ↑(Nat.choose n k) / (↑n - ↑k + 1) * bernoulli' k =
    ∑ x in range n, ↑(Nat.choose (succ n) x) * bernoulli' x
case succ
A : Type ?u.191355
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ k in range (succ n), ↑(Nat.choose (succ n) k) * bernoulli' k = ↑(succ n)
suffices
  ((n + 1 : ℚ) * ∑ k in range n, ↑(n.choose k) / (n - k + 1) * bernoulli' k) =
    ∑ x in range n, ↑(n.succ.choose x) * bernoulli' x by
  rw_mod_cast [sum_range_succ, bernoulli'_def, ← this, choose_succ_self_right]
  ring
case succ
A : Type ?u.191355
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ x in range n, (↑n + 1) * (↑(Nat.choose n x) / (↑n - ↑x + 1)) * bernoulli' x =
    ∑ x in range n, ↑(Nat.choose (succ n) x) * bernoulli' x
case succ
A : Type ?u.191355
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ (↑n + 1) * ∑ k in range n, ↑(Nat.choose n k) / (↑n - ↑k + 1) * bernoulli' k =
    ∑ x in range n, ↑(Nat.choose (succ n) x) * bernoulli' x
simp_rw [mul_sum, ← mul_assoc]
case succ
A : Type ?u.191355
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n k : ℕ
hk : k ∈ range n
⊢ (↑n + 1) * (↑(Nat.choose n k) / (↑n - ↑k + 1)) * bernoulli' k = ↑(Nat.choose (succ n) k) * bernoulli' k
case succ
A : Type ?u.191355
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ x in range n, (↑n + 1) * (↑(Nat.choose n x) / (↑n - ↑x + 1)) * bernoulli' x =
    ∑ x in range n, ↑(Nat.choose (succ n) x) * bernoulli' x
refine' sum_congr rfl fun k hk => _
case succ.e_a
A : Type ?u.191355
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n k : ℕ
hk : k ∈ range n
⊢ (↑n + 1) * (↑(Nat.choose n k) / (↑n - ↑k + 1)) = ↑(Nat.choose (succ n) k)
case succ
A : Type ?u.191355
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n k : ℕ
hk : k ∈ range n
⊢ (↑n + 1) * (↑(Nat.choose n k) / (↑n - ↑k + 1)) * bernoulli' k = ↑(Nat.choose (succ n) k) * bernoulli' k
congr
case succ.e_a
A : Type ?u.191355
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n k : ℕ
hk : k ∈ range n
this : ↑(n - k) + 1 ≠ 0
⊢ (↑n + 1) * (↑(Nat.choose n k) / (↑n - ↑k + 1)) = ↑(Nat.choose (succ n) k)
case succ.e_a
A : Type ?u.191355
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n k : ℕ
hk : k ∈ range n
⊢ (↑n + 1) * (↑(Nat.choose n k) / (↑n - ↑k + 1)) = ↑(Nat.choose (succ n) k)
have : ((n - k : ℕ) : ℚ) + 1 ≠ 0 := by norm_cast; exact succ_ne_zero _
case succ.e_a
A : Type ?u.191355
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n k : ℕ
hk : k ∈ range n
this : ↑(n - k) + 1 ≠ 0
⊢ ↑(Nat.choose n k) * (↑n + 1) = ↑(Nat.choose (succ n) k) * (↑(n - k) + 1)
case succ.e_a
A : Type ?u.191355
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n k : ℕ
hk : k ∈ range n
this : ↑(n - k) + 1 ≠ 0
⊢ (↑n + 1) * (↑(Nat.choose n k) / (↑n - ↑k + 1)) = ↑(Nat.choose (succ n) k)
field_simp [← cast_sub (mem_range.1 hk).le, mul_comm]
no goals
case succ.e_a
A : Type ?u.191355
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n k : ℕ
hk : k ∈ range n
this : ↑(n - k) + 1 ≠ 0
⊢ ↑(Nat.choose n k) * (↑n + 1) = ↑(Nat.choose (succ n) k) * (↑(n - k) + 1)
rw_mod_cast [tsub_add_eq_add_tsub (mem_range.1 hk).le, choose_mul_succ_eq]
no goals
case zero
A : Type ?u.191355
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ ∑ k in range zero, ↑(Nat.choose zero k) * bernoulli' k = ↑zero
simp
A : Type ?u.191355
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
this :
  ↑(n + 1) * ∑ x in range n, Rat.divInt (↑(Nat.choose n x)) (Int.subNatNat n x + 1) * bernoulli' x =
    ∑ x in range n, ↑(Nat.choose (succ n) x) * bernoulli' x
⊢ ↑(n + 1) * ∑ x in range n, Rat.divInt (↑(Nat.choose n x)) (Int.subNatNat n x + 1) * bernoulli' x +
      ↑(n + 1) * (1 - ∑ x in range n, Rat.divInt (↑(Nat.choose n x)) (Int.subNatNat n x + 1) * bernoulli' x) =
    ↑(succ n)
A : Type ?u.191355
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
this :
  (↑n + 1) * ∑ k in range n, ↑(Nat.choose n k) / (↑n - ↑k + 1) * bernoulli' k =
    ∑ x in range n, ↑(Nat.choose (succ n) x) * bernoulli' x
⊢ ∑ k in range (succ n), ↑(Nat.choose (succ n) k) * bernoulli' k = ↑(succ n)
rw_mod_cast [sum_range_succ, bernoulli'_def, ← this, choose_succ_self_right]
no goals
A : Type ?u.191355
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
this :
  ↑(n + 1) * ∑ x in range n, Rat.divInt (↑(Nat.choose n x)) (Int.subNatNat n x + 1) * bernoulli' x =
    ∑ x in range n, ↑(Nat.choose (succ n) x) * bernoulli' x
⊢ ↑(n + 1) * ∑ x in range n, Rat.divInt (↑(Nat.choose n x)) (Int.subNatNat n x + 1) * bernoulli' x +
      ↑(n + 1) * (1 - ∑ x in range n, Rat.divInt (↑(Nat.choose n x)) (Int.subNatNat n x + 1) * bernoulli' x) =
    ↑(succ n)
ring
A : Type ?u.191355
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n k : ℕ
hk : k ∈ range n
⊢ ¬n - k + 1 = 0
A : Type ?u.191355
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n k : ℕ
hk : k ∈ range n
⊢ ↑(n - k) + 1 ≠ 0
norm_cast
no goals
A : Type ?u.191355
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n k : ℕ
hk : k ∈ range n
⊢ ¬n - k + 1 = 0
exact succ_ne_zero _