-- Mathlib/RingTheory/Polynomial/Bernstein.lean
theorem iterate_derivative_at_0_eq_zero_of_lt (n : ℕ) {ν k : ℕ} :
    k < ν → (Polynomial.derivative^[k] (bernsteinPolynomial R n ν)).eval 0 = 0

Proof state:
case succ
R : Type u_1
inst✝ : CommRing R
n k ν : ℕ
⊢ k ≤ ν → Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R n (ν + 1))) = 0

Tactic:
induction' k with k ih generalizing n ν

Result:
case succ.zero
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ 0 ≤ ν → Polynomial.eval 0 ((⇑Polynomial.derivative)^[0] (bernsteinPolynomial R n (ν + 1))) = 0

case succ.succ
R : Type u_1
inst✝ : CommRing R
k : ℕ
ih : ∀ (n ν : ℕ), k ≤ ν → Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R n (ν + 1))) = 0
n ν : ℕ
⊢ k + 1 ≤ ν → Polynomial.eval 0 ((⇑Polynomial.derivative)^[k + 1] (bernsteinPolynomial R n (ν + 1))) = 0

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

Tactic:
simp only [derivative_succ, Int.natCast_eq_zero, mul_eq_zero, Function.comp_apply,
  Function.iterate_succ, Polynomial.iterate_derivative_sub,
  Polynomial.iterate_derivative_natCast_mul, Polynomial.eval_mul, Polynomial.eval_natCast,
  Polynomial.eval_sub]

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

Proof state:
case h.e'_2.h.e'_4.h.h.e'_4.h.e'_4
R : Type u_1
inst✝ : CommRing R
k : ℕ
ih : ∀ (n ν : ℕ), k ≤ ν → Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R n (ν + 1))) = 0
n ν : ℕ
h : k + 1 ≤ ν
e_2✝ : Ring.toSemiring = CommSemiring.toSemiring
⊢ ν = ν.pred + 1

Tactic:
exact (Nat.succ_pred_eq_of_pos (k.succ_pos.trans_le h)).symm

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
n ν k : ℕ
⊢ k < ν → Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R n ν)) = 0

Tactic:
rcases ν with - | ν

Result:
case zero
R : Type u_1
inst✝ : CommRing R
n k : ℕ
⊢ k < 0 → Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R n 0)) = 0

case succ
R : Type u_1
inst✝ : CommRing R
n k ν : ℕ
⊢ k < ν + 1 → Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R n (ν + 1))) = 0

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

Tactic:
apply mul_eq_zero_of_right

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

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

Tactic:
convert ih _ _ (Nat.pred_le_pred h)

Result:
case h.e'_2.h.e'_4.h.h.e'_4.h.e'_4
R : Type u_1
inst✝ : CommRing R
k : ℕ
ih : ∀ (n ν : ℕ), k ≤ ν → Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R n (ν + 1))) = 0
n ν : ℕ
h : k + 1 ≤ ν
e_2✝ : Ring.toSemiring = CommSemiring.toSemiring
⊢ ν = ν.pred + 1

Proof state:
case zero
R : Type u_1
inst✝ : CommRing R
n k : ℕ
⊢ k < 0 → Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R n 0)) = 0

Tactic:
rintro ⟨⟩

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝ : CommRing R
n k ν : ℕ
⊢ k < ν + 1 → Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R n (ν + 1))) = 0

Tactic:
rw [Nat.lt_succ_iff]

Result:
case succ
R : Type u_1
inst✝ : CommRing R
n k ν : ℕ
⊢ k ≤ ν → Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R n (ν + 1))) = 0

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

Tactic:
rw [ih _ _ (Nat.le_of_succ_le h), sub_zero]

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

Proof state:
case succ.zero
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ 0 ≤ ν → Polynomial.eval 0 ((⇑Polynomial.derivative)^[0] (bernsteinPolynomial R n (ν + 1))) = 0

Tactic:
simp [eval_at_0]

Result:
no goals

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

Tactic:
intro h

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