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

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