-- Mathlib/NumberTheory/Bernoulli.lean
theorem sum_bernoulli' (n : ℕ) : (∑ k ∈ range n, (n.choose k : ℚ) * bernoulli' k) = n

Proof state:
case succ.e_a
n k : ℕ
hk : k ∈ range n
⊢ (↑n + 1) * (↑(n.choose k) / (↑n - ↑k + 1)) = ↑(n.succ.choose k)

Tactic:
have : ((n - k : ℕ) : ℚ) + 1 ≠ 0 := by norm_cast

Result:
case succ.e_a
n k : ℕ
hk : k ∈ range n
this : ↑(n - k) + 1 ≠ 0
⊢ (↑n + 1) * (↑(n.choose k) / (↑n - ↑k + 1)) = ↑(n.succ.choose k)

Proof state:
case succ
n : ℕ
⊢ (↑n + 1) * ∑ k ∈ range n, ↑(n.choose k) / (↑n - ↑k + 1) * bernoulli' k =
    ∑ x ∈ range n, ↑(n.succ.choose x) * bernoulli' x

Tactic:
simp_rw [mul_sum, ← mul_assoc]

Result:
case succ
n : ℕ
⊢ ∑ x ∈ range n, (↑n + 1) * (↑(n.choose x) / (↑n - ↑x + 1)) * bernoulli' x =
    ∑ x ∈ range n, ↑(n.succ.choose x) * bernoulli' x

Proof state:
case succ
n : ℕ
⊢ ∑ x ∈ range n, (↑n + 1) * (↑(n.choose x) / (↑n - ↑x + 1)) * bernoulli' x =
    ∑ x ∈ range n, ↑(n.succ.choose x) * bernoulli' x

Tactic:
refine sum_congr rfl fun k hk => ?_

Result:
case succ
n k : ℕ
hk : k ∈ range n
⊢ (↑n + 1) * (↑(n.choose k) / (↑n - ↑k + 1)) * bernoulli' k = ↑(n.succ.choose k) * bernoulli' k

Proof state:
n : ℕ
this :
  (↑n + 1) * ∑ k ∈ range n, ↑(n.choose k) / (↑n - ↑k + 1) * bernoulli' k =
    ∑ x ∈ range n, ↑(n.succ.choose x) * bernoulli' x
⊢ ∑ k ∈ range (n + 1), ↑((n + 1).choose k) * bernoulli' k = ↑(n + 1)

Tactic:
rw_mod_cast [sum_range_succ, bernoulli'_def, ← this, choose_succ_self_right]

Result:
n : ℕ
this :
  ↑(n + 1) * ∑ x ∈ range n, Rat.divInt (↑(n.choose x)) (Int.subNatNat n x + 1) * bernoulli' x =
    ∑ x ∈ range n, ↑(n.succ.choose x) * bernoulli' x
⊢ ↑(n + 1) * ∑ x ∈ range n, Rat.divInt (↑(n.choose x)) (Int.subNatNat n x + 1) * bernoulli' x +
      ↑(n + 1) * (1 - ∑ x ∈ range n, Rat.divInt (↑(n.choose x)) (Int.subNatNat n x + 1) * bernoulli' x) =
    ↑(n + 1)

Proof state:
case succ.e_a
n k : ℕ
hk : k ∈ range n
this : ↑(n - k) + 1 ≠ 0
⊢ ↑(n.choose k) * (↑n + 1) = ↑((n + 1).choose k) * (↑(n - k) + 1)

Tactic:
rw_mod_cast [tsub_add_eq_add_tsub (mem_range.1 hk).le, choose_mul_succ_eq]

Result:
no goals

Proof state:
case succ
n : ℕ
⊢ ∑ k ∈ range (n + 1), ↑((n + 1).choose k) * bernoulli' k = ↑(n + 1)

Tactic:
suffices
  ((n + 1 : ℚ) * ∑ k ∈ range n, ↑(n.choose k) / (n - k + 1) * bernoulli' k) =
    ∑ x ∈ range n, ↑(n.succ.choose x) * bernoulli' x by
  rw_mod_cast [sum_range_succ, bernoulli'_def, ← this, choose_succ_self_right]
  ring

Result:
case succ
n : ℕ
⊢ (↑n + 1) * ∑ k ∈ range n, ↑(n.choose k) / (↑n - ↑k + 1) * bernoulli' k =
    ∑ x ∈ range n, ↑(n.succ.choose x) * bernoulli' x

Proof state:
case succ.e_a
n k : ℕ
hk : k ∈ range n
this : ↑(n - k) + 1 ≠ 0
⊢ (↑n + 1) * (↑(n.choose k) / (↑n - ↑k + 1)) = ↑(n.succ.choose k)

Tactic:
field_simp [← cast_sub (mem_range.1 hk).le, mul_comm]

Result:
case succ.e_a
n k : ℕ
hk : k ∈ range n
this : ↑(n - k) + 1 ≠ 0
⊢ ↑(n.choose k) * (↑n + 1) = ↑((n + 1).choose k) * (↑(n - k) + 1)

Proof state:
case succ
n k : ℕ
hk : k ∈ range n
⊢ (↑n + 1) * (↑(n.choose k) / (↑n - ↑k + 1)) * bernoulli' k = ↑(n.succ.choose k) * bernoulli' k

Tactic:
congr

Result:
case succ.e_a
n k : ℕ
hk : k ∈ range n
⊢ (↑n + 1) * (↑(n.choose k) / (↑n - ↑k + 1)) = ↑(n.succ.choose k)

Proof state:
n k : ℕ
hk : k ∈ range n
⊢ ↑(n - k) + 1 ≠ 0

Tactic:
norm_cast

Result:
no goals

Proof state:
case zero

⊢ ∑ k ∈ range 0, ↑(Nat.choose 0 k) * bernoulli' k = ↑0

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
this :
  ↑(n + 1) * ∑ x ∈ range n, Rat.divInt (↑(n.choose x)) (Int.subNatNat n x + 1) * bernoulli' x =
    ∑ x ∈ range n, ↑(n.succ.choose x) * bernoulli' x
⊢ ↑(n + 1) * ∑ x ∈ range n, Rat.divInt (↑(n.choose x)) (Int.subNatNat n x + 1) * bernoulli' x +
      ↑(n + 1) * (1 - ∑ x ∈ range n, Rat.divInt (↑(n.choose x)) (Int.subNatNat n x + 1) * bernoulli' x) =
    ↑(n + 1)

Tactic:
ring

Result:
no goals

Proof state:
n : ℕ
⊢ ∑ k ∈ range n, ↑(n.choose k) * bernoulli' k = ↑n

Tactic:
cases n with | zero => simp | succ n =>
suffices
  ((n + 1 : ℚ) * ∑ k ∈ range n, ↑(n.choose k) / (n - k + 1) * bernoulli' k) =
    ∑ x ∈ range n, ↑(n.succ.choose x) * bernoulli' x by
  rw_mod_cast [sum_range_succ, bernoulli'_def, ← this, choose_succ_self_right]
  ring
simp_rw [mul_sum, ← mul_assoc]
refine sum_congr rfl fun k hk => ?_
congr
have : ((n - k : ℕ) : ℚ) + 1 ≠ 0 := by norm_cast
field_simp [← cast_sub (mem_range.1 hk).le, mul_comm]
rw_mod_cast [tsub_add_eq_add_tsub (mem_range.1 hk).le, choose_mul_succ_eq]

Result:
no goals