awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
refine_1 :
  (↑((n + 1).choose (ν + 1)) : R[X]) * ((↑(ν + 1) : R[X]) * HPow.hPow (α := R[X]) X ν) *
      HSub.hSub (α := R[X]) 1 X ^ (n - ν) =
    (↑(n + 1) : R[X]) * ((↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (n - ν))
refine_2 :
  (↑((n + 1).choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1) *
      ((↑(n - ν) : R[X]) * HSub.hSub (α := R[X]) 1 X ^ (n - ν - 1)) =
    (↑(n + 1) : R[X]) *
      ((↑(n.choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1) * HSub.hSub (α := R[X]) 1 X ^ (n - (ν + 1)))
⊢ (↑((n + 1).choose (ν + 1)) : R[X]) * ((↑(ν + 1) : R[X]) * HPow.hPow (α := R[X]) X ν) *
        HSub.hSub (α := R[X]) 1 X ^ (n - ν) -
      (↑((n + 1).choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1) *
        ((↑(n - ν) : R[X]) * HSub.hSub (α := R[X]) 1 X ^ (n - ν - 1)) =
    (↑(n + 1) : R[X]) * ((↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (n - ν)) -
      (↑(n + 1) : R[X]) *
        ((↑(n.choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1) * HSub.hSub (α := R[X]) 1 X ^ (n - (ν + 1)))

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

Premises used: congr_arg, congr, Sub.sub
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
refine_1 :
  HMul.hMul (α := R[X]) (↑((n + 1).choose (ν + 1)) : R[X]) (↑(ν + 1) : R[X]) * HPow.hPow (α := R[X]) X ν *
      HSub.hSub (α := R[X]) 1 X ^ (n - ν) =
    HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν *
      HSub.hSub (α := R[X]) 1 X ^ (n - ν)
⊢ (↑((n + 1).choose (ν + 1)) : R[X]) * ((↑(ν + 1) : R[X]) * HPow.hPow (α := R[X]) X ν) *
      HSub.hSub (α := R[X]) 1 X ^ (n - ν) =
    (↑(n + 1) : R[X]) * ((↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (n - ν))

Tactic:
simp only [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
apply :
  HMul.hMul (α := R[X]) (↑((n + 1).choose (ν + 1)) : R[X]) (↑(ν + 1) : R[X]) =
    HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (↑(n.choose ν) : R[X])
⊢ HMul.hMul (α := R[X]) (↑((n + 1).choose (ν + 1)) : R[X]) (↑(ν + 1) : R[X]) * HPow.hPow (α := R[X]) X ν *
      HSub.hSub (α := R[X]) 1 X ^ (n - ν) =
    HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν *
      HSub.hSub (α := R[X]) 1 X ^ (n - ν)

Tactic:
apply congr (congr_arg (· * ·) (congr (congr_arg (· * ·) _) rfl)) rfl

Premises used: congr_arg, congr, rfl
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
⊢ HMul.hMul (α := R[X]) (↑((n + 1).choose (ν + 1)) : R[X]) (↑(ν + 1) : R[X]) =
    HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (↑(n.choose ν) : R[X])

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

Premises used: Nat.cast_mul._simp_1, Nat.choose, HMul.hMul, congrArg, cast, Nat.cast, congr_arg, Nat.cast_add, Nat.cast_mul, HAdd.hAdd, Nat.add_one_mul_choose_eq, congr, OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Eq.trans
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
⊢ HMul.hMul (α := R[X]) (↑((n + 1).choose (ν + 1)) : R[X]) (↑(ν + 1) : R[X]) =
    HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (↑(n.choose ν) : R[X])

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

Premises used: Nat.cast, congr_arg, Nat.add_one_mul_choose_eq, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
refine_2 :
  (↑((n + 1).choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1) * (↑(n - ν) : R[X]) *
      HSub.hSub (α := R[X]) 1 X ^ (n - (ν + 1)) =
    (↑(n + 1) : R[X]) * ((↑(n.choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1)) *
      HSub.hSub (α := R[X]) 1 X ^ (n - (ν + 1))
⊢ (↑((n + 1).choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1) *
      ((↑(n - ν) : R[X]) * HSub.hSub (α := R[X]) 1 X ^ (n - ν - 1)) =
    (↑(n + 1) : R[X]) *
      ((↑(n.choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1) * HSub.hSub (α := R[X]) 1 X ^ (n - (ν + 1)))

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

Premises used: mul_assoc, tsub_add_eq_tsub_tsub
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
refine_2 :
  (↑((n + 1).choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1) * (↑(n - ν) : R[X]) =
    (↑(n + 1) : R[X]) * ((↑(n.choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1))
⊢ (↑((n + 1).choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1) * (↑(n - ν) : R[X]) *
      HSub.hSub (α := R[X]) 1 X ^ (n - (ν + 1)) =
    (↑(n + 1) : R[X]) * ((↑(n.choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1)) *
      HSub.hSub (α := R[X]) 1 X ^ (n - (ν + 1))

Tactic:
congr 1
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
refine_2 :
  HMul.hMul (α := R[X]) (↑(n - ν) : R[X]) (↑((n + 1).choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1) =
    HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (↑(n.choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1)
⊢ (↑((n + 1).choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1) * (↑(n - ν) : R[X]) =
    (↑(n + 1) : R[X]) * ((↑(n.choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1))

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

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
refine_2 :
  HMul.hMul (α := R[X]) (↑(n - ν) : R[X]) (↑((n + 1).choose (ν + 1)) : R[X]) =
    HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (↑(n.choose (ν + 1)) : R[X])
⊢ HMul.hMul (α := R[X]) (↑(n - ν) : R[X]) (↑((n + 1).choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1) =
    HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (↑(n.choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1)

Tactic:
congr 1
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
refine_2 : Eq.{u_1 + 1} (α := R[X]) (↑((n - ν) * (n + 1).choose (ν + 1)) : R[X]) (↑((n + 1) * n.choose (ν + 1)) : R[X])
⊢ HMul.hMul (α := R[X]) (↑(n - ν) : R[X]) (↑((n + 1).choose (ν + 1)) : R[X]) =
    HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (↑(n.choose (ν + 1)) : R[X])

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
refine_2 : (n - ν) * (n + 1).choose (ν + 1) = (n + 1) * n.choose (ν + 1)
⊢ Eq.{u_1 + 1} (α := R[X]) (↑((n - ν) * (n + 1).choose (ν + 1)) : R[X]) (↑((n + 1) * n.choose (ν + 1)) : R[X])

Tactic:
congr 1
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
⊢ (n + 1).choose (ν + 1) * (n + 1 - (ν + 1)) = n.choose (ν + 1) * (n + 1)

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

Premises used: Nat.choose_mul_succ_eq, HAdd.hAdd, OfNat.ofNat, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
h : (n - ν) * (n + 1).choose (ν + 1) = (n + 1).choose (ν + 1) * (n + 1 - (ν + 1))
h₁ : (n + 1) * n.choose (ν + 1) = n.choose (ν + 1) * (n + 1)
⊢ (n - ν) * (n + 1).choose (ν + 1) = (n + 1) * n.choose (ν + 1)

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

Premises used: Nat.choose_mul_succ_eq, HAdd.hAdd, OfNat.ofNat, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
⊢ (n - ν) * (n + 1).choose (ν + 1) = (n + 1).choose (ν + 1) * (n - ν)

Tactic:
mul_comm _ _

Premises used: mul_comm
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
h : n + 1 - (ν + 1) = n - ν
⊢ (n - ν) * (n + 1).choose (ν + 1) = (n + 1).choose (ν + 1) * (n + 1 - (ν + 1))

Tactic:
convert! mul_comm _ _ using 2

Premises used: mul_comm
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
⊢ n + 1 - (ν + 1) = n - ν

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
⊢ (n + 1) * n.choose (ν + 1) = n.choose (ν + 1) * (n + 1)

Tactic:
apply mul_comm

Premises used: mul_comm
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
zero :
  (Polynomial.derivative : (a : R[X]) → R[X]) (bernsteinPolynomial R 0 (ν + 1)) =
    (↑0 : R[X]) *
      HSub.hSub (α := R[X]) (bernsteinPolynomial R (HSub.hSub (α := ℕ) 0 1) ν)
        (bernsteinPolynomial R (HSub.hSub (α := ℕ) 0 1) (ν + 1))
succ :
  ∀ (n : ℕ),
    (Polynomial.derivative : (a : R[X]) → R[X]) (bernsteinPolynomial R (n + 1) (ν + 1)) =
      (↑(n + 1) : R[X]) *
        HSub.hSub (α := R[X]) (bernsteinPolynomial R (n + 1 - 1) ν) (bernsteinPolynomial R (n + 1 - 1) (ν + 1))
⊢ (Polynomial.derivative : (a : R[X]) → R[X]) (bernsteinPolynomial R n (ν + 1)) =
    (↑n : R[X]) * HSub.hSub (α := R[X]) (bernsteinPolynomial R (n - 1) ν) (bernsteinPolynomial R (n - 1) (ν + 1))

Tactic:
cases n
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
ν : ℕ
⊢ (Polynomial.derivative : (a : R[X]) → R[X]) (bernsteinPolynomial R 0 (ν + 1)) =
    (↑0 : R[X]) *
      HSub.hSub (α := R[X]) (bernsteinPolynomial R (HSub.hSub (α := ℕ) 0 1) ν)
        (bernsteinPolynomial R (HSub.hSub (α := ℕ) 0 1) (ν + 1))

Tactic:
simp [bernsteinPolynomial]

Premises used: bernsteinPolynomial
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
ν n : ℕ
succ :
  (Polynomial.derivative : (a : R[X]) → R[X]) (bernsteinPolynomial R (n + 1) (ν + 1)) =
    HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 *
      HSub.hSub (α := R[X]) (bernsteinPolynomial R (n + 1 - 1) ν) (bernsteinPolynomial R (n + 1 - 1) (ν + 1))
⊢ (Polynomial.derivative : (a : R[X]) → R[X]) (bernsteinPolynomial R (n + 1) (ν + 1)) =
    (↑(n + 1) : R[X]) *
      HSub.hSub (α := R[X]) (bernsteinPolynomial R (n + 1 - 1) ν) (bernsteinPolynomial R (n + 1 - 1) (ν + 1))

Tactic:
rw [Nat.cast_succ]

Premises used: Nat.cast_succ
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
ν n : ℕ
⊢ (Polynomial.derivative : (a : R[X]) → R[X]) (bernsteinPolynomial R (n + 1) (ν + 1)) =
    HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 *
      HSub.hSub (α := R[X]) (bernsteinPolynomial R (n + 1 - 1) ν) (bernsteinPolynomial R (n + 1 - 1) (ν + 1))

Tactic:
apply derivative_succ_aux

Premises used: bernsteinPolynomial.derivative_succ_aux
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
⊢ (Polynomial.derivative : (a : R[X]) → R[X]) (bernsteinPolynomial R n 0) =
    HMul.hMul (α := R[X]) (-(↑n : R[X])) (bernsteinPolynomial R (n - 1) 0)

Tactic:
simp [bernsteinPolynomial, Polynomial.derivative_pow]

Premises used: bernsteinPolynomial, Polynomial.derivative_pow
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν k : ℕ
zero : k < 0 → Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R n 0)) = 0
succ :
  ∀ (ν : ℕ),
    k < ν + 1 →
      Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R n (ν + 1))) = 0
⊢ k < ν → Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R n ν)) = 0

Tactic:
rcases ν with - | ν
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n k ν : ℕ
succ :
  k ≤ ν → Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R n (ν + 1))) = 0
⊢ k < ν + 1 → Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R n (ν + 1))) = 0

Tactic:
rw [Nat.lt_succ_iff]

Premises used: Nat.lt_succ_iff
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
⊢ 0 ≤ ν → Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[0] (bernsteinPolynomial R n (ν + 1))) = 0

Tactic:
simp [eval_at_0]

Premises used: bernsteinPolynomial.eval_at_0
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
ih :
  ∀ (n ν : ℕ),
    k ≤ ν → Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R n (ν + 1))) = 0
n ν : ℕ
succ :
  k + 1 ≤ ν →
    (↑n : R) *
        (Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R (n - 1) ν)) -
          Polynomial.eval 0
            ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R (n - 1) (ν + 1)))) =
      0
⊢ k + 1 ≤ ν →
    Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k + 1] (bernsteinPolynomial R n (ν + 1))) = 0

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

Premises used: Function.iterate_succ, Polynomial.eval_natCast, Polynomial.iterate_derivative_natCast_mul, Polynomial.eval_mul, Polynomial.iterate_derivative_sub, bernsteinPolynomial.derivative_succ, Function.comp_apply, Polynomial.eval_sub
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
ih :
  ∀ (n ν : ℕ),
    k ≤ ν → Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R n (ν + 1))) = 0
n ν : ℕ
h : k + 1 ≤ ν
succ :
  Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R (n - 1) ν)) -
      Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R (n - 1) (ν + 1))) =
    0
