-- Mathlib/RingTheory/Polynomial/Bernstein.lean
theorem linearIndependent_aux (n k : ℕ) (h : k ≤ n + 1) :
    LinearIndependent ℚ fun ν : Fin k => bernsteinPolynomial ℚ n ν

Proof state:
n k : ℕ
h : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)
this : eval 1 ((⇑derivative)^[n - k] p) = 0
⊢ eval 1 ((⇑derivative)^[n - k] p) ≠ eval 1 ((⇑derivative)^[n - k] (bernsteinPolynomial ℚ n k))

Tactic:
rw [this]

Result:
n k : ℕ
h : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)
this : eval 1 ((⇑derivative)^[n - k] p) = 0
⊢ 0 ≠ eval 1 ((⇑derivative)^[n - k] (bernsteinPolynomial ℚ n k))

Proof state:
case succ.right
n k : ℕ
h : k ≤ n
⊢ bernsteinPolynomial ℚ n k ∉ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1.castSucc)

Tactic:
dsimp

Result:
case succ.right
n k : ℕ
h : k ≤ n
⊢ bernsteinPolynomial ℚ n k ∉ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)

Proof state:
case succ
n k : ℕ
ih : k ≤ n + 1 → LinearIndependent ℚ fun ν => bernsteinPolynomial ℚ n ↑ν
h : k + 1 ≤ n + 1
⊢ LinearIndependent ℚ (Fin.init fun ν => bernsteinPolynomial ℚ n ↑ν) ∧
    bernsteinPolynomial ℚ n ↑(Fin.last k) ∉ span ℚ (Set.range (Fin.init fun ν => bernsteinPolynomial ℚ n ↑ν))

Tactic:
fconstructor

Result:
case succ.left
n k : ℕ
ih : k ≤ n + 1 → LinearIndependent ℚ fun ν => bernsteinPolynomial ℚ n ↑ν
h : k + 1 ≤ n + 1
⊢ LinearIndependent ℚ (Fin.init fun ν => bernsteinPolynomial ℚ n ↑ν)

case succ.right
n k : ℕ
ih : k ≤ n + 1 → LinearIndependent ℚ fun ν => bernsteinPolynomial ℚ n ↑ν
h : k + 1 ≤ n + 1
⊢ bernsteinPolynomial ℚ n ↑(Fin.last k) ∉ span ℚ (Set.range (Fin.init fun ν => bernsteinPolynomial ℚ n ↑ν))

Proof state:
case succ
n k : ℕ
ih : k ≤ n + 1 → LinearIndependent ℚ fun ν => bernsteinPolynomial ℚ n ↑ν
h : k + 1 ≤ n + 1
⊢ LinearIndependent ℚ fun ν => bernsteinPolynomial ℚ n ↑ν

Tactic:
apply linearIndependent_fin_succ'.mpr

Result:
case succ
n k : ℕ
ih : k ≤ n + 1 → LinearIndependent ℚ fun ν => bernsteinPolynomial ℚ n ↑ν
h : k + 1 ≤ n + 1
⊢ LinearIndependent ℚ (Fin.init fun ν => bernsteinPolynomial ℚ n ↑ν) ∧
    bernsteinPolynomial ℚ n ↑(Fin.last k) ∉ span ℚ (Set.range (Fin.init fun ν => bernsteinPolynomial ℚ n ↑ν))

Proof state:
case refine_1
n k : ℕ
h : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)
⊢ ∀ (a : Fin k), eval 1 ((⇑derivative)^[n - k] (bernsteinPolynomial ℚ n ↑a)) = 0

Tactic:
rintro ⟨a, w⟩

Result:
case refine_1.mk
n k : ℕ
h : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)
a : ℕ
w : a < k
⊢ eval 1 ((⇑derivative)^[n - k] (bernsteinPolynomial ℚ n ↑⟨a, w⟩)) = 0

Proof state:
n k : ℕ
h : k ≤ n + 1
⊢ LinearIndependent ℚ fun ν => bernsteinPolynomial ℚ n ↑ν

Tactic:
induction' k with k ih

Result:
case zero
n : ℕ
h : 0 ≤ n + 1
⊢ LinearIndependent ℚ fun ν => bernsteinPolynomial ℚ n ↑ν

case succ
n k : ℕ
ih : k ≤ n + 1 → LinearIndependent ℚ fun ν => bernsteinPolynomial ℚ n ↑ν
h : k + 1 ≤ n + 1
⊢ LinearIndependent ℚ fun ν => bernsteinPolynomial ℚ n ↑ν

Proof state:
case zero
n : ℕ
h : 0 ≤ n + 1
⊢ LinearIndependent ℚ fun ν => bernsteinPolynomial ℚ n ↑ν

Tactic:
apply linearIndependent_empty_type

Result:
no goals

