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

Proof state:
case succ.succ.refine_1.e_f
n : ℕ
f :
  ∑ k ∈ range n, ↑(n.succ.succ.choose (k + 1 + 1)) * bernoulli' (k + 1 + 1) =
    ↑n + 1 + 1 - ↑(n.succ.succ.choose 0) * bernoulli' 0 - ↑(n.succ.succ.choose (0 + 1)) * bernoulli' (0 + 1)
⊢ (fun i => ↑((n + 2).choose (i + 2)) * bernoulli (i + 2)) = fun k =>
    ↑(n.succ.succ.choose (k + 1 + 1)) * bernoulli' (k + 1 + 1)

Tactic:
funext x

Result:
case succ.succ.refine_1.e_f.h
n : ℕ
f :
  ∑ k ∈ range n, ↑(n.succ.succ.choose (k + 1 + 1)) * bernoulli' (k + 1 + 1) =
    ↑n + 1 + 1 - ↑(n.succ.succ.choose 0) * bernoulli' 0 - ↑(n.succ.succ.choose (0 + 1)) * bernoulli' (0 + 1)
x : ℕ
⊢ ↑((n + 2).choose (x + 2)) * bernoulli (x + 2) = ↑(n.succ.succ.choose (x + 1 + 1)) * bernoulli' (x + 1 + 1)

Proof state:
n : ℕ
this : ∑ i ∈ range n, ↑((n + 2).choose (i + 2)) * bernoulli (i + 2) = ↑n / 2
⊢ ∑ k ∈ range (n + 1 + 1), ↑((n + 1 + 1).choose k) * bernoulli k = if n + 1 + 1 = 1 then 1 else 0

Tactic:
simp only [this, sum_range_succ', cast_succ, bernoulli_one, bernoulli_zero, choose_one_right,
  mul_one, choose_zero_right, cast_zero, if_false, zero_add, succ_succ_ne_one]

Result:
n : ℕ
this : ∑ i ∈ range n, ↑((n + 2).choose (i + 2)) * bernoulli (i + 2) = ↑n / 2
⊢ ↑n / 2 + (↑n + 1 + 1) * (-1 / 2) + 1 = 0

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

Tactic:
suffices (∑ i ∈ range n, ↑((n + 2).choose (i + 2)) * bernoulli (i + 2)) = n / 2 by
  simp only [this, sum_range_succ', cast_succ, bernoulli_one, bernoulli_zero, choose_one_right,
    mul_one, choose_zero_right, cast_zero, if_false, zero_add, succ_succ_ne_one]
  ring

Result:
case succ.succ
n : ℕ
⊢ ∑ i ∈ range n, ↑((n + 2).choose (i + 2)) * bernoulli (i + 2) = ↑n / 2

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

