-- Mathlib/RingTheory/Polynomial/Bernstein.lean
theorem derivative_succ_aux (n ν : ℕ) :
    Polynomial.derivative (bernsteinPolynomial R (n + 1) (ν + 1)) =
      (n + 1) * (bernsteinPolynomial R n ν - bernsteinPolynomial R n (ν + 1))

Proof state:
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑((n + 1).choose (ν + 1)) * (↑(ν + 1) * X ^ ν) * (1 - X) ^ (n - ν) -
      ↑((n + 1).choose (ν + 1)) * X ^ (ν + 1) * (↑(n - ν) * (1 - X) ^ (n - ν - 1)) =
    ↑(n + 1) * (↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν)) -
      ↑(n + 1) * (↑(n.choose (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n - (ν + 1)))

Tactic:
refine congr (congr_arg Sub.sub ?_) ?_

Result:
case refine_1
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑((n + 1).choose (ν + 1)) * (↑(ν + 1) * X ^ ν) * (1 - X) ^ (n - ν) =
    ↑(n + 1) * (↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν))

case refine_2
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑((n + 1).choose (ν + 1)) * X ^ (ν + 1) * (↑(n - ν) * (1 - X) ^ (n - ν - 1)) =
    ↑(n + 1) * (↑(n.choose (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n - (ν + 1)))

Proof state:
case h.e'_2
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ (n - ν) * (n + 1).choose (ν + 1) = (n + 1).choose (ν + 1) * (n + 1 - (ν + 1))

Tactic:
rw [mul_comm, Nat.succ_sub_succ_eq_sub]

Result:
no goals

Proof state:
case refine_2.e_a
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑(n - ν) * ↑((n + 1).choose (ν + 1)) * X ^ (ν + 1) = ↑(n + 1) * ↑(n.choose (ν + 1)) * X ^ (ν + 1)

Tactic:
congr 1

Result:
case refine_2.e_a.e_a
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑(n - ν) * ↑((n + 1).choose (ν + 1)) = ↑(n + 1) * ↑(n.choose (ν + 1))

Proof state:
case h.e'_3
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ (n + 1) * n.choose (ν + 1) = n.choose (ν + 1) * (n + 1)

Tactic:
apply mul_comm

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ Polynomial.derivative (↑((n + 1).choose (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n + 1 - (ν + 1))) =
    (↑n + 1) * (bernsteinPolynomial R n ν - bernsteinPolynomial R n (ν + 1))

Tactic:
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_natCast, 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]

Result:
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑((n + 1).choose (ν + 1)) * (↑(ν + 1) * X ^ ν) * (1 - X) ^ (n - ν) -
      ↑((n + 1).choose (ν + 1)) * X ^ (ν + 1) * (↑(n - ν) * (1 - X) ^ (n - ν - 1)) =
    ↑(n + 1) * (↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν) - ↑(n.choose (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n - (ν + 1)))

Proof state:
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑((n + 1).choose (ν + 1)) * (↑(ν + 1) * X ^ ν) * (1 - X) ^ (n - ν) -
      ↑((n + 1).choose (ν + 1)) * X ^ (ν + 1) * (↑(n - ν) * (1 - X) ^ (n - ν - 1)) =
    ↑(n + 1) * (↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν) - ↑(n.choose (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n - (ν + 1)))

Tactic:
conv_rhs => rw [mul_sub]

Result:
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑((n + 1).choose (ν + 1)) * (↑(ν + 1) * X ^ ν) * (1 - X) ^ (n - ν) -
      ↑((n + 1).choose (ν + 1)) * X ^ (ν + 1) * (↑(n - ν) * (1 - X) ^ (n - ν - 1)) =
    ↑(n + 1) * (↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν)) -
      ↑(n + 1) * (↑(n.choose (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n - (ν + 1)))

Proof state:
case refine_2.e_a.e_a.e_a
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ (n - ν) * (n + 1).choose (ν + 1) = (n + 1) * n.choose (ν + 1)

Tactic:
convert (Nat.choose_mul_succ_eq n (ν + 1)).symm using 1

Result:
case h.e'_2
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ (n - ν) * (n + 1).choose (ν + 1) = (n + 1).choose (ν + 1) * (n + 1 - (ν + 1))

case h.e'_3
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ (n + 1) * n.choose (ν + 1) = n.choose (ν + 1) * (n + 1)

Proof state:
case refine_2.e_a.e_a
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑(n - ν) * ↑((n + 1).choose (ν + 1)) = ↑(n + 1) * ↑(n.choose (ν + 1))

Tactic:
norm_cast

Result:
case refine_2.e_a.e_a
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑((n - ν) * (n + 1).choose (ν + 1)) = ↑((n + 1) * n.choose (ν + 1))

Proof state:
case refine_1
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑((n + 1).choose (ν + 1)) * (↑(ν + 1) * X ^ ν) * (1 - X) ^ (n - ν) =
    ↑(n + 1) * (↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν))

