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

Proof state:
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)

Tactic:
intro p m

Result:
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)

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

Tactic:
simp only [Nat.succ_eq_add_one, add_le_add_iff_right] at h

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

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

Tactic:
exact ih (le_of_lt h)

Result:
no goals

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

Tactic:
simp only [Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff]

Result:
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

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]),
    x ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1) →
      y ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1) →
        eval 1 ((⇑derivative)^[n - k] x) = 0 →
          eval 1 ((⇑derivative)^[n - k] y) = 0 → eval 1 ((⇑derivative)^[n - k] (x + y)) = 0

Tactic:
intro x y _ _ hx hy

Result:
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

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

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) = 0

Proof state:
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 ↑ν))

Tactic:
clear ih

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

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) = 0

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

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

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

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]),
    x ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1) →
      y ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1) →
        eval 1 ((⇑derivative)^[n - k] x) = 0 →
          eval 1 ((⇑derivative)^[n - k] y) = 0 → eval 1 ((⇑derivative)^[n - k] (x + y)) = 0

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