awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
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))
⊢ (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))
have 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))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
ν 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))
have 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))
Tactic: rw [Nat.cast_succ]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
n ν k : ℕ
⊢ k < ν → Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R n ν)) = 0
have zero : k < 0 → Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R n 0)) = 0
Tactic: rcases ν with - | ν
Cleared hypotheses: ν
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
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
⊢ k < ν → Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R n ν)) = 0
have succ : ∀ (ν : ℕ),
  k < ν + 1 → Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R n (ν + 1))) = 0
Tactic: rcases ν with - | ν
Cleared hypotheses: ν
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
n k ν : ℕ
⊢ k < ν + 1 → Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R n (ν + 1))) = 0
have succ : k ≤ ν → Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R n (ν + 1))) = 0
Tactic: rw [Nat.lt_succ_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
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 ν : ℕ
⊢ k + 1 ≤ ν →
    Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k + 1] (bernsteinPolynomial R n (ν + 1))) = 0
have 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
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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
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 ≤ ν
⊢ (↑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
have 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
Tactic: apply mul_eq_zero_of_right
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
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) ν)) -
      Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R (n - 1) (ν + 1))) =
    0
have succ : Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R (n - 1) ν)) = 0
Tactic: rw [ih _ _ (Nat.le_of_succ_le h), sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
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) ν)) = 0
have h₁ : Eq.{u_1 + 1} (α := Semiring R) Ring.toSemiring CommSemiring.toSemiring → ν = ν.pred + 1
Tactic: convert! ih _ _ (Nat.pred_le_pred h)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
n k ν : ℕ
⊢ k ≤ ν → Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R n (ν + 1))) = 0
have succ : ∀ (n ν : ℕ),
  0 ≤ ν → Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[0] (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
Cleared hypotheses: n, k, ν
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
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
⊢ k ≤ ν → Polynomial.eval 0 ((⇑Polynomial.derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R n (ν + 1))) = 0
have 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
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
Cleared hypotheses: n, k, ν
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ eval 0 ((⇑derivative : (a : R[X]) → R[X])^[ν] (bernsteinPolynomial R n ν)) ≠ 0
have simp : ¬eval (↑(n - (ν - 1)) : R) (ascPochhammer R ν) = 0
Tactic: simp only [bernsteinPolynomial.iterate_derivative_at_0, Ne]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ ¬eval (↑(n - (ν - 1)) : R) (ascPochhammer R ν) = 0
have simp : ¬Eq.{u_1 + 1} (α := R) (↑(eval (n - (ν - 1)) (ascPochhammer ℕ ν)) : R) 0
Tactic: simp only [← ascPochhammer_eval_cast]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ ¬Eq.{u_1 + 1} (α := R) (↑(eval (n - (ν - 1)) (ascPochhammer ℕ ν)) : R) 0
have norm_cast : ¬eval (n - (ν - 1)) (ascPochhammer ℕ ν) = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ ¬eval (n - (ν - 1)) (ascPochhammer ℕ ν) = 0
have h₁ : 0 < eval (n - (ν - 1)) (ascPochhammer ℕ ν)
Tactic: apply ne_of_gt
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ 0 < eval (n - (ν - 1)) (ascPochhammer ℕ ν)
have h₁ : ∀ (h : 0 ≤ n), 0 < eval (n - HSub.hSub (α := ℕ) 0 1) (ascPochhammer ℕ 0)
Tactic: obtain rfl | h' := Nat.eq_zero_or_pos ν
Cleared hypotheses: ν, h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
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)
⊢ 0 < eval (n - (ν - 1)) (ascPochhammer ℕ ν)
have h₂ : ∀ (h' : ν > 0), 0 < eval (n - (ν - 1)) (ascPochhammer ℕ ν)
Tactic: obtain rfl | h' := Nat.eq_zero_or_pos ν
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
n ν : ℕ
h : ν ≤ n
h' : ν > 0
⊢ 0 < eval (n - (ν - 1)) (ascPochhammer ℕ ν)
have h₁ : ν.pred.succ ≤ n
Tactic: rw [← Nat.succ_pred_eq_of_pos h'] at h
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
n ν k : ℕ
w : k < n - ν
⊢ eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k] (bernsteinPolynomial R n ν)) = 0
have rw : eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k] (comp (bernsteinPolynomial R n (n - ν)) (HSub.hSub (α := R[X]) 1 X))) = 0
Tactic: rw [flip' _ _ _ (tsub_pos_iff_lt.mp (pos_of_gt w)).le]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
h : ν ≤ 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 - ν))
have 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 - ν))
Tactic: rw [flip' _ _ _ h]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
h : ν ≤ 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 - ν))
have 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 - ν))
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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
h : ν ≤ n
⊢ 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 - ν))
have inl : ∀ (h : ν ≤ ν),
  HPow.hPow (α := R) (-1) (ν - ν) * eval (↑(ν - (ν - ν - 1)) : R) (ascPochhammer R (ν - ν)) =
    HPow.hPow (α := R) (-1) (ν - ν) * eval (HAdd.hAdd (α := R) (↑ν : R) 1) (ascPochhammer R (ν - ν))
