English
A reformulation of the expansion of (1 + y)^d: (d + 1)(1 + y)^d − (d + 1)y^d = ∑_{i=0}^d {d+1 \\choose i} · i · y^{i-1}.
Русский
Переформулировка разложения (1 + y)^d: (d+1)(1+y)^d − (d+1) y^d = ∑_{i=0}^d {d+1 \\choose i} · i · y^{i-1}.
LaTeX
$$$(d+1)(1+y)^d - (d+1) y^d = \\sum_{i=0}^d {d+1 \\choose i} \\cdot i \\cdot y^{i-1}$$$
Lean4
/-- A reformulation of the expansion of (1 + y)^d:
$$(d + 1) (1 + y)^d - (d + 1)y^d = \sum_{i = 0}^d {d + 1 \choose i} \cdot i \cdot y^{i - 1}.$$
-/
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)) :=
by
have cast_succ : (d + 1 : S) = ((d.succ : ℕ) : S) := by simp only [Nat.cast_succ]
rw [cast_succ, eval_monomial, eval_monomial, add_comm, add_pow]
simp only [one_pow, mul_one, mul_comm (y ^ _) (d.choose _)]
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]
refine sum_congr rfl fun y _hy => ?_
rw [← mul_assoc, ← mul_assoc, ← Nat.cast_mul, Nat.succ_mul_choose_eq, Nat.cast_mul, Nat.add_sub_cancel]