Tactic:
simp_rw [sum_range_succ', cast_succ, ← eq_sub_iff_add_eq] at f

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

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

Tactic:
refine Eq.trans ?_ (Eq.trans f ?_)

Result:
case succ.succ.refine_1
n : ℕ
f :
  ∑ k ∈ range n, ↑(n.succ.succ.choose (k + 1 + 1)) * bernoulli' (k + 1 + 1) =
    ↑n + 1 + 1 - ↑(n.succ.succ.choose 0) * bernoulli' 0 - ↑(n.succ.succ.choose (0 + 1)) * bernoulli' (0 + 1)
⊢ ∑ i ∈ range n, ↑((n + 2).choose (i + 2)) * bernoulli (i + 2) =
    ∑ k ∈ range n, ↑(n.succ.succ.choose (k + 1 + 1)) * bernoulli' (k + 1 + 1)

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

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

Tactic:
simp only [one_div, mul_one, bernoulli'_zero, cast_one, choose_zero_right, add_sub_cancel_right,
  zero_add, choose_one_right, cast_succ, cast_add, cast_one, bernoulli'_one, one_div]

Result:
case succ.succ.refine_2
n : ℕ
f :
  ∑ k ∈ range n, ↑(n.succ.succ.choose (k + 1 + 1)) * bernoulli' (k + 1 + 1) =
    ↑n + 1 + 1 - ↑(n.succ.succ.choose 0) * bernoulli' 0 - ↑(n.succ.succ.choose (0 + 1)) * bernoulli' (0 + 1)
⊢ ↑n + 1 + 1 - (↑0 + 1) - (↑n + 1 + 1) * 2⁻¹ = ↑n / 2

Proof state:
case zero

⊢ ∑ k ∈ range 0, ↑(Nat.choose 0 k) * bernoulli k = if 0 = 1 then 1 else 0

Tactic:
simp

Result:
no goals

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

Tactic:
congr

Result:
case succ.succ.refine_1.e_f
n : ℕ
f :
  ∑ k ∈ range n, ↑(n.succ.succ.choose (k + 1 + 1)) * bernoulli' (k + 1 + 1) =
    ↑n + 1 + 1 - ↑(n.succ.succ.choose 0) * bernoulli' 0 - ↑(n.succ.succ.choose (0 + 1)) * bernoulli' (0 + 1)
⊢ (fun i => ↑((n + 2).choose (i + 2)) * bernoulli (i + 2)) = fun k =>
    ↑(n.succ.succ.choose (k + 1 + 1)) * bernoulli' (k + 1 + 1)

Proof state:
n : ℕ
this : ∑ i ∈ range n, ↑((n + 2).choose (i + 2)) * bernoulli (i + 2) = ↑n / 2
⊢ ↑n / 2 + (↑n + 1 + 1) * (-1 / 2) + 1 = 0

Tactic:
ring

Result:
no goals

Proof state:
case succ.zero

⊢ ↑((0 + 1).choose 0) * bernoulli 0 = if 0 + 1 = 1 then 1 else 0

Tactic:
simp

Result:
no goals

Proof state:
case succ.succ.refine_2
n : ℕ
f :
  ∑ k ∈ range n, ↑(n.succ.succ.choose (k + 1 + 1)) * bernoulli' (k + 1 + 1) =
    ↑n + 1 + 1 - ↑(n.succ.succ.choose 0) * bernoulli' 0 - ↑(n.succ.succ.choose (0 + 1)) * bernoulli' (0 + 1)
⊢ ↑n + 1 + 1 - (↑0 + 1) - (↑n + 1 + 1) * 2⁻¹ = ↑n / 2

Tactic:
ring

Result:
no goals

Proof state:
case succ.zero

⊢ ∑ k ∈ range (0 + 1), ↑((0 + 1).choose k) * bernoulli k = if 0 + 1 = 1 then 1 else 0

Tactic:
rw [sum_range_one]

Result:
case succ.zero

⊢ ↑((0 + 1).choose 0) * bernoulli 0 = if 0 + 1 = 1 then 1 else 0

Proof state:
case succ.succ.refine_1.e_f.h
n : ℕ
f :
  ∑ k ∈ range n, ↑(n.succ.succ.choose (k + 1 + 1)) * bernoulli' (k + 1 + 1) =
    ↑n + 1 + 1 - ↑(n.succ.succ.choose 0) * bernoulli' 0 - ↑(n.succ.succ.choose (0 + 1)) * bernoulli' (0 + 1)
x : ℕ
⊢ ↑((n + 2).choose (x + 2)) * bernoulli (x + 2) = ↑(n.succ.succ.choose (x + 1 + 1)) * bernoulli' (x + 1 + 1)

Tactic:
rw [bernoulli_eq_bernoulli'_of_ne_one (succ_ne_zero x ∘ succ.inj)]

Result:
no goals

Proof state:
case succ.succ
n : ℕ
⊢ ∑ i ∈ range n, ↑((n + 2).choose (i + 2)) * bernoulli (i + 2) = ↑n / 2

Tactic:
have f := sum_bernoulli' n.succ.succ

Result:
case succ.succ
n : ℕ
f : ∑ k ∈ range n.succ.succ, ↑(n.succ.succ.choose k) * bernoulli' k = ↑n.succ.succ
⊢ ∑ i ∈ range n, ↑((n + 2).choose (i + 2)) * bernoulli (i + 2) = ↑n / 2