⊢ (↑n : R) *
      (Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R (n - 1) ν)) -
        Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R (n - 1) (ν + 1)))) =
    0

Tactic:
apply mul_eq_zero_of_right

Premises used: mul_eq_zero_of_right
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
ih :
  ∀ (n ν : ℕ),
    k ≤ ν → Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R n (ν + 1))) = 0
n ν : ℕ
h : k + 1 ≤ ν
succ : Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R (n - 1) ν)) = 0
⊢ Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R (n - 1) ν)) -
      Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R (n - 1) (ν + 1))) =
    0

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

Premises used: sub_zero, Nat.le_of_succ_le
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
ih :
  ∀ (n ν : ℕ),
    k ≤ ν → Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R n (ν + 1))) = 0
n ν : ℕ
h : k + 1 ≤ ν
⊢ Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R (n - 1) (ν.pred + 1))) = 0

Tactic:
ih _ _ (Nat.pred_le_pred h)

Premises used: Nat.pred_le_pred
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
ih :
  ∀ (n ν : ℕ),
    k ≤ ν → Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R n (ν + 1))) = 0
n ν : ℕ
h : k + 1 ≤ ν
h₁ : Eq.{u_1 + 1} (α := Semiring R) Ring.toSemiring CommSemiring.toSemiring → ν = ν.pred + 1
⊢ Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R (n - 1) ν)) = 0

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

