case zero
R : Type u_1
inst✝ : CommRing R
ν : ℕ
⊢ ↑Polynomial.derivative (bernsteinPolynomial R Nat.zero (ν + 1)) =
    ↑Nat.zero * (bernsteinPolynomial R (Nat.zero - 1) ν - bernsteinPolynomial R (Nat.zero - 1) (ν + 1))

case succ
R : Type u_1
inst✝ : CommRing R
ν n✝ : ℕ
⊢ ↑Polynomial.derivative (bernsteinPolynomial R (Nat.succ n✝) (ν + 1)) =
    ↑(Nat.succ n✝) * (bernsteinPolynomial R (Nat.succ n✝ - 1) ν - bernsteinPolynomial R (Nat.succ n✝ - 1) (ν + 1))
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑Polynomial.derivative (bernsteinPolynomial R n (ν + 1)) =
    ↑n * (bernsteinPolynomial R (n - 1) ν - bernsteinPolynomial R (n - 1) (ν + 1))
cases n
no goals
case zero
R : Type u_1
inst✝ : CommRing R
ν : ℕ
⊢ ↑Polynomial.derivative (bernsteinPolynomial R Nat.zero (ν + 1)) =
    ↑Nat.zero * (bernsteinPolynomial R (Nat.zero - 1) ν - bernsteinPolynomial R (Nat.zero - 1) (ν + 1))
simp [bernsteinPolynomial]
case succ
R : Type u_1
inst✝ : CommRing R
ν n✝ : ℕ
⊢ ↑Polynomial.derivative (bernsteinPolynomial R (Nat.succ n✝) (ν + 1)) =
    (↑n✝ + 1) * (bernsteinPolynomial R (Nat.succ n✝ - 1) ν - bernsteinPolynomial R (Nat.succ n✝ - 1) (ν + 1))
case succ
R : Type u_1
inst✝ : CommRing R
ν n✝ : ℕ
⊢ ↑Polynomial.derivative (bernsteinPolynomial R (Nat.succ n✝) (ν + 1)) =
    ↑(Nat.succ n✝) * (bernsteinPolynomial R (Nat.succ n✝ - 1) ν - bernsteinPolynomial R (Nat.succ n✝ - 1) (ν + 1))
rw [Nat.cast_succ]
no goals
case succ
R : Type u_1
inst✝ : CommRing R
ν n✝ : ℕ
⊢ ↑Polynomial.derivative (bernsteinPolynomial R (Nat.succ n✝) (ν + 1)) =
    (↑n✝ + 1) * (bernsteinPolynomial R (Nat.succ n✝ - 1) ν - bernsteinPolynomial R (Nat.succ n✝ - 1) (ν + 1))
apply derivative_succ_aux