awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
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 (ν - ν))
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 - ν))
⊢ 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

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
ν : ℕ
h : ν ≤ ν
⊢ HPow.hPow (α := R) (-1) (ν - ν) * eval (↑(ν - (ν - ν - 1)) : R) (ascPochhammer R (ν - ν)) =
    HPow.hPow (α := R) (-1) (ν - ν) * eval (HAdd.hAdd (α := R) (↑ν : R) 1) (ascPochhammer R (ν - ν))

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
h : ν ≤ n
h' : ν < n
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)
⊢ 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:
norm_cast
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
h : ν ≤ n
h' : ν < n
inr : n - (n - ν - 1) = ν + 1
⊢ 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:
congr
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
h : ν ≤ n
h' : ν < n
⊢ n - (n - ν - 1) = ν + 1

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
n ν : ℕ
h : ν ≤ n
rw : ¬eval ν.succ (ascPochhammer ℕ (n - ν)) = 0
⊢ eval 1 ((⇑derivative : (a : R[X]) → R[X])^[n - ν] (bernsteinPolynomial R 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]

Premises used: Nat.cast_succ, Ne, Nat.cast_inj, ascPochhammer_eval_cast, Nat.cast_zero, neg_one_pow_mul_eq_zero_iff, bernsteinPolynomial.iterate_derivative_at_1
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ ¬eval ν.succ (ascPochhammer ℕ (n - ν)) = 0

Tactic:
(ascPochhammer_pos _ _ (Nat.succ_pos ν)).ne'

Premises used: LT.lt.ne', ascPochhammer_pos, Nat.succ_pos
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ ¬eval ν.succ (ascPochhammer ℕ (n - ν)) = 0

Tactic:
exact (ascPochhammer_pos _ _ (Nat.succ_pos ν)).ne'

Premises used: LT.lt.ne', ascPochhammer_pos, Nat.succ_pos
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
n : ℕ
h : 0 ≤ n + 1
⊢ LinearIndependent ℚ (M := ℚ[X]) fun (ν : Fin 0) ↦ bernsteinPolynomial ℚ n (↑ν : ℕ)

Tactic:
apply linearIndependent_empty_type

Premises used: linearIndependent_empty_type
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
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 (↑ν : ℕ)) ∧
    bernsteinPolynomial ℚ n (↑(Fin.last k) : ℕ) ∉
      span ℚ
        (Set.range (ι := Fin k)
          (Fin.init (α := fun (i : Fin (k + 1)) ↦ ℚ[X]) fun (ν : Fin (k + 1)) ↦ bernsteinPolynomial ℚ n (↑ν : ℕ)))
⊢ LinearIndependent ℚ (M := ℚ[X]) fun (ν : Fin (k + 1)) ↦ bernsteinPolynomial ℚ n (↑ν : ℕ)

Tactic:
apply linearIndependent_finSucc'.mpr

Premises used: Iff.mpr, linearIndependent_finSucc'
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
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 (↑ν : ℕ))
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 (↑ν : ℕ)))
⊢ 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:
fconstructor
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
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 (↑ν : ℕ))

Tactic:
ih (le_of_lt h)

Premises used: le_of_lt, Fin.init, bernsteinPolynomial
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
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 (↑ν : ℕ))

Tactic:
exact ih (le_of_lt h)

Premises used: le_of_lt
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
n k : ℕ
h : k + 1 ≤ n + 1
⊢ k ≤ n

Tactic:
simp only [add_le_add_iff_right] at h

Premises used: add_le_add_iff_right
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
n k : ℕ
h : k ≤ n
succ : bernsteinPolynomial ℚ n k ∉ span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1.castSucc : ℕ))
⊢ 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:
simp only [Fin.val_last, Fin.init_def]

Premises used: Fin.init_def, Fin.val_last
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
n k : ℕ
h : k ≤ n
succ : bernsteinPolynomial ℚ n k ∉ span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ))
⊢ bernsteinPolynomial ℚ n k ∉ span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1.castSucc : ℕ))

Tactic:
dsimp
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
n k : ℕ
h : k ≤ n
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 : ℕ)))
⊢ bernsteinPolynomial ℚ n k ∉ span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ))

Tactic:
apply notMem_span_of_apply_notMem_span_image (@Polynomial.derivative ℚ _ ^ (n - k))

Premises used: Polynomial.derivative, HSub.hSub, HPow.hPow, Submodule.notMem_span_of_apply_notMem_span_image
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
n k : ℕ
h : k ≤ n
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])
⊢ ((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:
simp only [not_exists, not_and, Submodule.mem_map, Submodule.span_image _]

Premises used: Submodule.mem_map, not_exists, Submodule.span_image, not_and
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
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
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)))
⊢ ¬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])

Tactic:
apply_fun Polynomial.eval (1 : ℚ)

Premises used: Polynomial.eval, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
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
simp :
  eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] p) ≠
    eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] (bernsteinPolynomial ℚ n k))
