R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν =
    ∑ m in Finset.range (n + 1), X ^ m * (1 - X) ^ (n - m) * ↑(choose n m)
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν = (X + (1 - X)) ^ n
rw [add_pow]
no goals
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν =
    ∑ m in Finset.range (n + 1), X ^ m * (1 - X) ^ (n - m) * ↑(choose n m)
simp only [bernsteinPolynomial, mul_comm, mul_assoc, mul_left_comm]
no goals
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ (X + (1 - X)) ^ n = 1
simp