n p : ℕ
⊢ ∑ x in range (p + 1), _root_.bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x) =
    ∑ i in range (succ p + 1), eval (↑n) (↑(monomial i) (_root_.bernoulli (succ p - i) * ↑(Nat.choose (succ p) i))) -
      _root_.bernoulli (succ p)

n p : ℕ
⊢ ↑p + 1 ≠ 0
n p : ℕ
⊢ (↑p + 1) * ∑ k in range n, ↑k ^ p = eval (↑n) (bernoulli (succ p)) - _root_.bernoulli (succ p)
rw [sum_range_pow, bernoulli_def, eval_finset_sum, ← sum_div, mul_div_cancel' _ _]
n p : ℕ
⊢ ∑ x in range (p + 1), _root_.bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x) =
    ∑ x in range (succ p + 1), _root_.bernoulli (succ p - x) * ↑(Nat.choose (succ p) x) * ↑n ^ x -
      _root_.bernoulli (succ p)
n p : ℕ
⊢ ∑ x in range (p + 1), _root_.bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x) =
    ∑ i in range (succ p + 1), eval (↑n) (↑(monomial i) (_root_.bernoulli (succ p - i) * ↑(Nat.choose (succ p) i))) -
      _root_.bernoulli (succ p)
simp_rw [eval_monomial]
n p : ℕ
⊢ ∑ x in range (succ p + 1), _root_.bernoulli (succ p - x) * ↑(Nat.choose (succ p) x) * ↑n ^ x -
      _root_.bernoulli (succ p) =
    ∑ x in range (p + 1), _root_.bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x)
n p : ℕ
⊢ ∑ x in range (p + 1), _root_.bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x) =
    ∑ x in range (succ p + 1), _root_.bernoulli (succ p - x) * ↑(Nat.choose (succ p) x) * ↑n ^ x -
      _root_.bernoulli (succ p)
symm
n p : ℕ
⊢ ∑ x in range (p + 1),
          _root_.bernoulli (succ p - (p + 1 - x)) * ↑(Nat.choose (succ p) (p + 1 - x)) * ↑n ^ (p + 1 - x) +
        _root_.bernoulli (succ p - (p + 1 - (p + 1))) * ↑(Nat.choose (succ p) (p + 1 - (p + 1))) *
          ↑n ^ (p + 1 - (p + 1)) -
      _root_.bernoulli (succ p) =
    ∑ x in range (p + 1), _root_.bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x)
n p : ℕ
⊢ ∑ x in range (succ p + 1), _root_.bernoulli (succ p - x) * ↑(Nat.choose (succ p) x) * ↑n ^ x -
      _root_.bernoulli (succ p) =
    ∑ x in range (p + 1), _root_.bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x)
rw [← sum_flip _, sum_range_succ]
n p : ℕ
⊢ ∑ x in range (p + 1),
      _root_.bernoulli (succ p - (p + 1 - x)) * ↑(Nat.choose (succ p) (p + 1 - x)) * ↑n ^ (p + 1 - x) =
    ∑ x in range (p + 1), _root_.bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x)
n p : ℕ
⊢ ∑ x in range (p + 1),
          _root_.bernoulli (succ p - (p + 1 - x)) * ↑(Nat.choose (succ p) (p + 1 - x)) * ↑n ^ (p + 1 - x) +
        _root_.bernoulli (succ p - (p + 1 - (p + 1))) * ↑(Nat.choose (succ p) (p + 1 - (p + 1))) *
          ↑n ^ (p + 1 - (p + 1)) -
      _root_.bernoulli (succ p) =
    ∑ x in range (p + 1), _root_.bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x)
simp only [tsub_self, tsub_zero, choose_zero_right, cast_one, mul_one, _root_.pow_zero,
  add_tsub_cancel_right]
n p : ℕ
⊢ ∀ (x : ℕ),
    x ∈ range (p + 1) →
      _root_.bernoulli (succ p - (p + 1 - x)) * ↑(Nat.choose (succ p) (p + 1 - x)) * ↑n ^ (p + 1 - x) =
        _root_.bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x)
n p : ℕ
⊢ ∑ x in range (p + 1),
      _root_.bernoulli (succ p - (p + 1 - x)) * ↑(Nat.choose (succ p) (p + 1 - x)) * ↑n ^ (p + 1 - x) =
    ∑ x in range (p + 1), _root_.bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x)
apply sum_congr rfl fun x hx => _
n p x : ℕ
hx : x ∈ range (p + 1)
⊢ _root_.bernoulli (succ p - (p + 1 - x)) * ↑(Nat.choose (succ p) (p + 1 - x)) * ↑n ^ (p + 1 - x) =
    _root_.bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x)
n p : ℕ
⊢ ∀ (x : ℕ),
    x ∈ range (p + 1) →
      _root_.bernoulli (succ p - (p + 1 - x)) * ↑(Nat.choose (succ p) (p + 1 - x)) * ↑n ^ (p + 1 - x) =
        _root_.bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x)
intro x hx
n p x : ℕ
hx : x ∈ range (p + 1)
⊢ _root_.bernoulli (succ p - (p + 1 - x)) = _root_.bernoulli x

n p x : ℕ
hx : x ∈ range (p + 1)
⊢ ↑(Nat.choose (succ p) (p + 1 - x)) = ↑(Nat.choose (p + 1) x)
n p x : ℕ
hx : x ∈ range (p + 1)
⊢ _root_.bernoulli (succ p - (p + 1 - x)) * ↑(Nat.choose (succ p) (p + 1 - x)) * ↑n ^ (p + 1 - x) =
    _root_.bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x)
apply congr_arg₂ _ (congr_arg₂ _ _ _) rfl
no goals
n p x : ℕ
hx : x ∈ range (p + 1)
⊢ _root_.bernoulli (succ p - (p + 1 - x)) = _root_.bernoulli x
rw [Nat.sub_sub_self (mem_range_le hx)]
no goals
n p x : ℕ
hx : x ∈ range (p + 1)
⊢ ↑(Nat.choose (succ p) (p + 1 - x)) = ↑(Nat.choose (p + 1) x)
rw [← choose_symm (mem_range_le hx)]
n p : ℕ
⊢ ¬p + 1 = 0
n p : ℕ
⊢ ↑p + 1 ≠ 0
norm_cast
no goals
n p : ℕ
⊢ ¬p + 1 = 0
apply succ_ne_zero _