⊢ 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:
simp only [Module.End.pow_apply]

Premises used: Module.End.pow_apply
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
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
rw : 0 ≠ eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] (bernsteinPolynomial ℚ n k))
⊢ eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] p) ≠
    eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] (bernsteinPolynomial ℚ n k))

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
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
⊢ 0 ≠ eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] (bernsteinPolynomial ℚ n k))

Tactic:
(iterate_derivative_at_1_ne_zero ℚ n k h).symm

Premises used: Rat, Ne.symm, bernsteinPolynomial.iterate_derivative_at_1_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
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
⊢ 0 ≠ eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] (bernsteinPolynomial ℚ n k))

Tactic:
exact (iterate_derivative_at_1_ne_zero ℚ n k h).symm

Premises used: Rat, Ne.symm, bernsteinPolynomial.iterate_derivative_at_1_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
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
suffices : 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))

Tactic:
suffices (Polynomial.derivative^[n - k] p).eval 1 = 0 by
        rw [this]
        exact (iterate_derivative_at_1_ne_zero ℚ n k h).symm
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
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

Tactic:
span_induction ?_ ?_ ?_ ?_ m

Premises used: Submodule.span_induction
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
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
refine_2 : Eq (α := ℚ) (eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] 0)) 0
refine_3 :
  ∀ (x y : ℚ[X])
    (hx :
      Membership.mem (γ := Submodule ℚ ℚ[X]) (span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ)))
        x)
    (hy :
      Membership.mem (γ := Submodule ℚ ℚ[X]) (span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ)))
        y),
    eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] x) = 0 →
      eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] y) = 0 →
        eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] (x + y)) = 0
refine_4 :
  ∀ (a : ℚ) (x : ℚ[X])
    (hx :
      Membership.mem (γ := Submodule ℚ ℚ[X]) (span ℚ (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] (a • x)) = 0
⊢ eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] p) = 0

Tactic:
refine span_induction ?_ ?_ ?_ ?_ m
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
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 : ∀ (a : Fin k), eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] (bernsteinPolynomial ℚ n (↑a : ℕ))) = 0
⊢ ∀ (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:
simp only [Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff]

Premises used: Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
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
a : ℕ
w : a < k
refine_1 : eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] (bernsteinPolynomial ℚ n a)) = 0
⊢ eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] (bernsteinPolynomial ℚ n (↑(⟨a, w⟩ : Fin k) : ℕ))) = 0

Tactic:
simp only
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
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
a : ℕ
w : a < k
refine_1 refine_1₁ : Eq (α := ℚ) 0 0
⊢ eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] (bernsteinPolynomial ℚ n a)) = 0

Tactic:
rw [iterate_derivative_at_1_eq_zero_of_lt ℚ n ((tsub_lt_tsub_iff_left_of_le h).mpr w)]

Premises used: Iff.mpr, tsub_lt_tsub_iff_left_of_le, Rat, bernsteinPolynomial.iterate_derivative_at_1_eq_zero_of_lt
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
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 (α := ℚ) (eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] 0)) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
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
x y : ℚ[X]
refine_3 :
  Membership.mem (γ := Submodule ℚ ℚ[X]) (span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ))) x →
    ∀
      (hy :
        Membership.mem (γ := Submodule ℚ ℚ[X])
          (span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ))) y),
      eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] x) = 0 →
        eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] y) = 0 →
          eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] (x + y)) = 0
⊢ ∀
    (hx :
      Membership.mem (γ := Submodule ℚ ℚ[X]) (span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ)))
        x)
    (hy :
      Membership.mem (γ := Submodule ℚ ℚ[X]) (span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ)))
        y),
    eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] x) = 0 →
      eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] y) = 0 →
        eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] (x + y)) = 0

Tactic:
_
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
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
x y : ℚ[X]
hx :
  Membership.mem (γ := Submodule ℚ ℚ[X]) (span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ))) x
refine_3 :
  Membership.mem (γ := Submodule ℚ ℚ[X]) (span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ))) y →
    eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] x) = 0 →
      eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] y) = 0 →
        eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] (x + y)) = 0
⊢ ∀
    (hy :
      Membership.mem (γ := Submodule ℚ ℚ[X]) (span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ)))
        y),
    eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] x) = 0 →
      eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] y) = 0 →
        eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] (x + y)) = 0

Tactic:
_
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
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
x y : ℚ[X]
hx_1 :
  Membership.mem (γ := Submodule ℚ ℚ[X]) (span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ))) x
hy_1 :
  Membership.mem (γ := Submodule ℚ ℚ[X]) (span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ))) y
hx : eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] x) = 0
hy : eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] y) = 0
⊢ eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] (x + y)) = 0

Tactic:
simp [hx, hy]
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
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
a : ℚ
x : ℚ[X]
refine_4 :
  Membership.mem (γ := Submodule ℚ ℚ[X]) (span ℚ (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] (a • x)) = 0
