R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ Polynomial.eval 1 (↑(choose n ν) * X ^ ν * (1 - X) ^ (n - ν)) = if ν = n then 1 else 0
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ Polynomial.eval 1 (bernsteinPolynomial R n ν) = if ν = n then 1 else 0
rw [bernsteinPolynomial]
case inl
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν = n
⊢ Polynomial.eval 1 (↑(choose n ν) * X ^ ν * (1 - X) ^ (n - ν)) = 1

case inr
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ¬ν = n
⊢ Polynomial.eval 1 (↑(choose n ν) * X ^ ν * (1 - X) ^ (n - ν)) = 0
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ Polynomial.eval 1 (↑(choose n ν) * X ^ ν * (1 - X) ^ (n - ν)) = if ν = n then 1 else 0
split_ifs with h
case inl
R : Type u_1
inst✝ : CommRing R
ν : ℕ
⊢ Polynomial.eval 1 (↑(choose ν ν) * X ^ ν * (1 - X) ^ (ν - ν)) = 1
case inl
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν = n
⊢ Polynomial.eval 1 (↑(choose n ν) * X ^ ν * (1 - X) ^ (n - ν)) = 1
subst h
no goals
case inl
R : Type u_1
inst✝ : CommRing R
ν : ℕ
⊢ Polynomial.eval 1 (↑(choose ν ν) * X ^ ν * (1 - X) ^ (ν - ν)) = 1
simp
case inr.inl
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ¬ν = n
w : n - ν = 0
⊢ Polynomial.eval 1 (↑(choose n ν) * X ^ ν * (1 - X) ^ (n - ν)) = 0

case inr.inr
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ¬ν = n
w : n - ν > 0
⊢ Polynomial.eval 1 (↑(choose n ν) * X ^ ν * (1 - X) ^ (n - ν)) = 0
case inr
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ¬ν = n
⊢ Polynomial.eval 1 (↑(choose n ν) * X ^ ν * (1 - X) ^ (n - ν)) = 0
obtain w | w := (n - ν).eq_zero_or_pos
no goals
case inr.inl
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ¬ν = n
w : n - ν = 0
⊢ Polynomial.eval 1 (↑(choose n ν) * X ^ ν * (1 - X) ^ (n - ν)) = 0
simp [Nat.choose_eq_zero_of_lt ((tsub_eq_zero_iff_le.mp w).lt_of_ne (Ne.symm h))]
no goals
case inr.inr
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ¬ν = n
w : n - ν > 0
⊢ Polynomial.eval 1 (↑(choose n ν) * X ^ ν * (1 - X) ^ (n - ν)) = 0
simp [zero_pow w]