-- Mathlib/NumberTheory/BernoulliPolynomials.lean
theorem bernoulli_eval_one_add (n : ℕ) (x : ℚ) :
    (bernoulli n).eval (1 + x) = (bernoulli n).eval x + n * x ^ (n - 1)

Proof state:
n : ℕ
x : ℚ
⊢ eval (1 + x) (bernoulli n) = eval x (bernoulli n) + ↑n * x ^ (n - 1)

Tactic:
refine Nat.strong_induction_on n fun d hd => ?_

Result:
n : ℕ
x : ℚ
d : ℕ
hd : ∀ m < d, eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
⊢ eval (1 + x) (bernoulli d) = eval x (bernoulli d) + ↑d * x ^ (d - 1)

Proof state:
n : ℕ
x : ℚ
d : ℕ
hd : ∀ m < d, eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑d.succ ≠ 0
⊢ ↑d.succ * eval (1 + x) (bernoulli d) = ↑d.succ * (eval x (bernoulli d) + ↑d * x ^ (d - 1))

Tactic:
rw [← smul_eq_mul, ← eval_smul, bernoulli_eq_sub_sum, mul_add, ← smul_eq_mul, ← eval_smul,
  bernoulli_eq_sub_sum, eval_sub, eval_finset_sum]

Result:
n : ℕ
x : ℚ
d : ℕ
hd : ∀ m < d, eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑d.succ ≠ 0
⊢ eval (1 + x) ((monomial d) ↑d.succ) - ∑ i ∈ range d, eval (1 + x) (↑((d + 1).choose i) • bernoulli i) =
    eval x ((monomial d) ↑d.succ - ∑ k ∈ range d, ↑((d + 1).choose k) • bernoulli k) + ↑d.succ * (↑d * x ^ (d - 1))

Proof state:
n : ℕ
x : ℚ
d : ℕ
hd : ∀ m < d, eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑d.succ ≠ 0
⊢ eval (1 + x) ((monomial d) ↑d.succ) - eval x ((monomial d) ↑d.succ) =
    ∑ x_1 ∈ range d, ↑((d + 1).choose x_1) • (↑x_1 * x ^ (x_1 - 1)) + ↑((d + 1).choose d) * (↑d * x ^ (d - 1))

Tactic:
rw [Nat.cast_succ, ← smul_eq_mul, ← sum_range_succ _ d, eval_monomial_one_add_sub]

Result:
n : ℕ
x : ℚ
d : ℕ
hd : ∀ m < d, eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑d.succ ≠ 0
⊢ ∑ x_1 ∈ range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * x ^ (x_1 - 1)) =
    ∑ x_1 ∈ range (d + 1), ↑((d + 1).choose x_1) • (↑x_1 * x ^ (x_1 - 1))

Proof state:
n : ℕ
x : ℚ
d : ℕ
hd : ∀ m < d, eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑d.succ ≠ 0
⊢ eval (1 + x) ((monomial d) ↑d.succ) -
      ∑ x_1 ∈ range d, ↑((d + 1).choose x_1) • (eval x (bernoulli x_1) + ↑x_1 * x ^ (x_1 - 1)) =
    eval x ((monomial d) ↑d.succ) - ∑ i ∈ range d, eval x (↑((d + 1).choose i) • bernoulli i) +
      ↑d.succ * (↑d * x ^ (d - 1))

Tactic:
simp_rw [eval_smul, smul_add]

Result:
n : ℕ
x : ℚ
d : ℕ
hd : ∀ m < d, eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑d.succ ≠ 0
⊢ eval (1 + x) ((monomial d) ↑d.succ) -
      ∑ x_1 ∈ range d,
        (↑((d + 1).choose x_1) • eval x (bernoulli x_1) + ↑((d + 1).choose x_1) • (↑x_1 * x ^ (x_1 - 1))) =
    eval x ((monomial d) ↑d.succ) - ∑ x_1 ∈ range d, ↑((d + 1).choose x_1) • eval x (bernoulli x_1) +
      ↑d.succ * (↑d * x ^ (d - 1))