⊢ ∀
    (hx :
      Membership.mem (γ := Submodule ℚ ℚ[X]) (span ℚ (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] (a • x)) = 0

Tactic:
_
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
n k : ℕ
h_1 : k ≤ n
p : ℚ[X]
m : Membership.mem (γ := Submodule ℚ ℚ[X]) (span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ))) p
a : ℚ
x : ℚ[X]
hx :
  Membership.mem (γ := Submodule ℚ ℚ[X]) (span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ))) x
h : eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] x) = 0
⊢ eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] (a • x)) = 0

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
n k : ℕ
h : k ≤ n + 1
zero : ∀ (h : 0 ≤ n + 1), LinearIndependent ℚ (M := ℚ[X]) fun (ν : Fin 0) ↦ bernsteinPolynomial ℚ n (↑ν : ℕ)
succ :
  ∀ (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 (↑ν : ℕ)
⊢ LinearIndependent ℚ (M := ℚ[X]) fun (ν : Fin k) ↦ bernsteinPolynomial ℚ n (↑ν : ℕ)

Tactic:
induction k with
  | zero => apply linearIndependent_empty_type
  | succ k ih =>
    apply linearIndependent_finSucc'.mpr
    fconstructor
    · exact ih (le_of_lt h)
    · -- The actual work!
      -- We show that the (n-k)-th derivative at 1 doesn't vanish,
      -- but vanishes for everything in the span.
      clear ih
      simp only [add_le_add_iff_right] at h
      simp only [Fin.val_last, Fin.init_def]
      dsimp
      apply notMem_span_of_apply_notMem_span_image (@Polynomial.derivative ℚ _ ^ (n - k))
      -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to change `span_image` into `span_image _`
      simp only [not_exists, not_and, Submodule.mem_map, Submodule.span_image _]
      intro p m
      apply_fun Polynomial.eval (1 : ℚ)
      simp only [Module.End.pow_apply]
      -- The right-hand side is nonzero,
      -- so it will suffice to show the left-hand side is always zero.
      suffices (Polynomial.derivative^[n - k] p).eval 1 = 0 by
        rw [this]
        exact (iterate_derivative_at_1_ne_zero ℚ n k h).symm
      refine span_induction ?_ ?_ ?_ ?_ m
      · simp only [Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff]
        rintro ⟨a, w⟩; simp only
        rw [iterate_derivative_at_1_eq_zero_of_lt ℚ n ((tsub_lt_tsub_iff_left_of_le h).mpr w)]
      · simp
      · intro x y _ _ hx hy; simp [hx, hy]
      · intro a x _ h; simp [h]

Premises used: Fin.init_def, Iff.mpr, Polynomial.derivative, Polynomial.eval, Set.mem_range, linearIndependent_empty_type, Submodule.mem_map, linearIndependent_finSucc', HSub.hSub, forall_exists_index, not_exists, Module.End.pow_apply, add_le_add_iff_right, HPow.hPow, Submodule.zero, Submodule.span_image, OfNat.ofNat, Submodule.notMem_span_of_apply_notMem_span_image, forall_apply_eq_imp_iff, not_and, Fin.val_last
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
n : ℕ
⊢ LinearIndependent ℚ (M := ℚ[X]) fun (ν : Fin (n + 1)) ↦ bernsteinPolynomial ℚ n (↑ν : ℕ)

Tactic:
linearIndependent_aux n (n + 1) le_rfl

Premises used: le_rfl, bernsteinPolynomial.linearIndependent_aux, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
rw :
  Eq.{u_1 + 1} (α := R[X]) (∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν)
    (∑ m ∈ Finset.range (n + 1),
      HPow.hPow (α := R[X]) X m * HSub.hSub (α := R[X]) 1 X ^ (n - m) * (↑(n.choose m) : R[X]))
⊢ ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν = (X + HSub.hSub (α := R[X]) 1 X) ^ n

Tactic:
rw [add_pow]

Premises used: add_pow
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R[X]) (∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν)
    (∑ m ∈ Finset.range (n + 1),
      HPow.hPow (α := R[X]) X m * HSub.hSub (α := R[X]) 1 X ^ (n - m) * (↑(n.choose m) : R[X]))

Tactic:
simp only [bernsteinPolynomial, mul_comm, mul_assoc]

Premises used: mul_assoc, bernsteinPolynomial, mul_comm
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
⊢ (X + HSub.hSub (α := R[X]) 1 X) ^ n = 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
rw :
  Eq.{u_1 + 1} (α := MvPolynomial Bool R)
    (Pi.single (M := fun (x : Bool) ↦ MvPolynomial Bool R) true 1 true : MvPolynomial Bool R) (1 : MvPolynomial Bool R)
⊢ Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) x : MvPolynomial Bool R) (1 : MvPolynomial Bool R)

Tactic:
rw [pderiv_X]

Premises used: MvPolynomial.pderiv_X