Proof state:
case refine_1.mk
n k : ℕ
h : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)
a : ℕ
w : a < k
⊢ eval 1 ((⇑derivative)^[n - k] (bernsteinPolynomial ℚ n ↑⟨a, w⟩)) = 0

Tactic:
simp only [Fin.val_mk]

Result:
case refine_1.mk
n k : ℕ
h : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)
a : ℕ
w : a < k
⊢ eval 1 ((⇑derivative)^[n - k] (bernsteinPolynomial ℚ n a)) = 0

Proof state:
case succ.right
n k : ℕ
h : k ≤ n
⊢ (derivative ^ (n - k)) (bernsteinPolynomial ℚ n k) ∉
    span ℚ (⇑(derivative ^ (n - k)) '' Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)

Tactic:
simp only [not_exists, not_and, Submodule.mem_map, Submodule.span_image _]

Result:
case succ.right
n k : ℕ
h : k ≤ n
⊢ ∀ x ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1),
    ¬(derivative ^ (n - k)) x = (derivative ^ (n - k)) (bernsteinPolynomial ℚ n k)

Proof state:
n k : ℕ
h : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)
this : eval 1 ((⇑derivative)^[n - k] p) = 0
⊢ 0 ≠ eval 1 ((⇑derivative)^[n - k] (bernsteinPolynomial ℚ n k))

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

Result:
no goals

Proof state:
case succ.right
n k : ℕ
h : k ≤ n
⊢ bernsteinPolynomial ℚ n ↑(Fin.last k) ∉ span ℚ (Set.range (Fin.init fun ν => bernsteinPolynomial ℚ n ↑ν))

Tactic:
simp only [Fin.val_last, Fin.init_def]

Result:
case succ.right
n k : ℕ
h : k ≤ n
⊢ bernsteinPolynomial ℚ n k ∉ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1.castSucc)

Proof state:
case refine_2
n k : ℕ
h : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)
⊢ eval 1 ((⇑derivative)^[n - k] 0) = 0

Tactic:
simp

Result:
no goals

Proof state:
n k : ℕ
h : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)
⊢ eval 1 ((derivative ^ (n - k)) p) ≠ eval 1 ((derivative ^ (n - k)) (bernsteinPolynomial ℚ n k))

Tactic:
simp only [LinearMap.pow_apply]

Result:
n k : ℕ
h : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)
⊢ eval 1 ((⇑derivative)^[n - k] p) ≠ eval 1 ((⇑derivative)^[n - k] (bernsteinPolynomial ℚ n k))

Proof state:
case succ.right
n k : ℕ
h : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)
⊢ ¬(derivative ^ (n - k)) p = (derivative ^ (n - k)) (bernsteinPolynomial ℚ n k)

Tactic:
apply_fun Polynomial.eval (1 : ℚ)

Result:
n k : ℕ
h : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)
⊢ eval 1 ((derivative ^ (n - k)) p) ≠ eval 1 ((derivative ^ (n - k)) (bernsteinPolynomial ℚ n k))

Proof state:
case refine_4
n k : ℕ
h : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)
⊢ ∀ (a : ℚ),
    ∀ x ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1),
      eval 1 ((⇑derivative)^[n - k] x) = 0 → eval 1 ((⇑derivative)^[n - k] (a • x)) = 0

Tactic:
intro a x _ h

Result:
case refine_4
n k : ℕ
h✝ : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)
a : ℚ
x : ℚ[X]
hx✝ : x ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)
h : eval 1 ((⇑derivative)^[n - k] x) = 0
⊢ eval 1 ((⇑derivative)^[n - k] (a • x)) = 0

Proof state:
case refine_4
n k : ℕ
h✝ : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)
a : ℚ
x : ℚ[X]
hx✝ : x ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)
h : eval 1 ((⇑derivative)^[n - k] x) = 0
⊢ eval 1 ((⇑derivative)^[n - k] (a • x)) = 0

Tactic:
simp [h]

Result:
no goals

Proof state:
case refine_3
n k : ℕ
h : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)
x y : ℚ[X]
hx✝ : x ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)
hy✝ : y ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)
hx : eval 1 ((⇑derivative)^[n - k] x) = 0
hy : eval 1 ((⇑derivative)^[n - k] y) = 0
⊢ eval 1 ((⇑derivative)^[n - k] (x + y)) = 0

Tactic:
simp [hx, hy]

Result:
no goals

Proof state:
case succ.right
n k : ℕ
h : k ≤ n
⊢ bernsteinPolynomial ℚ n k ∉ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)

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

Result:
case succ.right
n k : ℕ
h : k ≤ n
⊢ (derivative ^ (n - k)) (bernsteinPolynomial ℚ n k) ∉
    span ℚ (⇑(derivative ^ (n - k)) '' Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)

Proof state:
case refine_1.mk
n k : ℕ
h : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)
a : ℕ
w : a < k
⊢ eval 1 ((⇑derivative)^[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)]

Result:
no goals