-- Mathlib/RingTheory/Polynomial/Bernstein.lean
theorem iterate_derivative_at_0 (n ν : ℕ) :
    (Polynomial.derivative^[ν] (bernsteinPolynomial R n ν)).eval 0 =
      (ascPochhammer R ν).eval ((n - (ν - 1) : ℕ) : R)

Proof state:
case pos.succ.inr
R : Type u_1
inst✝ : CommRing R
ν : ℕ
ih :
  ∀ (n : ℕ), ν ≤ n → eval 0 ((⇑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (ascPochhammer R ν)
n : ℕ
h : ν + 1 ≤ n
h' : ν ≤ n - 1
h'' : ν > 0
⊢ ↑n * eval (↑(n - 1 - (ν - 1))) (ascPochhammer R ν) = ↑(n - ν) * eval (↑(n - ν) + 1) (ascPochhammer R ν)

Tactic:
have : n - 1 - (ν - 1) = n - ν := by omega

Result:
case pos.succ.inr
R : Type u_1
inst✝ : CommRing R
ν : ℕ
ih :
  ∀ (n : ℕ), ν ≤ n → eval 0 ((⇑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (ascPochhammer R ν)
n : ℕ
h : ν + 1 ≤ n
h' : ν ≤ n - 1
h'' : ν > 0
this : n - 1 - (ν - 1) = n - ν
⊢ ↑n * eval (↑(n - 1 - (ν - 1))) (ascPochhammer R ν) = ↑(n - ν) * eval (↑(n - ν) + 1) (ascPochhammer R ν)

Proof state:
case pos.succ.inl
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih :
  ∀ (n : ℕ), 0 ≤ n → eval 0 ((⇑derivative)^[0] (bernsteinPolynomial R n 0)) = eval (↑(n - (0 - 1))) (ascPochhammer R 0)
h : 0 + 1 ≤ n
h' : 0 ≤ n - 1
⊢ ↑n * eval (↑(n - 1 - (0 - 1))) (ascPochhammer R 0) = ↑(n - 0) * eval (↑(n - 0) + 1) (ascPochhammer R 0)

Tactic:
simp

Result:
no goals

Proof state:
case pos.succ.inr
R : Type u_1
inst✝ : CommRing R
ν : ℕ
ih :
  ∀ (n : ℕ), ν ≤ n → eval 0 ((⇑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (ascPochhammer R ν)
n : ℕ
h : ν + 1 ≤ n
h' : ν ≤ n - 1
h'' : ν > 0
this : n - 1 - (ν - 1) = n - ν
⊢ ↑n * eval (↑(n - 1 - (ν - 1))) (ascPochhammer R ν) = ↑(n - ν) * eval (↑(n - ν) + 1) (ascPochhammer R ν)

Tactic:
rw [this, ascPochhammer_eval_succ]

Result:
case pos.succ.inr
R : Type u_1
inst✝ : CommRing R
ν : ℕ
ih :
  ∀ (n : ℕ), ν ≤ n → eval 0 ((⇑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (ascPochhammer R ν)
n : ℕ
h : ν + 1 ≤ n
h' : ν ≤ n - 1
h'' : ν > 0
this : n - 1 - (ν - 1) = n - ν
⊢ ↑n * eval (↑(n - ν)) (ascPochhammer R ν) = (↑(n - ν) + ↑ν) * eval (↑(n - ν)) (ascPochhammer R ν)

Proof state:
case neg
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : n < ν
⊢ eval 0 ((⇑derivative)^[ν] 0) = eval (↑0) (ascPochhammer R ν)

Tactic:
simp [pos_iff_ne_zero.mp (pos_of_gt h)]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : n < ν
⊢ eval 0 ((⇑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (ascPochhammer R ν)

Tactic:
rw [tsub_eq_zero_iff_le.mpr (Nat.le_sub_one_of_lt h), eq_zero_of_lt R h]

Result:
case neg
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : n < ν
⊢ eval 0 ((⇑derivative)^[ν] 0) = eval (↑0) (ascPochhammer R ν)

Proof state:
case pos.succ
R : Type u_1
inst✝ : CommRing R
ν : ℕ
ih :
  ∀ (n : ℕ), ν ≤ n → eval 0 ((⇑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (ascPochhammer R ν)
n : ℕ
h : ν + 1 ≤ n
⊢ eval 0 ((⇑derivative)^[ν + 1] (bernsteinPolynomial R n (ν + 1))) = eval (↑(n - (ν + 1 - 1))) (ascPochhammer R (ν + 1))

Tactic:
have h' : ν ≤ n - 1 := le_tsub_of_add_le_right h

Result:
case pos.succ
R : Type u_1
inst✝ : CommRing R
ν : ℕ
ih :
  ∀ (n : ℕ), ν ≤ n → eval 0 ((⇑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (ascPochhammer R ν)
n : ℕ
h : ν + 1 ≤ n
h' : ν ≤ n - 1
⊢ eval 0 ((⇑derivative)^[ν + 1] (bernsteinPolynomial R n (ν + 1))) = eval (↑(n - (ν + 1 - 1))) (ascPochhammer R (ν + 1))

Proof state:
case pos.succ.inr
R : Type u_1
inst✝ : CommRing R
ν : ℕ
ih :
  ∀ (n : ℕ), ν ≤ n → eval 0 ((⇑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (ascPochhammer R ν)
n : ℕ
h : ν + 1 ≤ n
h' : ν ≤ n - 1
h'' : ν > 0
this : n - 1 - (ν - 1) = n - ν
⊢ ↑n * eval (↑(n - ν)) (ascPochhammer R ν) = (↑(n - ν) + ↑ν) * eval (↑(n - ν)) (ascPochhammer R ν)

Tactic:
rw_mod_cast [tsub_add_cancel_of_le (h'.trans n.pred_le)]

Result:
no goals

Proof state:
case pos.zero
R : Type u_1
inst✝ : CommRing R
n : ℕ
h : 0 ≤ n
⊢ eval 0 ((⇑derivative)^[0] (bernsteinPolynomial R n 0)) = eval (↑(n - (0 - 1))) (ascPochhammer R 0)

Tactic:
simp [eval_at_0]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
ν : ℕ
ih :
  ∀ (n : ℕ), ν ≤ n → eval 0 ((⇑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (ascPochhammer R ν)
n : ℕ
h : ν + 1 ≤ n
h' : ν ≤ n - 1
h'' : ν > 0
⊢ n - 1 - (ν - 1) = n - ν

Tactic:
omega

Result:
no goals

Proof state:
case pos.succ
R : Type u_1
inst✝ : CommRing R
ν : ℕ
ih :
  ∀ (n : ℕ), ν ≤ n → eval 0 ((⇑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (ascPochhammer R ν)
n : ℕ
h : ν + 1 ≤ n
h' : ν ≤ n - 1
⊢ ↑n * eval (↑(n - 1 - (ν - 1))) (ascPochhammer R ν) = ↑(n - ν) * eval (↑(n - ν) + 1) (ascPochhammer R ν)

Tactic:
obtain rfl | h'' := ν.eq_zero_or_pos

Result:
case pos.succ.inl
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih :
  ∀ (n : ℕ), 0 ≤ n → eval 0 ((⇑derivative)^[0] (bernsteinPolynomial R n 0)) = eval (↑(n - (0 - 1))) (ascPochhammer R 0)
h : 0 + 1 ≤ n
h' : 0 ≤ n - 1
⊢ ↑n * eval (↑(n - 1 - (0 - 1))) (ascPochhammer R 0) = ↑(n - 0) * eval (↑(n - 0) + 1) (ascPochhammer R 0)

case pos.succ.inr
R : Type u_1
inst✝ : CommRing R
ν : ℕ
ih :
  ∀ (n : ℕ), ν ≤ n → eval 0 ((⇑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (ascPochhammer R ν)
n : ℕ
h : ν + 1 ≤ n
h' : ν ≤ n - 1
h'' : ν > 0
⊢ ↑n * eval (↑(n - 1 - (ν - 1))) (ascPochhammer R ν) = ↑(n - ν) * eval (↑(n - ν) + 1) (ascPochhammer R ν)

Proof state:
case pos.succ
R : Type u_1
inst✝ : CommRing R
ν : ℕ
ih :
  ∀ (n : ℕ), ν ≤ n → eval 0 ((⇑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (ascPochhammer R ν)
n : ℕ
h : ν + 1 ≤ n
h' : ν ≤ n - 1
⊢ eval 0 ((⇑derivative)^[ν + 1] (bernsteinPolynomial R n (ν + 1))) = eval (↑(n - (ν + 1 - 1))) (ascPochhammer R (ν + 1))

Tactic:
simp only [derivative_succ, ih (n - 1) h', iterate_derivative_succ_at_0_eq_zero,
  Nat.succ_sub_succ_eq_sub, tsub_zero, sub_zero, iterate_derivative_sub,
  iterate_derivative_natCast_mul, eval_one, eval_mul, eval_add, eval_sub, eval_X, eval_comp,
  eval_natCast, Function.comp_apply, Function.iterate_succ, ascPochhammer_succ_left]

Result:
case pos.succ
R : Type u_1
inst✝ : CommRing R
ν : ℕ
ih :
  ∀ (n : ℕ), ν ≤ n → eval 0 ((⇑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (ascPochhammer R ν)
n : ℕ
h : ν + 1 ≤ n
h' : ν ≤ n - 1
⊢ ↑n * eval (↑(n - 1 - (ν - 1))) (ascPochhammer R ν) = ↑(n - ν) * eval (↑(n - ν) + 1) (ascPochhammer R ν)

Proof state:
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ eval 0 ((⇑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (ascPochhammer R ν)

Tactic:
by_cases h : ν ≤ n

Result:
case pos
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
⊢ eval 0 ((⇑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (ascPochhammer R ν)

case neg
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ¬ν ≤ n
⊢ eval 0 ((⇑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (ascPochhammer R ν)

Proof state:
case neg
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ¬ν ≤ n
⊢ eval 0 ((⇑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (ascPochhammer R ν)

Tactic:
simp only [not_le] at h

Result:
case neg
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : n < ν
⊢ eval 0 ((⇑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (ascPochhammer R ν)