Tactic: obtain rfl | h' := h.eq_or_lt
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
h : ν ≤ n
inl :
  ∀ (h : ν ≤ ν),
    HPow.hPow (α := R) (-1) (ν - ν) * eval (↑(ν - (ν - ν - 1)) : R) (ascPochhammer R (ν - ν)) =
      HPow.hPow (α := R) (-1) (ν - ν) * eval (HAdd.hAdd (α := R) (↑ν : R) 1) (ascPochhammer R (ν - ν))
⊢ 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 - ν))
have inr : ∀ (h' : ν < n),
  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 - ν))
Tactic: obtain rfl | h' := h.eq_or_lt
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
h : ν ≤ n
h' : ν < n
⊢ 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 - ν))
have inr : HMul.hMul (α := R) (↑(Int.negSucc 0 ^ (n - ν)) : R) (↑(eval (n - (n - ν - 1)) (ascPochhammer ℕ (n - ν))) : R) =
  HMul.hMul (α := R) (↑(Int.negSucc 0 ^ (n - ν)) : R) (↑(eval (ν + 1) (ascPochhammer ℕ (n - ν))) : R)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
h : ν ≤ n
h' : ν < n
⊢ HMul.hMul (α := R) (↑(Int.negSucc 0 ^ (n - ν)) : R) (↑(eval (n - (n - ν - 1)) (ascPochhammer ℕ (n - ν))) : R) =
    HMul.hMul (α := R) (↑(Int.negSucc 0 ^ (n - ν)) : R) (↑(eval (ν + 1) (ascPochhammer ℕ (n - ν))) : R)
have inr : n - (n - ν - 1) = ν + 1
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ eval 1 ((⇑derivative : (a : R[X]) → R[X])^[n - ν] (bernsteinPolynomial R n ν)) ≠ 0
have rw : ¬eval ν.succ (ascPochhammer ℕ (n - ν)) = 0
Tactic: rw [bernsteinPolynomial.iterate_derivative_at_1 _ _ _ h, Ne, neg_one_pow_mul_eq_zero_iff, ←
    Nat.cast_succ, ← ascPochhammer_eval_cast, ← Nat.cast_zero, Nat.cast_inj]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
n k : ℕ
ih : ∀ (h : k ≤ n + 1), LinearIndependent ℚ (M := ℚ[X]) fun (ν : Fin k) ↦ bernsteinPolynomial ℚ n (↑ν : ℕ)
h : k + 1 ≤ n + 1
⊢ LinearIndependent ℚ (M := ℚ[X]) fun (ν : Fin (k + 1)) ↦ bernsteinPolynomial ℚ n (↑ν : ℕ)
have succ : LinearIndependent (ι := Fin k) ℚ (M := ℚ[X])
    (Fin.init (α := fun (i : Fin (k + 1)) ↦ ℚ[X]) fun (ν : Fin (k + 1)) ↦ bernsteinPolynomial ℚ n (↑ν : ℕ)) ∧
  bernsteinPolynomial ℚ n (↑(Fin.last k) : ℕ) ∉
    span ℚ
      (Set.range (ι := Fin k)
        (Fin.init (α := fun (i : Fin (k + 1)) ↦ ℚ[X]) fun (ν : Fin (k + 1)) ↦ bernsteinPolynomial ℚ n (↑ν : ℕ)))
Tactic: apply linearIndependent_finSucc'.mpr
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
n k : ℕ
ih : ∀ (h : k ≤ n + 1), LinearIndependent ℚ (M := ℚ[X]) fun (ν : Fin k) ↦ bernsteinPolynomial ℚ n (↑ν : ℕ)
h : k + 1 ≤ n + 1
⊢ LinearIndependent (ι := Fin k) ℚ (M := ℚ[X])
      (Fin.init (α := fun (i : Fin (k + 1)) ↦ ℚ[X]) fun (ν : Fin (k + 1)) ↦ bernsteinPolynomial ℚ n (↑ν : ℕ)) ∧
    bernsteinPolynomial ℚ n (↑(Fin.last k) : ℕ) ∉
      span ℚ
        (Set.range (ι := Fin k)
          (Fin.init (α := fun (i : Fin (k + 1)) ↦ ℚ[X]) fun (ν : Fin (k + 1)) ↦ bernsteinPolynomial ℚ n (↑ν : ℕ)))
