-- Mathlib/NumberTheory/BernoulliPolynomials.lean
theorem sum_range_pow_eq_bernoulli_sub (n p : ℕ) :
    ((p + 1 : ℚ) * ∑ k ∈ range n, (k : ℚ) ^ p) = (bernoulli p.succ).eval (n : ℚ) -
    _root_.bernoulli p.succ

Proof state:
n p : ℕ
⊢ (↑p + 1) * ∑ k ∈ range n, ↑k ^ p = eval (↑n) (bernoulli p.succ) - _root_.bernoulli p.succ

Tactic:
rw [sum_range_pow, bernoulli_def, eval_finset_sum, ← sum_div, mul_div_cancel₀ _ _]

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

n p : ℕ
⊢ ↑p + 1 ≠ 0

Proof state:
n p : ℕ
⊢ ∑ x ∈ range (p + 1), _root_.bernoulli (p.succ - (p + 1 - x)) * ↑(p.succ.choose (p + 1 - x)) * ↑n ^ (p + 1 - x) +
        _root_.bernoulli (p.succ - (p + 1 - (p + 1))) * ↑(p.succ.choose (p + 1 - (p + 1))) * ↑n ^ (p + 1 - (p + 1)) -
      _root_.bernoulli p.succ =
    ∑ i ∈ range (p + 1), _root_.bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i)

Tactic:
simp only [tsub_self, tsub_zero, choose_zero_right, cast_one, mul_one, _root_.pow_zero,
  add_tsub_cancel_right]

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

Proof state:
n p x : ℕ
hx : x ∈ range (p + 1)
⊢ ↑(p.succ.choose (p + 1 - x)) = ↑((p + 1).choose x)

Tactic:
rw [← choose_symm (mem_range_le hx)]

Result:
no goals

Proof state:
n p x : ℕ
hx : x ∈ range (p + 1)
⊢ _root_.bernoulli (p.succ - (p + 1 - x)) = _root_.bernoulli x

Tactic:
rw [Nat.sub_sub_self (mem_range_le hx)]

Result:
no goals

Proof state:
n p : ℕ
⊢ ∑ x ∈ range (p.succ + 1), _root_.bernoulli (p.succ - x) * ↑(p.succ.choose x) * ↑n ^ x - _root_.bernoulli p.succ =
    ∑ i ∈ range (p + 1), _root_.bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i)

Tactic:
rw [← sum_flip _, sum_range_succ]

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

Proof state:
n p x : ℕ
hx : x ∈ range (p + 1)
⊢ _root_.bernoulli (p.succ - (p + 1 - x)) * ↑(p.succ.choose (p + 1 - x)) * ↑n ^ (p + 1 - x) =
    _root_.bernoulli x * ↑((p + 1).choose x) * ↑n ^ (p + 1 - x)

Tactic:
apply congr_arg₂ _ (congr_arg₂ _ _ _) rfl

Result:
n p x : ℕ
hx : x ∈ range (p + 1)
⊢ _root_.bernoulli (p.succ - (p + 1 - x)) = _root_.bernoulli x

n p x : ℕ
hx : x ∈ range (p + 1)
⊢ ↑(p.succ.choose (p + 1 - x)) = ↑((p + 1).choose x)

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

Tactic:
simp_rw [eval_monomial]

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

Proof state:
n p : ℕ
⊢ ∀ x ∈ range (p + 1),
    _root_.bernoulli (p.succ - (p + 1 - x)) * ↑(p.succ.choose (p + 1 - x)) * ↑n ^ (p + 1 - x) =
      _root_.bernoulli x * ↑((p + 1).choose x) * ↑n ^ (p + 1 - x)

Tactic:
intro x hx

Result:
n p x : ℕ
hx : x ∈ range (p + 1)
⊢ _root_.bernoulli (p.succ - (p + 1 - x)) * ↑(p.succ.choose (p + 1 - x)) * ↑n ^ (p + 1 - x) =
    _root_.bernoulli x * ↑((p + 1).choose x) * ↑n ^ (p + 1 - x)

Proof state:
n p : ℕ
⊢ ∑ x ∈ range (p + 1), _root_.bernoulli (p.succ - (p + 1 - x)) * ↑(p.succ.choose (p + 1 - x)) * ↑n ^ (p + 1 - x) =
    ∑ i ∈ range (p + 1), _root_.bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i)

Tactic:
apply sum_congr rfl fun x hx => _

Result:
n p : ℕ
⊢ ∀ x ∈ range (p + 1),
    _root_.bernoulli (p.succ - (p + 1 - x)) * ↑(p.succ.choose (p + 1 - x)) * ↑n ^ (p + 1 - x) =
      _root_.bernoulli x * ↑((p + 1).choose x) * ↑n ^ (p + 1 - x)

Proof state:
n p : ℕ
⊢ ∑ i ∈ range (p + 1), _root_.bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) =
    ∑ x ∈ range (p.succ + 1), _root_.bernoulli (p.succ - x) * ↑(p.succ.choose x) * ↑n ^ x - _root_.bernoulli p.succ

Tactic:
symm

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

Proof state:
n p : ℕ
⊢ ↑p + 1 ≠ 0

Tactic:
norm_cast

Result:
no goals