Proof state:
n : ℕ
x : ℚ
d : ℕ
hd : ∀ m < d, eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑d.succ ≠ 0
⊢ eval (1 + x) ((monomial d) ↑d.succ) -
      ∑ x_1 ∈ range d,
        (↑((d + 1).choose x_1) • eval x (bernoulli x_1) + ↑((d + 1).choose x_1) • (↑x_1 * x ^ (x_1 - 1))) =
    eval x ((monomial d) ↑d.succ) - ∑ x_1 ∈ range d, ↑((d + 1).choose x_1) • eval x (bernoulli x_1) +
      ↑d.succ * (↑d * x ^ (d - 1))

Tactic:
rw [sum_add_distrib, sub_add, sub_eq_sub_iff_sub_eq_sub, _root_.add_sub_sub_cancel]

Result:
n : ℕ
x : ℚ
d : ℕ
hd : ∀ m < d, eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑d.succ ≠ 0
⊢ eval (1 + x) ((monomial d) ↑d.succ) - eval x ((monomial d) ↑d.succ) =
    ∑ x_1 ∈ range d, ↑((d + 1).choose x_1) • (↑x_1 * x ^ (x_1 - 1)) + ↑d.succ * (↑d * x ^ (d - 1))

Proof state:
n : ℕ
x : ℚ
d : ℕ
hd : ∀ m < d, eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑d.succ ≠ 0
⊢ eval (1 + x) (bernoulli d) = eval x (bernoulli d) + ↑d * x ^ (d - 1)

Tactic:
apply (mul_right_inj' nz).1

Result:
n : ℕ
x : ℚ
d : ℕ
hd : ∀ m < d, eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑d.succ ≠ 0
⊢ ↑d.succ * eval (1 + x) (bernoulli d) = ↑d.succ * (eval x (bernoulli d) + ↑d * x ^ (d - 1))

Proof state:
n : ℕ
x : ℚ
d : ℕ
hd : ∀ m < d, eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
⊢ ↑d.succ ≠ 0

Tactic:
norm_cast

Result:
no goals

Proof state:
n : ℕ
x : ℚ
d : ℕ
hd : ∀ m < d, eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑d.succ ≠ 0
⊢ eval (1 + x) ((monomial d) ↑d.succ) -
      ∑ x_1 ∈ range d, ↑((d + 1).choose x_1) • (eval x (bernoulli x_1) + ↑x_1 * x ^ (x_1 - 1)) =
    eval x ((monomial d) ↑d.succ - ∑ k ∈ range d, ↑((d + 1).choose k) • bernoulli k) + ↑d.succ * (↑d * x ^ (d - 1))

Tactic:
rw [eval_sub, eval_finset_sum]

Result:
n : ℕ
x : ℚ
d : ℕ
hd : ∀ m < d, eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑d.succ ≠ 0
⊢ eval (1 + x) ((monomial d) ↑d.succ) -
      ∑ x_1 ∈ range d, ↑((d + 1).choose x_1) • (eval x (bernoulli x_1) + ↑x_1 * x ^ (x_1 - 1)) =
    eval x ((monomial d) ↑d.succ) - ∑ i ∈ range d, eval x (↑((d + 1).choose i) • bernoulli i) +
      ↑d.succ * (↑d * x ^ (d - 1))

Proof state:
n : ℕ
x : ℚ
d : ℕ
hd : ∀ m < d, eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑d.succ ≠ 0
x✝ : ℕ
a✝ : x✝ ∈ range d
⊢ x✝ ∈ range d

Tactic:
assumption

Result:
no goals

Proof state:
n : ℕ
x : ℚ
d : ℕ
hd : ∀ m < d, eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑d.succ ≠ 0
⊢ ∑ x_1 ∈ range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * x ^ (x_1 - 1)) =
    ∑ x_1 ∈ range (d + 1), ↑((d + 1).choose x_1) • (↑x_1 * x ^ (x_1 - 1))

Tactic:
simp_rw [smul_eq_mul]

Result:
no goals

Proof state:
n : ℕ
x : ℚ
d : ℕ
hd : ∀ m < d, eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
⊢ eval (1 + x) (bernoulli d) = eval x (bernoulli d) + ↑d * x ^ (d - 1)

Tactic:
have nz : ((d.succ : ℕ) : ℚ) ≠ 0 := by norm_cast

Result:
n : ℕ
x : ℚ
d : ℕ
hd : ∀ m < d, eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑d.succ ≠ 0
⊢ eval (1 + x) (bernoulli d) = eval x (bernoulli d) + ↑d * x ^ (d - 1)