n ν : ℕ
x : ↑I
⊢ Polynomial.eval (↑x) (↑(Nat.choose n ν) * Polynomial.X ^ ν * (1 - Polynomial.X) ^ (n - ν)) =
    ↑(Nat.choose n ν) * ↑x ^ ν * (1 - ↑x) ^ (n - ν)
n ν : ℕ
x : ↑I
⊢ ↑(bernstein n ν) x = ↑(Nat.choose n ν) * ↑x ^ ν * (1 - ↑x) ^ (n - ν)
dsimp [bernstein, Polynomial.toContinuousMapOn, Polynomial.toContinuousMap, bernsteinPolynomial]
no goals
n ν : ℕ
x : ↑I
⊢ Polynomial.eval (↑x) (↑(Nat.choose n ν) * Polynomial.X ^ ν * (1 - Polynomial.X) ^ (n - ν)) =
    ↑(Nat.choose n ν) * ↑x ^ ν * (1 - ↑x) ^ (n - ν)
simp