have succ : LinearIndependent (ι := Fin k) ℚ (M := ℚ[X])
  (Fin.init (α := fun (i : Fin (k + 1)) ↦ ℚ[X]) fun (ν : Fin (k + 1)) ↦ bernsteinPolynomial ℚ n (↑ν : ℕ))
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
n k : ℕ
ih : ∀ (h : k ≤ n + 1), LinearIndependent ℚ (M := ℚ[X]) fun (ν : Fin k) ↦ bernsteinPolynomial ℚ n (↑ν : ℕ)
h : k + 1 ≤ n + 1
succ :
  LinearIndependent (ι := Fin k) ℚ (M := ℚ[X])
    (Fin.init (α := fun (i : Fin (k + 1)) ↦ ℚ[X]) fun (ν : Fin (k + 1)) ↦ bernsteinPolynomial ℚ n (↑ν : ℕ))
⊢ LinearIndependent (ι := Fin k) ℚ (M := ℚ[X])
      (Fin.init (α := fun (i : Fin (k + 1)) ↦ ℚ[X]) fun (ν : Fin (k + 1)) ↦ bernsteinPolynomial ℚ n (↑ν : ℕ)) ∧
    bernsteinPolynomial ℚ n (↑(Fin.last k) : ℕ) ∉
      span ℚ
        (Set.range (ι := Fin k)
          (Fin.init (α := fun (i : Fin (k + 1)) ↦ ℚ[X]) fun (ν : Fin (k + 1)) ↦ bernsteinPolynomial ℚ n (↑ν : ℕ)))
have succ₁ : bernsteinPolynomial ℚ n (↑(Fin.last k) : ℕ) ∉
  span ℚ
    (Set.range (ι := Fin k)
      (Fin.init (α := fun (i : Fin (k + 1)) ↦ ℚ[X]) fun (ν : Fin (k + 1)) ↦ bernsteinPolynomial ℚ n (↑ν : ℕ)))
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (hypothesis)
Goal:
n k : ℕ
h : k + 1 ≤ n + 1
⊢ bernsteinPolynomial ℚ n (↑(Fin.last k) : ℕ) ∉
    span ℚ
      (Set.range (ι := Fin k)
        (Fin.init (α := fun (i : Fin (k + 1)) ↦ ℚ[X]) fun (ν : Fin (k + 1)) ↦ bernsteinPolynomial ℚ n (↑ν : ℕ)))
have h₁ : k ≤ n
Tactic: simp only [add_le_add_iff_right] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
n k : ℕ
h : k ≤ n
⊢ bernsteinPolynomial ℚ n (↑(Fin.last k) : ℕ) ∉
    span ℚ
      (Set.range (ι := Fin k)
        (Fin.init (α := fun (i : Fin (k + 1)) ↦ ℚ[X]) fun (ν : Fin (k + 1)) ↦ bernsteinPolynomial ℚ n (↑ν : ℕ)))
have succ : bernsteinPolynomial ℚ n k ∉ span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1.castSucc : ℕ))
Tactic: simp only [Fin.val_last, Fin.init_def]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
n k : ℕ
h : k ≤ n
⊢ bernsteinPolynomial ℚ n k ∉ span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1.castSucc : ℕ))
have succ : bernsteinPolynomial ℚ n k ∉ span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
n k : ℕ
h : k ≤ n
⊢ bernsteinPolynomial ℚ n k ∉ span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ))
have succ : ((HPow.hPow (α := ℚ[X] →ₗ[ℚ] ℚ[X]) derivative (n - k) : (a : ℚ[X]) → ℚ[X]) (bernsteinPolynomial ℚ n k) : ℚ[X]) ∉
  span ℚ
    (Set.image (α := ℚ[X]) (⇑(HPow.hPow (α := ℚ[X] →ₗ[ℚ] ℚ[X]) derivative (n - k)) : (a : ℚ[X]) → ℚ[X])
      (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ)))
Tactic: apply notMem_span_of_apply_notMem_span_image (@Polynomial.derivative ℚ _ ^ (n - k))
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
n k : ℕ
h : k ≤ n
⊢ ((HPow.hPow (α := ℚ[X] →ₗ[ℚ] ℚ[X]) derivative (n - k) : (a : ℚ[X]) → ℚ[X]) (bernsteinPolynomial ℚ n k) : ℚ[X]) ∉
    span ℚ
      (Set.image (α := ℚ[X]) (⇑(HPow.hPow (α := ℚ[X] →ₗ[ℚ] ℚ[X]) derivative (n - k)) : (a : ℚ[X]) → ℚ[X])
        (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ)))