Premises used: Nat.pred_le_pred
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
ih :
  ∀ (n ν : ℕ),
    k ≤ ν → Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R n (ν + 1))) = 0
n ν : ℕ
h : k + 1 ≤ ν
e_2 : Eq.{u_1 + 1} (α := Semiring R) Ring.toSemiring CommSemiring.toSemiring
⊢ ν = ν.pred + 1

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

Premises used: Nat.succ_pred_eq_of_pos, LT.lt.trans_le, Nat.succ_pos, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
ih :
  ∀ (n ν : ℕ),
    k ≤ ν → Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R n (ν + 1))) = 0
n ν : ℕ
h : k + 1 ≤ ν
e_2 : Eq.{u_1 + 1} (α := Semiring R) Ring.toSemiring CommSemiring.toSemiring
⊢ ν = ν.pred + 1

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

Premises used: Nat.succ_pred_eq_of_pos, LT.lt.trans_le, Nat.succ_pos, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n k ν : ℕ
succ :
  ∀ (n ν : ℕ),
    0 ≤ ν → Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[0] (bernsteinPolynomial R n (ν + 1))) = 0
succ₁ :
  ∀ (k : ℕ)
    (ih :
      ∀ (n ν : ℕ),
        k ≤ ν →
          Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R n (ν + 1))) = 0)
    (n ν : ℕ),
    k + 1 ≤ ν →
      Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k + 1] (bernsteinPolynomial R n (ν + 1))) = 0
