n : ℕ
⊢ ∑ x in range n, eval 0 (↑(monomial (n - x)) (_root_.bernoulli x * ↑(Nat.choose n x))) +
      eval 0 (↑(monomial (n - n)) (_root_.bernoulli n * ↑(Nat.choose n n))) =
    _root_.bernoulli n
n : ℕ
⊢ eval 0 (bernoulli n) = _root_.bernoulli n
rw [bernoulli, eval_finset_sum, sum_range_succ]
n : ℕ
this : ∑ x in range n, _root_.bernoulli x * ↑(Nat.choose n x) * 0 ^ (n - x) = 0
⊢ ∑ x in range n, eval 0 (↑(monomial (n - x)) (_root_.bernoulli x * ↑(Nat.choose n x))) +
      eval 0 (↑(monomial (n - n)) (_root_.bernoulli n * ↑(Nat.choose n n))) =
    _root_.bernoulli n
n : ℕ
⊢ ∑ x in range n, eval 0 (↑(monomial (n - x)) (_root_.bernoulli x * ↑(Nat.choose n x))) +
      eval 0 (↑(monomial (n - n)) (_root_.bernoulli n * ↑(Nat.choose n n))) =
    _root_.bernoulli n
have : (∑ x : ℕ in range n, _root_.bernoulli x * n.choose x * 0 ^ (n - x)) = 0 := by
  apply sum_eq_zero <| fun x hx => _
  intros x hx
  have h : x  <  n := (mem_range.1 hx)
  simp [h]
no goals
n : ℕ
this : ∑ x in range n, _root_.bernoulli x * ↑(Nat.choose n x) * 0 ^ (n - x) = 0
⊢ ∑ x in range n, eval 0 (↑(monomial (n - x)) (_root_.bernoulli x * ↑(Nat.choose n x))) +
      eval 0 (↑(monomial (n - n)) (_root_.bernoulli n * ↑(Nat.choose n n))) =
    _root_.bernoulli n
simp [this]
n : ℕ
⊢ ∀ (x : ℕ), x ∈ range n → _root_.bernoulli x * ↑(Nat.choose n x) * 0 ^ (n - x) = 0
n : ℕ
⊢ ∑ x in range n, _root_.bernoulli x * ↑(Nat.choose n x) * 0 ^ (n - x) = 0
apply sum_eq_zero <| fun x hx => _
n x : ℕ
hx : x ∈ range n
⊢ _root_.bernoulli x * ↑(Nat.choose n x) * 0 ^ (n - x) = 0
n : ℕ
⊢ ∀ (x : ℕ), x ∈ range n → _root_.bernoulli x * ↑(Nat.choose n x) * 0 ^ (n - x) = 0
intros x hx
n x : ℕ
hx : x ∈ range n
h : x < n
⊢ _root_.bernoulli x * ↑(Nat.choose n x) * 0 ^ (n - x) = 0
n x : ℕ
hx : x ∈ range n
⊢ _root_.bernoulli x * ↑(Nat.choose n x) * 0 ^ (n - x) = 0
have h : x  <  n := (mem_range.1 hx)
no goals
n x : ℕ
hx : x ∈ range n
h : x < n
⊢ _root_.bernoulli x * ↑(Nat.choose n x) * 0 ^ (n - x) = 0
simp [h]