R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑Polynomial.derivative (↑(choose (n + 1) (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n + 1 - (ν + 1))) =
    (↑n + 1) * (bernsteinPolynomial R n ν - bernsteinPolynomial R n (ν + 1))
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑Polynomial.derivative (bernsteinPolynomial R (n + 1) (ν + 1)) =
    (↑n + 1) * (bernsteinPolynomial R n ν - bernsteinPolynomial R n (ν + 1))
rw [bernsteinPolynomial]
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑(choose (n + 1) (ν + 1)) * (↑(ν + 1) * X ^ ν) * (1 - X) ^ (n - ν) -
      ↑(choose (n + 1) (ν + 1)) * X ^ (ν + 1) * (↑(n - ν) * (1 - X) ^ (n - ν - 1)) =
    ↑(n + 1) * (↑(choose n ν) * X ^ ν * (1 - X) ^ (n - ν) - ↑(choose n (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n - (ν + 1)))
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑Polynomial.derivative (↑(choose (n + 1) (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n + 1 - (ν + 1))) =
    (↑n + 1) * (bernsteinPolynomial R n ν - bernsteinPolynomial R n (ν + 1))
suffices ((n + 1).choose (ν + 1) : R[X]) * ((↑(ν + 1 : ℕ) : R[X]) * X ^ ν) * (1 - X) ^ (n - ν) -
    ((n + 1).choose (ν + 1) : R[X]) * X ^ (ν + 1) * ((↑(n - ν) : R[X]) * (1 - X) ^ (n - ν - 1)) =
    (↑(n + 1) : R[X]) * ((n.choose ν : R[X]) * X ^ ν * (1 - X) ^ (n - ν) -
      (n.choose (ν + 1) : R[X]) * X ^ (ν + 1) * (1 - X) ^ (n - (ν + 1))) by
  simpa [Polynomial.derivative_pow, ← sub_eq_add_neg, Nat.succ_sub_succ_eq_sub,
    Polynomial.derivative_mul, Polynomial.derivative_nat_cast, MulZeroClass.zero_mul,
    Nat.cast_add, algebraMap.coe_one, Polynomial.derivative_X, mul_one, zero_add,
    Polynomial.derivative_sub, Polynomial.derivative_one, zero_sub, mul_neg, Nat.sub_zero,
    bernsteinPolynomial, map_add, map_natCast, Nat.cast_one]
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑(choose (n + 1) (ν + 1)) * (↑(ν + 1) * X ^ ν) * (1 - X) ^ (n - ν) -
      ↑(choose (n + 1) (ν + 1)) * X ^ (ν + 1) * (↑(n - ν) * (1 - X) ^ (n - ν - 1)) =
    ↑(n + 1) * (↑(choose n ν) * X ^ ν * (1 - X) ^ (n - ν)) -
      ↑(n + 1) * (↑(choose n (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n - (ν + 1)))
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑(choose (n + 1) (ν + 1)) * (↑(ν + 1) * X ^ ν) * (1 - X) ^ (n - ν) -
      ↑(choose (n + 1) (ν + 1)) * X ^ (ν + 1) * (↑(n - ν) * (1 - X) ^ (n - ν - 1)) =
    ↑(n + 1) * (↑(choose n ν) * X ^ ν * (1 - X) ^ (n - ν) - ↑(choose n (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n - (ν + 1)))
conv_rhs => rw [mul_sub]
case refine'_1
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑(choose (n + 1) (ν + 1)) * (↑(ν + 1) * X ^ ν) * (1 - X) ^ (n - ν) =
    ↑(n + 1) * (↑(choose n ν) * X ^ ν * (1 - X) ^ (n - ν))

case refine'_2
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑(choose (n + 1) (ν + 1)) * X ^ (ν + 1) * (↑(n - ν) * (1 - X) ^ (n - ν - 1)) =
    ↑(n + 1) * (↑(choose n (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n - (ν + 1)))
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑(choose (n + 1) (ν + 1)) * (↑(ν + 1) * X ^ ν) * (1 - X) ^ (n - ν) -
      ↑(choose (n + 1) (ν + 1)) * X ^ (ν + 1) * (↑(n - ν) * (1 - X) ^ (n - ν - 1)) =
    ↑(n + 1) * (↑(choose n ν) * X ^ ν * (1 - X) ^ (n - ν)) -
      ↑(n + 1) * (↑(choose n (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n - (ν + 1)))
refine' congr (congr_arg Sub.sub _) _
no goals
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
this :
  ↑(choose (n + 1) (ν + 1)) * (↑(ν + 1) * X ^ ν) * (1 - X) ^ (n - ν) -
      ↑(choose (n + 1) (ν + 1)) * X ^ (ν + 1) * (↑(n - ν) * (1 - X) ^ (n - ν - 1)) =
    ↑(n + 1) * (↑(choose n ν) * X ^ ν * (1 - X) ^ (n - ν) - ↑(choose n (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n - (ν + 1)))
⊢ ↑Polynomial.derivative (↑(choose (n + 1) (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n + 1 - (ν + 1))) =
    (↑n + 1) * (bernsteinPolynomial R n ν - bernsteinPolynomial R n (ν + 1))
simpa [Polynomial.derivative_pow, ← sub_eq_add_neg, Nat.succ_sub_succ_eq_sub,
  Polynomial.derivative_mul, Polynomial.derivative_nat_cast, MulZeroClass.zero_mul,
  Nat.cast_add, algebraMap.coe_one, Polynomial.derivative_X, mul_one, zero_add,
  Polynomial.derivative_sub, Polynomial.derivative_one, zero_sub, mul_neg, Nat.sub_zero,
  bernsteinPolynomial, map_add, map_natCast, Nat.cast_one]
case refine'_1
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑(choose (n + 1) (ν + 1)) * ↑(ν + 1) * X ^ ν * (1 - X) ^ (n - ν) =
    ↑(n + 1) * ↑(choose n ν) * X ^ ν * (1 - X) ^ (n - ν)
case refine'_1
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑(choose (n + 1) (ν + 1)) * (↑(ν + 1) * X ^ ν) * (1 - X) ^ (n - ν) =
    ↑(n + 1) * (↑(choose n ν) * X ^ ν * (1 - X) ^ (n - ν))
simp only [← mul_assoc]
no goals
case refine'_1
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑(choose (n + 1) (ν + 1)) * ↑(ν + 1) = ↑(n + 1) * ↑(choose n ν)
exact_mod_cast congr_arg (fun m : ℕ => (m : R[X])) (Nat.succ_mul_choose_eq n ν).symm
case refine'_2
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑(choose (n + 1) (ν + 1)) * X ^ (ν + 1) * ↑(n - ν) * (1 - X) ^ (n - (ν + 1)) =
    ↑(n + 1) * (↑(choose n (ν + 1)) * X ^ (ν + 1)) * (1 - X) ^ (n - (ν + 1))
case refine'_2
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑(choose (n + 1) (ν + 1)) * X ^ (ν + 1) * (↑(n - ν) * (1 - X) ^ (n - ν - 1)) =
    ↑(n + 1) * (↑(choose n (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n - (ν + 1)))
rw [← tsub_add_eq_tsub_tsub, ← mul_assoc, ← mul_assoc]
case refine'_2.e_a
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑(choose (n + 1) (ν + 1)) * X ^ (ν + 1) * ↑(n - ν) = ↑(n + 1) * (↑(choose n (ν + 1)) * X ^ (ν + 1))
case refine'_2
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑(choose (n + 1) (ν + 1)) * X ^ (ν + 1) * ↑(n - ν) * (1 - X) ^ (n - (ν + 1)) =
    ↑(n + 1) * (↑(choose n (ν + 1)) * X ^ (ν + 1)) * (1 - X) ^ (n - (ν + 1))
congr 1
case refine'_2.e_a
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑(n - ν) * ↑(choose (n + 1) (ν + 1)) * X ^ (ν + 1) = ↑(n + 1) * ↑(choose n (ν + 1)) * X ^ (ν + 1)
case refine'_2.e_a
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑(choose (n + 1) (ν + 1)) * X ^ (ν + 1) * ↑(n - ν) = ↑(n + 1) * (↑(choose n (ν + 1)) * X ^ (ν + 1))
rw [mul_comm, ← mul_assoc, ← mul_assoc]
case refine'_2.e_a.e_a
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑(n - ν) * ↑(choose (n + 1) (ν + 1)) = ↑(n + 1) * ↑(choose n (ν + 1))
case refine'_2.e_a
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑(n - ν) * ↑(choose (n + 1) (ν + 1)) * X ^ (ν + 1) = ↑(n + 1) * ↑(choose n (ν + 1)) * X ^ (ν + 1)
congr 1
case refine'_2.e_a.e_a
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑((n - ν) * choose (n + 1) (ν + 1)) = ↑((n + 1) * choose n (ν + 1))
case refine'_2.e_a.e_a
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑(n - ν) * ↑(choose (n + 1) (ν + 1)) = ↑(n + 1) * ↑(choose n (ν + 1))
norm_cast
case refine'_2.e_a.e_a.e_a
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ (n - ν) * choose (n + 1) (ν + 1) = (n + 1) * choose n (ν + 1)
case refine'_2.e_a.e_a
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑((n - ν) * choose (n + 1) (ν + 1)) = ↑((n + 1) * choose n (ν + 1))
congr 1
case h.e'_2
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ (n - ν) * choose (n + 1) (ν + 1) = choose (n + 1) (ν + 1) * (n + 1 - (ν + 1))

case h.e'_3
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ (n + 1) * choose n (ν + 1) = choose n (ν + 1) * (n + 1)
case refine'_2.e_a.e_a.e_a
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ (n - ν) * choose (n + 1) (ν + 1) = (n + 1) * choose n (ν + 1)
convert (Nat.choose_mul_succ_eq n (ν + 1)).symm using 1
no goals
case h.e'_2
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ (n - ν) * choose (n + 1) (ν + 1) = choose (n + 1) (ν + 1) * (n + 1 - (ν + 1))
rw [mul_comm, Nat.succ_sub_succ_eq_sub]
no goals
case h.e'_3
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ (n + 1) * choose n (ν + 1) = choose n (ν + 1) * (n + 1)
apply mul_comm