case zero
R : Type ?u.195275
inst✝ : CommRing R
n k : ℕ
h✝ : k ≤ n + 1
h : Nat.zero ≤ n + 1
⊢ LinearIndependent ℚ fun ν => bernsteinPolynomial ℚ n ↑ν

case succ
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
k : ℕ
ih : k ≤ n + 1 → LinearIndependent ℚ fun ν => bernsteinPolynomial ℚ n ↑ν
h : Nat.succ k ≤ n + 1
⊢ LinearIndependent ℚ fun ν => bernsteinPolynomial ℚ n ↑ν
R : Type ?u.195275
inst✝ : CommRing R
n k : ℕ
h : k ≤ n + 1
⊢ LinearIndependent ℚ fun ν => bernsteinPolynomial ℚ n ↑ν
induction' k with k ih
case zero
R : Type ?u.195275
inst✝ : CommRing R
n k : ℕ
h✝ : k ≤ n + 1
h : Nat.zero ≤ n + 1
⊢ LinearIndependent ℚ fun ν => bernsteinPolynomial ℚ n ↑ν
case zero
R : Type ?u.195275
inst✝ : CommRing R
n k : ℕ
h✝ : k ≤ n + 1
h : Nat.zero ≤ n + 1
⊢ LinearIndependent ℚ fun ν => bernsteinPolynomial ℚ n ↑ν
simp [Nat.zero_eq]
no goals
case zero
R : Type ?u.195275
inst✝ : CommRing R
n k : ℕ
h✝ : k ≤ n + 1
h : Nat.zero ≤ n + 1
⊢ LinearIndependent ℚ fun ν => bernsteinPolynomial ℚ n ↑ν
apply linearIndependent_empty_type
case succ
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
k : ℕ
ih : k ≤ n + 1 → LinearIndependent ℚ fun ν => bernsteinPolynomial ℚ n ↑ν
h : Nat.succ k ≤ n + 1
⊢ LinearIndependent ℚ (Fin.init fun ν => bernsteinPolynomial ℚ n ↑ν) ∧
    ¬bernsteinPolynomial ℚ n ↑(Fin.last k) ∈ span ℚ (Set.range (Fin.init fun ν => bernsteinPolynomial ℚ n ↑ν))
case succ
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
k : ℕ
ih : k ≤ n + 1 → LinearIndependent ℚ fun ν => bernsteinPolynomial ℚ n ↑ν
h : Nat.succ k ≤ n + 1
⊢ LinearIndependent ℚ fun ν => bernsteinPolynomial ℚ n ↑ν
apply linearIndependent_fin_succ'.mpr
case succ.left
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
k : ℕ
ih : k ≤ n + 1 → LinearIndependent ℚ fun ν => bernsteinPolynomial ℚ n ↑ν
h : Nat.succ k ≤ n + 1
⊢ LinearIndependent ℚ (Fin.init fun ν => bernsteinPolynomial ℚ n ↑ν)

case succ.right
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
k : ℕ
ih : k ≤ n + 1 → LinearIndependent ℚ fun ν => bernsteinPolynomial ℚ n ↑ν
h : Nat.succ k ≤ n + 1
⊢ ¬bernsteinPolynomial ℚ n ↑(Fin.last k) ∈ span ℚ (Set.range (Fin.init fun ν => bernsteinPolynomial ℚ n ↑ν))
case succ
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
k : ℕ
ih : k ≤ n + 1 → LinearIndependent ℚ fun ν => bernsteinPolynomial ℚ n ↑ν
h : Nat.succ k ≤ n + 1
⊢ LinearIndependent ℚ (Fin.init fun ν => bernsteinPolynomial ℚ n ↑ν) ∧
    ¬bernsteinPolynomial ℚ n ↑(Fin.last k) ∈ span ℚ (Set.range (Fin.init fun ν => bernsteinPolynomial ℚ n ↑ν))