⊢ k ≤ ν → Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R n (ν + 1))) = 0

Tactic:
induction k generalizing n ν with
    | zero => simp [eval_at_0]
    | succ k ih =>
      simp only [derivative_succ, Function.comp_apply,
        Function.iterate_succ, Polynomial.iterate_derivative_sub,
        Polynomial.iterate_derivative_natCast_mul, Polynomial.eval_mul, Polynomial.eval_natCast,
        Polynomial.eval_sub]
      intro h
      apply mul_eq_zero_of_right
      rw [ih _ _ (Nat.le_of_succ_le h), sub_zero]
      convert! ih _ _ (Nat.pred_le_pred h)
      exact (Nat.succ_pred_eq_of_pos (k.succ_pos.trans_le h)).symm

Premises used: Function.iterate_succ, sub_zero, Polynomial.eval_natCast, Polynomial.iterate_derivative_natCast_mul, mul_eq_zero_of_right, Polynomial.eval_mul, Polynomial.iterate_derivative_sub, bernsteinPolynomial.derivative_succ, bernsteinPolynomial.eval_at_0, Function.comp_apply, Polynomial.eval_sub
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
⊢ Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[ν] (bernsteinPolynomial R n (ν + 1))) = 0

Tactic:
iterate_derivative_at_0_eq_zero_of_lt R n (lt_add_one ν)

