R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
⊢ eval 1 ((↑derivative^[n - ν]) (comp (bernsteinPolynomial R n (n - ν)) (1 - X))) =
    (-1) ^ (n - ν) * eval (↑ν + 1) (pochhammer R (n - ν))
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
⊢ eval 1 ((↑derivative^[n - ν]) (bernsteinPolynomial R n ν)) = (-1) ^ (n - ν) * eval (↑ν + 1) (pochhammer R (n - ν))
rw [flip' _ _ _ h]
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
⊢ (-1) ^ (n - ν) * eval (↑(n - (n - ν - 1))) (pochhammer R (n - ν)) =
    (-1) ^ (n - ν) * eval (↑ν + 1) (pochhammer R (n - ν))
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
⊢ eval 1 ((↑derivative^[n - ν]) (comp (bernsteinPolynomial R n (n - ν)) (1 - X))) =
    (-1) ^ (n - ν) * eval (↑ν + 1) (pochhammer R (n - ν))
simp [Polynomial.eval_comp, h]
case inl
R : Type u_1
inst✝ : CommRing R
ν : ℕ
h : ν ≤ ν
⊢ (-1) ^ (ν - ν) * eval (↑(ν - (ν - ν - 1))) (pochhammer R (ν - ν)) =
    (-1) ^ (ν - ν) * eval (↑ν + 1) (pochhammer R (ν - ν))

case inr
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
h' : ν < n
⊢ (-1) ^ (n - ν) * eval (↑(n - (n - ν - 1))) (pochhammer R (n - ν)) =
    (-1) ^ (n - ν) * eval (↑ν + 1) (pochhammer R (n - ν))
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
⊢ (-1) ^ (n - ν) * eval (↑(n - (n - ν - 1))) (pochhammer R (n - ν)) =
    (-1) ^ (n - ν) * eval (↑ν + 1) (pochhammer R (n - ν))
obtain rfl | h' := h.eq_or_lt
no goals
case inl
R : Type u_1
inst✝ : CommRing R
ν : ℕ
h : ν ≤ ν
⊢ (-1) ^ (ν - ν) * eval (↑(ν - (ν - ν - 1))) (pochhammer R (ν - ν)) =
    (-1) ^ (ν - ν) * eval (↑ν + 1) (pochhammer R (ν - ν))
simp
case inr.e_a.e_a
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
h' : ν < n
⊢ ↑(n - (n - ν - 1)) = ↑ν + 1
case inr
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
h' : ν < n
⊢ (-1) ^ (n - ν) * eval (↑(n - (n - ν - 1))) (pochhammer R (n - ν)) =
    (-1) ^ (n - ν) * eval (↑ν + 1) (pochhammer R (n - ν))
congr
case inr.e_a.e_a
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
h' : ν < n
⊢ ↑(n - (n - ν - 1)) = ↑(ν + 1)
case inr.e_a.e_a
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
h' : ν < n
⊢ ↑(n - (n - ν - 1)) = ↑ν + 1
norm_cast
no goals
case inr.e_a.e_a
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
h' : ν < n
⊢ ↑(n - (n - ν - 1)) = ↑(ν + 1)
rw [← tsub_add_eq_tsub_tsub, tsub_tsub_cancel_of_le (Nat.succ_le_iff.mpr h')]