fconstructor
no goals
case succ.left
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
k : ℕ
ih : k ≤ n + 1 → LinearIndependent ℚ fun ν => bernsteinPolynomial ℚ n ↑ν
h : Nat.succ k ≤ n + 1
⊢ LinearIndependent ℚ (Fin.init fun ν => bernsteinPolynomial ℚ n ↑ν)
exact ih (le_of_lt h)
case succ.right
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
k : ℕ
h : Nat.succ k ≤ n + 1
⊢ ¬bernsteinPolynomial ℚ n ↑(Fin.last k) ∈ span ℚ (Set.range (Fin.init fun ν => bernsteinPolynomial ℚ n ↑ν))
case succ.right
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
k : ℕ
ih : k ≤ n + 1 → LinearIndependent ℚ fun ν => bernsteinPolynomial ℚ n ↑ν
h : Nat.succ k ≤ n + 1
⊢ ¬bernsteinPolynomial ℚ n ↑(Fin.last k) ∈ span ℚ (Set.range (Fin.init fun ν => bernsteinPolynomial ℚ n ↑ν))
clear ih
case succ.right
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
k : ℕ
h : k ≤ n
⊢ ¬bernsteinPolynomial ℚ n ↑(Fin.last k) ∈ span ℚ (Set.range (Fin.init fun ν => bernsteinPolynomial ℚ n ↑ν))
case succ.right
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
k : ℕ
h : Nat.succ k ≤ n + 1
⊢ ¬bernsteinPolynomial ℚ n ↑(Fin.last k) ∈ span ℚ (Set.range (Fin.init fun ν => bernsteinPolynomial ℚ n ↑ν))
simp only [Nat.succ_eq_add_one, add_le_add_iff_right] at h
case succ.right
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
k : ℕ
h : k ≤ n
⊢ ¬bernsteinPolynomial ℚ n k ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑(↑Fin.castSucc k_1))
case succ.right
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
k : ℕ
h : k ≤ n
⊢ ¬bernsteinPolynomial ℚ n ↑(Fin.last k) ∈ span ℚ (Set.range (Fin.init fun ν => bernsteinPolynomial ℚ n ↑ν))
simp only [Fin.val_last, Fin.init_def]
case succ.right
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
k : ℕ
h : k ≤ n
⊢ ¬bernsteinPolynomial ℚ n k ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)
case succ.right
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
k : ℕ
h : k ≤ n
⊢ ¬bernsteinPolynomial ℚ n k ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑(↑Fin.castSucc k_1))
dsimp
case succ.right
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
k : ℕ
h : k ≤ n
⊢ ¬↑(derivative ^ (n - k)) (bernsteinPolynomial ℚ n k) ∈
      span ℚ (↑(derivative ^ (n - k)) '' Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)
case succ.right
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
k : ℕ
h : k ≤ n
⊢ ¬bernsteinPolynomial ℚ n k ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)
apply not_mem_span_of_apply_not_mem_span_image (@Polynomial.derivative ℚ _ ^ (n - k))
case succ.right
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
k : ℕ
h : k ≤ n
⊢ ∀ (x : ℚ[X]),
    x ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1) →
      ¬↑(derivative ^ (n - k)) x = ↑(derivative ^ (n - k)) (bernsteinPolynomial ℚ n k)
case succ.right
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
k : ℕ
h : k ≤ n
⊢ ¬↑(derivative ^ (n - k)) (bernsteinPolynomial ℚ n k) ∈
      span ℚ (↑(derivative ^ (n - k)) '' Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)
simp only [not_exists, not_and, Submodule.mem_map, Submodule.span_image]
case succ.right
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
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)
case succ.right
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
k : ℕ
h : k ≤ n
⊢ ∀ (x : ℚ[X]),
    x ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1) →
      ¬↑(derivative ^ (n - k)) x = ↑(derivative ^ (n - k)) (bernsteinPolynomial ℚ n k)