Premises used: lt_add_one, bernsteinPolynomial.iterate_derivative_at_0_eq_zero_of_lt
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
n ν : ℕ
h : ν ≤ n
simp : ¬eval (↑(n - (ν - 1)) : R) (ascPochhammer R ν) = 0
⊢ eval 0 ((⇑derivative : (a : R[X]) → R[X])^[ν] (bernsteinPolynomial R n ν)) ≠ 0

Tactic:
simp only [bernsteinPolynomial.iterate_derivative_at_0, Ne]

Premises used: Ne, bernsteinPolynomial.iterate_derivative_at_0
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
n ν : ℕ
h : ν ≤ n
simp : ¬Eq.{u_1 + 1} (α := R) (↑(eval (n - (ν - 1)) (ascPochhammer ℕ ν)) : R) 0
⊢ ¬eval (↑(n - (ν - 1)) : R) (ascPochhammer R ν) = 0

Tactic:
simp only [← ascPochhammer_eval_cast]

Premises used: ascPochhammer_eval_cast
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
n ν : ℕ
h : ν ≤ n
norm_cast : ¬eval (n - (ν - 1)) (ascPochhammer ℕ ν) = 0
⊢ ¬Eq.{u_1 + 1} (α := R) (↑(eval (n - (ν - 1)) (ascPochhammer ℕ ν)) : R) 0

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
n ν : ℕ
h : ν ≤ n
h₁ : 0 < eval (n - (ν - 1)) (ascPochhammer ℕ ν)
⊢ ¬eval (n - (ν - 1)) (ascPochhammer ℕ ν) = 0

Tactic:
apply ne_of_gt

