n : ℕ
⊢ ∑ i in range (n + 1), eval 1 (↑(monomial (n - i)) (_root_.bernoulli i * ↑(Nat.choose n i))) = bernoulli' n
n : ℕ
⊢ eval 1 (bernoulli n) = bernoulli' n
simp only [bernoulli, eval_finset_sum]
n : ℕ
⊢ (if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n
n : ℕ
⊢ ∑ i in range (n + 1), eval 1 (↑(monomial (n - i)) (_root_.bernoulli i * ↑(Nat.choose n i))) = bernoulli' n
simp only [← succ_eq_add_one, sum_range_succ, mul_one, cast_one, choose_self,
  (_root_.bernoulli _).mul_comm, sum_bernoulli, one_pow, mul_one, eval_C, eval_monomial, one_mul]
case pos
n : ℕ
h : n = 1
⊢ (if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n

case neg
n : ℕ
h : ¬n = 1
⊢ (if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n
n : ℕ
⊢ (if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n
by_cases h : n = 1
case pos
n : ℕ
h : n = 1
⊢ 1 + -1 / 2 = 2⁻¹
case pos
n : ℕ
h : n = 1
⊢ (if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n
simp [h]
no goals
case pos
n : ℕ
h : n = 1
⊢ 1 + -1 / 2 = 2⁻¹
norm_num
case neg
n : ℕ
h : ¬n = 1
⊢ _root_.bernoulli n = bernoulli' n
case neg
n : ℕ
h : ¬n = 1
⊢ (if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n
simp [h]
no goals
case neg
n : ℕ
h : ¬n = 1
⊢ _root_.bernoulli n = bernoulli' n
exact bernoulli_eq_bernoulli'_of_ne_one h