Tactic:
simp only [← mul_assoc]

Result:
case refine_1
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑((n + 1).choose (ν + 1)) * ↑(ν + 1) * X ^ ν * (1 - X) ^ (n - ν) =
    ↑(n + 1) * ↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν)

Proof state:
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ Polynomial.derivative (bernsteinPolynomial R (n + 1) (ν + 1)) =
    (↑n + 1) * (bernsteinPolynomial R n ν - bernsteinPolynomial R n (ν + 1))

Tactic:
rw [bernsteinPolynomial]

Result:
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ Polynomial.derivative (↑((n + 1).choose (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n + 1 - (ν + 1))) =
    (↑n + 1) * (bernsteinPolynomial R n ν - bernsteinPolynomial R n (ν + 1))

Proof state:
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
this :
  ↑((n + 1).choose (ν + 1)) * (↑(ν + 1) * X ^ ν) * (1 - X) ^ (n - ν) -
      ↑((n + 1).choose (ν + 1)) * X ^ (ν + 1) * (↑(n - ν) * (1 - X) ^ (n - ν - 1)) =
    ↑(n + 1) * (↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν) - ↑(n.choose (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n - (ν + 1)))
⊢ Polynomial.derivative (↑((n + 1).choose (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n + 1 - (ν + 1))) =
    (↑n + 1) * (bernsteinPolynomial R n ν - bernsteinPolynomial R n (ν + 1))

Tactic:
simpa [Polynomial.derivative_pow, ← sub_eq_add_neg, Nat.succ_sub_succ_eq_sub,
  Polynomial.derivative_mul, Polynomial.derivative_natCast, 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]

Result:
no goals

Proof state:
case refine_2
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑((n + 1).choose (ν + 1)) * X ^ (ν + 1) * (↑(n - ν) * (1 - X) ^ (n - ν - 1)) =
    ↑(n + 1) * (↑(n.choose (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n - (ν + 1)))

Tactic:
rw [← tsub_add_eq_tsub_tsub, ← mul_assoc, ← mul_assoc]

Result:
case refine_2
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑((n + 1).choose (ν + 1)) * X ^ (ν + 1) * ↑(n - ν) * (1 - X) ^ (n - (ν + 1)) =
    ↑(n + 1) * (↑(n.choose (ν + 1)) * X ^ (ν + 1)) * (1 - X) ^ (n - (ν + 1))

Proof state:
case refine_2.e_a.e_a
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑((n - ν) * (n + 1).choose (ν + 1)) = ↑((n + 1) * n.choose (ν + 1))

Tactic:
congr 1

Result:
case refine_2.e_a.e_a.e_a
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ (n - ν) * (n + 1).choose (ν + 1) = (n + 1) * n.choose (ν + 1)

Proof state:
case refine_2
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑((n + 1).choose (ν + 1)) * X ^ (ν + 1) * ↑(n - ν) * (1 - X) ^ (n - (ν + 1)) =
    ↑(n + 1) * (↑(n.choose (ν + 1)) * X ^ (ν + 1)) * (1 - X) ^ (n - (ν + 1))

Tactic:
congr 1

Result:
case refine_2.e_a
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑((n + 1).choose (ν + 1)) * X ^ (ν + 1) * ↑(n - ν) = ↑(n + 1) * (↑(n.choose (ν + 1)) * X ^ (ν + 1))

Proof state:
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑((n + 1).choose (ν + 1)) * ↑(ν + 1) = ↑(n + 1) * ↑(n.choose ν)

Tactic:
exact mod_cast congr_arg (fun m : ℕ => (m : R[X])) (Nat.succ_mul_choose_eq n ν).symm

Result:
no goals