have succ : ∀ (x : ℚ[X]),
  Membership.mem (γ := Submodule ℚ ℚ[X]) (span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ))) x →
    ¬Eq (α := ℚ[X]) ((HPow.hPow (α := ℚ[X] →ₗ[ℚ] ℚ[X]) derivative (n - k) : (a : ℚ[X]) → ℚ[X]) x : ℚ[X])
        ((HPow.hPow (α := ℚ[X] →ₗ[ℚ] ℚ[X]) derivative (n - k) : (a : ℚ[X]) → ℚ[X]) (bernsteinPolynomial ℚ n k) : ℚ[X])
Tactic: simp only [not_exists, not_and, Submodule.mem_map, Submodule.span_image _]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
n k : ℕ
h : k ≤ n
p : ℚ[X]
m : Membership.mem (γ := Submodule ℚ ℚ[X]) (span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ))) p
⊢ ¬Eq (α := ℚ[X]) ((HPow.hPow (α := ℚ[X] →ₗ[ℚ] ℚ[X]) derivative (n - k) : (a : ℚ[X]) → ℚ[X]) p : ℚ[X])
      ((HPow.hPow (α := ℚ[X] →ₗ[ℚ] ℚ[X]) derivative (n - k) : (a : ℚ[X]) → ℚ[X]) (bernsteinPolynomial ℚ n k) : ℚ[X])
have apply_fun : Ne (α := ℚ) (eval 1 ((HPow.hPow (α := ℚ[X] →ₗ[ℚ] ℚ[X]) derivative (n - k) : (a : ℚ[X]) → ℚ[X]) p))
  (eval 1 ((HPow.hPow (α := ℚ[X] →ₗ[ℚ] ℚ[X]) derivative (n - k) : (a : ℚ[X]) → ℚ[X]) (bernsteinPolynomial ℚ n k)))
Tactic: apply_fun Polynomial.eval (1 : ℚ)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
n k : ℕ
h : k ≤ n
p : ℚ[X]
m : Membership.mem (γ := Submodule ℚ ℚ[X]) (span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ))) p
⊢ Ne (α := ℚ) (eval 1 ((HPow.hPow (α := ℚ[X] →ₗ[ℚ] ℚ[X]) derivative (n - k) : (a : ℚ[X]) → ℚ[X]) p))
    (eval 1 ((HPow.hPow (α := ℚ[X] →ₗ[ℚ] ℚ[X]) derivative (n - k) : (a : ℚ[X]) → ℚ[X]) (bernsteinPolynomial ℚ n k)))
have simp : eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] p) ≠
  eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] (bernsteinPolynomial ℚ n k))
Tactic: simp only [Module.End.pow_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
n k : ℕ
h : k ≤ n
p : ℚ[X]
m : Membership.mem (γ := Submodule ℚ ℚ[X]) (span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ))) p
this : eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] p) = 0
⊢ eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] p) ≠
    eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] (bernsteinPolynomial ℚ n k))
have rw : 0 ≠ eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] (bernsteinPolynomial ℚ n k))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
n k : ℕ
h : k ≤ n
p : ℚ[X]
m : Membership.mem (γ := Submodule ℚ ℚ[X]) (span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ))) p
⊢ eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] p) ≠
    eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] (bernsteinPolynomial ℚ n k))
have suffices : eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] p) = 0
Tactic: suffices (Polynomial.derivative^[n - k] p).eval 1 = 0 by
        rw [this]
        exact (iterate_derivative_at_1_ne_zero ℚ n k h).symm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
n k : ℕ
h : k ≤ n
p : ℚ[X]
m : Membership.mem (γ := Submodule ℚ ℚ[X]) (span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ))) p
⊢ eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] p) = 0
have refine_1 : ∀ (x : ℚ[X]) (h : Membership.mem (γ := Set ℚ[X]) (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ)) x),
  eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] x) = 0
Tactic: refine span_induction ?_ ?_ ?_ ?_ m
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
n k : ℕ
h : k ≤ n
p : ℚ[X]
m : Membership.mem (γ := Submodule ℚ ℚ[X]) (span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ))) p
refine_1 :
  ∀ (x : ℚ[X])
    (h : Membership.mem (γ := Set ℚ[X]) (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ)) x),
    eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] x) = 0
⊢ eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] p) = 0
have refine_2 : Eq (α := ℚ) (eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] 0)) 0
Tactic: refine span_induction ?_ ?_ ?_ ?_ m