-- Mathlib/Algebra/Polynomial/Eval/Degree.lean
theorem eval_monomial_one_add_sub [CommRing S] (d : ℕ) (y : S) :
    eval (1 + y) (monomial d (d + 1 : S)) - eval y (monomial d (d + 1 : S)) =
      ∑ x_1 ∈ range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))

Proof state:
S : Type v
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑d.succ
⊢ ↑d.succ * ∑ x ∈ range (d + 1), ↑(d.choose x) * y ^ x - ↑d.succ * y ^ d =
    ∑ x_1 ∈ range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))

Tactic:
rw [sum_range_succ, mul_add, Nat.choose_self, Nat.cast_one, one_mul, add_sub_cancel_right,
  mul_sum, sum_range_succ', Nat.cast_zero, zero_mul, mul_zero, add_zero]

Result:
S : Type v
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑d.succ
⊢ ∑ i ∈ range d, ↑d.succ * (↑(d.choose i) * y ^ i) =
    ∑ k ∈ range d, ↑((d + 1).choose (k + 1)) * (↑(k + 1) * y ^ (k + 1 - 1))

Proof state:
S : Type v
inst✝ : CommRing S
d : ℕ
y : S
⊢ eval (1 + y) ((monomial d) (↑d + 1)) - eval y ((monomial d) (↑d + 1)) =
    ∑ x_1 ∈ range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))

Tactic:
have cast_succ : (d + 1 : S) = ((d.succ : ℕ) : S) := by simp only [Nat.cast_succ]

Result:
S : Type v
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑d.succ
⊢ eval (1 + y) ((monomial d) (↑d + 1)) - eval y ((monomial d) (↑d + 1)) =
    ∑ x_1 ∈ range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))

Proof state:
S : Type v
inst✝ : CommRing S
d : ℕ
y : S
⊢ ↑d + 1 = ↑d.succ

Tactic:
simp only [Nat.cast_succ]

Result:
no goals

Proof state:
S : Type v
inst✝ : CommRing S
d : ℕ
y✝ : S
cast_succ : ↑d + 1 = ↑d.succ
y : ℕ
_hy : y ∈ range d
⊢ ↑d.succ * (↑(d.choose y) * y✝ ^ y) = ↑((d + 1).choose (y + 1)) * (↑(y + 1) * y✝ ^ (y + 1 - 1))

Tactic:
rw [← mul_assoc, ← mul_assoc, ← Nat.cast_mul, Nat.succ_mul_choose_eq, Nat.cast_mul,
  Nat.add_sub_cancel]

Result:
no goals

Proof state:
S : Type v
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑d.succ
⊢ eval (1 + y) ((monomial d) (↑d + 1)) - eval y ((monomial d) (↑d + 1)) =
    ∑ x_1 ∈ range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))

Tactic:
rw [cast_succ, eval_monomial, eval_monomial, add_comm, add_pow]

Result:
S : Type v
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑d.succ
⊢ ↑d.succ * ∑ m ∈ range (d + 1), y ^ m * 1 ^ (d - m) * ↑(d.choose m) - ↑d.succ * y ^ d =
    ∑ x_1 ∈ range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))

Proof state:
S : Type v
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑d.succ
⊢ ∑ i ∈ range d, ↑d.succ * (↑(d.choose i) * y ^ i) =
    ∑ k ∈ range d, ↑((d + 1).choose (k + 1)) * (↑(k + 1) * y ^ (k + 1 - 1))

Tactic:
refine sum_congr rfl fun y _hy => ?_

Result:
S : Type v
inst✝ : CommRing S
d : ℕ
y✝ : S
cast_succ : ↑d + 1 = ↑d.succ
y : ℕ
_hy : y ∈ range d
⊢ ↑d.succ * (↑(d.choose y) * y✝ ^ y) = ↑((d + 1).choose (y + 1)) * (↑(y + 1) * y✝ ^ (y + 1 - 1))

Proof state:
S : Type v
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑d.succ
⊢ ↑d.succ * ∑ m ∈ range (d + 1), y ^ m * 1 ^ (d - m) * ↑(d.choose m) - ↑d.succ * y ^ d =
    ∑ x_1 ∈ range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))

Tactic:
simp only [one_pow, mul_one, mul_comm (y ^ _) (d.choose _)]

Result:
S : Type v
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑d.succ
⊢ ↑d.succ * ∑ x ∈ range (d + 1), ↑(d.choose x) * y ^ x - ↑d.succ * y ^ d =
    ∑ x_1 ∈ range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))