Premises used: ne_of_gt
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
n ν : ℕ
h : ν ≤ n
h₁ : ∀ (h : 0 ≤ n), 0 < eval (n - HSub.hSub (α := ℕ) 0 1) (ascPochhammer ℕ 0)
h₂ : ∀ (h' : ν > 0), 0 < eval (n - (ν - 1)) (ascPochhammer ℕ ν)
⊢ 0 < eval (n - (ν - 1)) (ascPochhammer ℕ ν)

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

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
n : ℕ
h : 0 ≤ n
⊢ 0 < eval (n - HSub.hSub (α := ℕ) 0 1) (ascPochhammer ℕ 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
n ν : ℕ
h : ν ≤ n
h' : ν > 0
⊢ ν.pred.succ ≤ n

Tactic:
rw [← Nat.succ_pred_eq_of_pos h'] at h

Premises used: Nat.succ_pred_eq_of_pos
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
n ν : ℕ
h : ν ≤ n
h' : ν > 0
h₁ : ν.pred.succ ≤ n
⊢ ν > 0

Tactic:
rw [← Nat.succ_pred_eq_of_pos h'] at h

Premises used: Nat.succ_pred_eq_of_pos
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
n ν : ℕ
h : ν.pred.succ ≤ n
h' : ν > 0
⊢ 0 < eval (n - (ν - 1)) (ascPochhammer ℕ ν)

Tactic:
ascPochhammer_pos _ _ (tsub_pos_of_lt (Nat.lt_of_succ_le h))

Premises used: Nat.lt_of_succ_le, ascPochhammer_pos, tsub_pos_of_lt
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
n ν : ℕ
h : ν.pred.succ ≤ n
h' : ν > 0
⊢ 0 < eval (n - (ν - 1)) (ascPochhammer ℕ ν)

Tactic:
exact ascPochhammer_pos _ _ (tsub_pos_of_lt (Nat.lt_of_succ_le h))

Premises used: Nat.lt_of_succ_le, ascPochhammer_pos, tsub_pos_of_lt
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν k : ℕ
w : k < n - ν
rw :
  eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k] (comp (bernsteinPolynomial R n (n - ν)) (HSub.hSub (α := R[X]) 1 X))) =
    0
⊢ eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R n ν)) = 0

Tactic:
rw [flip' _ _ _ (tsub_pos_iff_lt.mp (pos_of_gt w)).le]

Premises used: tsub_pos_iff_lt, bernsteinPolynomial.flip', pos_of_gt, LT.lt.le, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν k : ℕ
w : k < n - ν
⊢ eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k] (comp (bernsteinPolynomial R n (n - ν)) (HSub.hSub (α := R[X]) 1 X))) =
    0

Tactic:
simp [Polynomial.eval_comp, iterate_derivative_at_0_eq_zero_of_lt R n w]

Premises used: Polynomial.eval_comp, bernsteinPolynomial.iterate_derivative_at_0_eq_zero_of_lt
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
h : ν ≤ n
rw :
  eval 1
      ((⇑derivative : (a : R[X]) → R[X])^[n - ν] (comp (bernsteinPolynomial R n (n - ν)) (HSub.hSub (α := R[X]) 1 X))) =
    HPow.hPow (α := R) (-1) (n - ν) * eval (HAdd.hAdd (α := R) (↑ν : R) 1) (ascPochhammer R (n - ν))
⊢ eval 1 ((⇑derivative : (a : R[X]) → R[X])^[n - ν] (bernsteinPolynomial R n ν)) =
    HPow.hPow (α := R) (-1) (n - ν) * eval (HAdd.hAdd (α := R) (↑ν : R) 1) (ascPochhammer R (n - ν))

Tactic:
rw [flip' _ _ _ h]

Premises used: bernsteinPolynomial.flip'
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
h : ν ≤ n
simp :
  HPow.hPow (α := R) (-1) (n - ν) * eval (↑(n - (n - ν - 1)) : R) (ascPochhammer R (n - ν)) =
    HPow.hPow (α := R) (-1) (n - ν) * eval (HAdd.hAdd (α := R) (↑ν : R) 1) (ascPochhammer R (n - ν))
⊢ eval 1
      ((⇑derivative : (a : R[X]) → R[X])^[n - ν] (comp (bernsteinPolynomial R n (n - ν)) (HSub.hSub (α := R[X]) 1 X))) =
    HPow.hPow (α := R) (-1) (n - ν) * eval (HAdd.hAdd (α := R) (↑ν : R) 1) (ascPochhammer R (n - ν))

Tactic:
simp only [iterate_derivative_comp_one_sub_X, eval_mul, eval_pow, eval_neg, eval_one, eval_comp,
    eval_sub, eval_X, sub_self, iterate_derivative_at_0]

Premises used: sub_self, Polynomial.eval_X, Polynomial.eval_pow, Polynomial.iterate_derivative_comp_one_sub_X, Polynomial.eval_mul, Polynomial.eval_comp, Polynomial.eval_one, Polynomial.eval_neg, bernsteinPolynomial.iterate_derivative_at_0, Polynomial.eval_sub