intro p m
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
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))
case succ.right
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
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)
apply_fun Polynomial.eval (1 : ℚ)
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
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))
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
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))
simp only [LinearMap.pow_apply]
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
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
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
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))
suffices ((Polynomial.derivative^[n - k]) p).eval 1 = 0 by
  rw [this]
  exact (iterate_derivative_at_1_ne_zero ℚ n k h).symm
case refine_1
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
k : ℕ
h : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)
⊢ ∀ (x : ℚ[X]), (x ∈ Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1) → eval 1 ((↑derivative^[n - k]) x) = 0

case refine_2
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
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
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
k : ℕ
h : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)
⊢ ∀ (x y : ℚ[X]),
    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
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
k : ℕ
h : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)
⊢ ∀ (a : ℚ) (x : ℚ[X]), eval 1 ((↑derivative^[n - k]) x) = 0 → eval 1 ((↑derivative^[n - k]) (a • x)) = 0
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
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
refine span_induction m ?_ ?_ ?_ ?_
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
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))
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
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))
rw [this]
no goals
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
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))
exact (iterate_derivative_at_1_ne_zero ℚ n k h).symm
case refine_1
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
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
case refine_1
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
k : ℕ
h : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)
⊢ ∀ (x : ℚ[X]), (x ∈ Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1) → eval 1 ((↑derivative^[n - k]) x) = 0
simp
case refine_1.mk
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
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 ↑{ val := a, isLt := w })) = 0
case refine_1
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
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
rintro ⟨a, w⟩
case refine_1.mk
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
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
case refine_1.mk
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
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 ↑{ val := a, isLt := w })) = 0
simp only [Fin.val_mk]
no goals
case refine_1.mk
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
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
rw [iterate_derivative_at_1_eq_zero_of_lt ℚ n ((tsub_lt_tsub_iff_left_of_le h).mpr w)]
no goals
case refine_2
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
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
simp
case refine_3
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
k : ℕ
h : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)
x y : ℚ[X]
hx : eval 1 ((↑derivative^[n - k]) x) = 0
hy : eval 1 ((↑derivative^[n - k]) y) = 0
⊢ eval 1 ((↑derivative^[n - k]) (x + y)) = 0
case refine_3
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
k : ℕ
h : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)
⊢ ∀ (x y : ℚ[X]),
    eval 1 ((↑derivative^[n - k]) x) = 0 →
      eval 1 ((↑derivative^[n - k]) y) = 0 → eval 1 ((↑derivative^[n - k]) (x + y)) = 0
intro x y hx hy
no goals
case refine_3
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
k : ℕ
h : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)
x y : ℚ[X]
hx : eval 1 ((↑derivative^[n - k]) x) = 0
hy : eval 1 ((↑derivative^[n - k]) y) = 0
⊢ eval 1 ((↑derivative^[n - k]) (x + y)) = 0
simp [hx, hy]
case refine_4
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝¹ : k✝ ≤ n + 1
k : ℕ
h✝ : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)
a : ℚ
x : ℚ[X]
h : eval 1 ((↑derivative^[n - k]) x) = 0
⊢ eval 1 ((↑derivative^[n - k]) (a • x)) = 0
case refine_4
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝ : k✝ ≤ n + 1
k : ℕ
h : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)
⊢ ∀ (a : ℚ) (x : ℚ[X]), eval 1 ((↑derivative^[n - k]) x) = 0 → eval 1 ((↑derivative^[n - k]) (a • x)) = 0
intro a x h
no goals
case refine_4
R : Type ?u.195275
inst✝ : CommRing R
n k✝ : ℕ
h✝¹ : k✝ ≤ n + 1
k : ℕ
h✝ : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 => bernsteinPolynomial ℚ n ↑k_1)
a : ℚ
x : ℚ[X]
h : eval 1 ((↑derivative^[n - k]) x) = 0
⊢ eval 1 ((↑derivative^[n - k]) (a • x)) = 0
simp [h]