R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
⊢ eval (1 + y) (↑(monomial d) (↑d + 1)) - eval y (↑(monomial d) (↑d + 1)) =
    ∑ x_1 in range (d + 1), ↑(Nat.choose (d + 1) x_1) * (↑x_1 * y ^ (x_1 - 1))
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
⊢ eval (1 + y) (↑(monomial d) (↑d + 1)) - eval y (↑(monomial d) (↑d + 1)) =
    ∑ x_1 in range (d + 1), ↑(Nat.choose (d + 1) x_1) * (↑x_1 * y ^ (x_1 - 1))
have cast_succ : (d + 1 : S) = ((d.succ : ℕ) : S) := by simp only [Nat.cast_succ]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
⊢ ↑(Nat.succ d) * ∑ m in range (d + 1), y ^ m * 1 ^ (d - m) * ↑(Nat.choose d m) - ↑(Nat.succ d) * y ^ d =
    ∑ x_1 in range (d + 1), ↑(Nat.choose (d + 1) x_1) * (↑x_1 * y ^ (x_1 - 1))
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
⊢ eval (1 + y) (↑(monomial d) (↑d + 1)) - eval y (↑(monomial d) (↑d + 1)) =
    ∑ x_1 in range (d + 1), ↑(Nat.choose (d + 1) x_1) * (↑x_1 * y ^ (x_1 - 1))
rw [cast_succ, eval_monomial, eval_monomial, add_comm, add_pow]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
⊢ ∑ x in range d, ↑(Nat.succ d) * (↑(Nat.choose d x) * y ^ x) =
    ∑ k in range d, ↑(Nat.choose (d + 1) (k + 1)) * (↑(k + 1) * y ^ (k + 1 - 1))
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
⊢ ↑(Nat.succ d) * ∑ x in range (d + 1), ↑(Nat.choose d x) * y ^ x - ↑(Nat.succ d) * y ^ d =
    ∑ x_1 in range (d + 1), ↑(Nat.choose (d + 1) x_1) * (↑x_1 * y ^ (x_1 - 1))
rw [sum_range_succ, mul_add, Nat.choose_self, Nat.cast_one, one_mul, add_sub_cancel, mul_sum,
  sum_range_succ', Nat.cast_zero, zero_mul, mul_zero, add_zero]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y✝ : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
y : ℕ
_hy : y ∈ range d
⊢ ↑(Nat.succ d) * (↑(Nat.choose d y) * y✝ ^ y) = ↑(Nat.choose (d + 1) (y + 1)) * (↑(y + 1) * y✝ ^ (y + 1 - 1))
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
⊢ ∑ x in range d, ↑(Nat.succ d) * (↑(Nat.choose d x) * y ^ x) =
    ∑ k in range d, ↑(Nat.choose (d + 1) (k + 1)) * (↑(k + 1) * y ^ (k + 1 - 1))
refine sum_congr rfl fun y _hy => ?_
no goals
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y✝ : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
y : ℕ
_hy : y ∈ range d
⊢ ↑(Nat.succ d) * (↑(Nat.choose d y) * y✝ ^ y) = ↑(Nat.choose (d + 1) (y + 1)) * (↑(y + 1) * y✝ ^ (y + 1 - 1))
rw [← mul_assoc, ← mul_assoc, ← Nat.cast_mul, Nat.succ_mul_choose_eq, Nat.cast_mul,
  Nat.add_sub_cancel]
no goals
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
⊢ ↑d + 1 = ↑(Nat.succ d)
simp only [Nat.cast_succ]