[GOAL]
R : Type u_1
inst✝ : CommRing R
⊢ bernsteinPolynomial ℤ 3 2 = 3 * X ^ 2 - 3 * X ^ 3
[PROOFSTEP]
simp [bernsteinPolynomial, choose]
[GOAL]
R : Type u_1
inst✝ : CommRing R
⊢ (1 + 1 + 1) * X ^ 2 * (1 - X) = 3 * X ^ 2 - 3 * X ^ 3
[PROOFSTEP]
norm_num
[GOAL]
R : Type u_1
inst✝ : CommRing R
⊢ 3 * X ^ 2 * (1 - X) = 3 * X ^ 2 - 3 * X ^ 3
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : n < ν
⊢ bernsteinPolynomial R n ν = 0
[PROOFSTEP]
simp [bernsteinPolynomial, Nat.choose_eq_zero_of_lt h]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
n ν : ℕ
⊢ Polynomial.map f (bernsteinPolynomial R n ν) = bernsteinPolynomial S n ν
[PROOFSTEP]
simp [bernsteinPolynomial]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
⊢ Polynomial.comp (bernsteinPolynomial R n ν) (1 - X) = bernsteinPolynomial R n (n - ν)
[PROOFSTEP]
simp [bernsteinPolynomial, h, tsub_tsub_assoc, mul_right_comm]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
⊢ bernsteinPolynomial R n ν = Polynomial.comp (bernsteinPolynomial R n (n - ν)) (1 - X)
[PROOFSTEP]
simp [← flip _ _ _ h, Polynomial.comp_assoc]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ Polynomial.eval 0 (bernsteinPolynomial R n ν) = if ν = 0 then 1 else 0
[PROOFSTEP]
rw [bernsteinPolynomial]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ Polynomial.eval 0 (↑(choose n ν) * X ^ ν * (1 - X) ^ (n - ν)) = if ν = 0 then 1 else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν = 0
⊢ Polynomial.eval 0 (↑(choose n ν) * X ^ ν * (1 - X) ^ (n - ν)) = 1
[PROOFSTEP]
subst h
[GOAL]
case pos
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ Polynomial.eval 0 (↑(choose n 0) * X ^ 0 * (1 - X) ^ (n - 0)) = 1
[PROOFSTEP]
simp
[GOAL]
case neg
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ¬ν = 0
⊢ Polynomial.eval 0 (↑(choose n ν) * X ^ ν * (1 - X) ^ (n - ν)) = 0
[PROOFSTEP]
simp [zero_pow (Nat.pos_of_ne_zero h)]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ Polynomial.eval 1 (bernsteinPolynomial R n ν) = if ν = n then 1 else 0
[PROOFSTEP]
rw [bernsteinPolynomial]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ Polynomial.eval 1 (↑(choose n ν) * X ^ ν * (1 - X) ^ (n - ν)) = if ν = n then 1 else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν = n
⊢ Polynomial.eval 1 (↑(choose n ν) * X ^ ν * (1 - X) ^ (n - ν)) = 1
[PROOFSTEP]
subst h
[GOAL]
case pos
R : Type u_1
inst✝ : CommRing R
ν : ℕ
⊢ Polynomial.eval 1 (↑(choose ν ν) * X ^ ν * (1 - X) ^ (ν - ν)) = 1
[PROOFSTEP]
simp
[GOAL]
case neg
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ¬ν = n
⊢ Polynomial.eval 1 (↑(choose n ν) * X ^ ν * (1 - X) ^ (n - ν)) = 0
[PROOFSTEP]
obtain w | w := (n - ν).eq_zero_or_pos
[GOAL]
case neg.inl
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ¬ν = n
w : n - ν = 0
⊢ Polynomial.eval 1 (↑(choose n ν) * X ^ ν * (1 - X) ^ (n - ν)) = 0
[PROOFSTEP]
simp [Nat.choose_eq_zero_of_lt ((tsub_eq_zero_iff_le.mp w).lt_of_ne (Ne.symm h))]
[GOAL]
case neg.inr
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ¬ν = n
w : n - ν > 0
⊢ Polynomial.eval 1 (↑(choose n ν) * X ^ ν * (1 - X) ^ (n - ν)) = 0
[PROOFSTEP]
simp [zero_pow w]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑Polynomial.derivative (bernsteinPolynomial R (n + 1) (ν + 1)) =
    (↑n + 1) * (bernsteinPolynomial R n ν - bernsteinPolynomial R n (ν + 1))
[PROOFSTEP]
rw [bernsteinPolynomial]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑Polynomial.derivative (↑(choose (n + 1) (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n + 1 - (ν + 1))) =
    (↑n + 1) * (bernsteinPolynomial R n ν - bernsteinPolynomial R n (ν + 1))
[PROOFSTEP]
suffices
  ((n + 1).choose (ν + 1) : R[X]) * ((↑(ν + 1 : ℕ) : R[X]) * X ^ ν) * (1 - X) ^ (n - ν) -
      ((n + 1).choose (ν + 1) : R[X]) * X ^ (ν + 1) * ((↑(n - ν) : R[X]) * (1 - X) ^ (n - ν - 1)) =
    (↑(n + 1) : R[X]) *
      ((n.choose ν : R[X]) * X ^ ν * (1 - X) ^ (n - ν) -
        (n.choose (ν + 1) : R[X]) * X ^ (ν + 1) * (1 - X) ^ (n - (ν + 1)))
  by
  simpa [Polynomial.derivative_pow, ← sub_eq_add_neg, Nat.succ_sub_succ_eq_sub, Polynomial.derivative_mul,
    Polynomial.derivative_nat_cast, zero_mul, Nat.cast_add, algebraMap.coe_one, Polynomial.derivative_X, mul_one,
    zero_add, Polynomial.derivative_sub, Polynomial.derivative_one, zero_sub, mul_neg, Nat.sub_zero,
    bernsteinPolynomial, map_add, map_natCast, Nat.cast_one]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
this :
  ↑(choose (n + 1) (ν + 1)) * (↑(ν + 1) * X ^ ν) * (1 - X) ^ (n - ν) -
      ↑(choose (n + 1) (ν + 1)) * X ^ (ν + 1) * (↑(n - ν) * (1 - X) ^ (n - ν - 1)) =
    ↑(n + 1) * (↑(choose n ν) * X ^ ν * (1 - X) ^ (n - ν) - ↑(choose n (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n - (ν + 1)))
⊢ ↑Polynomial.derivative (↑(choose (n + 1) (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n + 1 - (ν + 1))) =
    (↑n + 1) * (bernsteinPolynomial R n ν - bernsteinPolynomial R n (ν + 1))
[PROOFSTEP]
simpa [Polynomial.derivative_pow, ← sub_eq_add_neg, Nat.succ_sub_succ_eq_sub, Polynomial.derivative_mul,
  Polynomial.derivative_nat_cast, zero_mul, Nat.cast_add, algebraMap.coe_one, Polynomial.derivative_X, mul_one,
  zero_add, Polynomial.derivative_sub, Polynomial.derivative_one, zero_sub, mul_neg, Nat.sub_zero, bernsteinPolynomial,
  map_add, map_natCast, Nat.cast_one]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑(choose (n + 1) (ν + 1)) * (↑(ν + 1) * X ^ ν) * (1 - X) ^ (n - ν) -
      ↑(choose (n + 1) (ν + 1)) * X ^ (ν + 1) * (↑(n - ν) * (1 - X) ^ (n - ν - 1)) =
    ↑(n + 1) * (↑(choose n ν) * X ^ ν * (1 - X) ^ (n - ν) - ↑(choose n (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n - (ν + 1)))
[PROOFSTEP]
conv_rhs =>
  rw [mul_sub]
    -- We'll prove the two terms match up separately.
[GOAL]
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
| ↑(n + 1) * (↑(choose n ν) * X ^ ν * (1 - X) ^ (n - ν) - ↑(choose n (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n - (ν + 1)))
[PROOFSTEP]
rw [mul_sub]
    -- We'll prove the two terms match up separately.
[GOAL]
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
| ↑(n + 1) * (↑(choose n ν) * X ^ ν * (1 - X) ^ (n - ν) - ↑(choose n (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n - (ν + 1)))
[PROOFSTEP]
rw [mul_sub]
    -- We'll prove the two terms match up separately.
[GOAL]
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
| ↑(n + 1) * (↑(choose n ν) * X ^ ν * (1 - X) ^ (n - ν) - ↑(choose n (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n - (ν + 1)))
[PROOFSTEP]
rw [mul_sub]
  -- We'll prove the two terms match up separately.
[GOAL]
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑(choose (n + 1) (ν + 1)) * (↑(ν + 1) * X ^ ν) * (1 - X) ^ (n - ν) -
      ↑(choose (n + 1) (ν + 1)) * X ^ (ν + 1) * (↑(n - ν) * (1 - X) ^ (n - ν - 1)) =
    ↑(n + 1) * (↑(choose n ν) * X ^ ν * (1 - X) ^ (n - ν)) -
      ↑(n + 1) * (↑(choose n (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n - (ν + 1)))
[PROOFSTEP]
refine' congr (congr_arg Sub.sub _) _
[GOAL]
case refine'_1
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑(choose (n + 1) (ν + 1)) * (↑(ν + 1) * X ^ ν) * (1 - X) ^ (n - ν) =
    ↑(n + 1) * (↑(choose n ν) * X ^ ν * (1 - X) ^ (n - ν))
[PROOFSTEP]
simp only [← mul_assoc]
[GOAL]
case refine'_1
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑(choose (n + 1) (ν + 1)) * ↑(ν + 1) * X ^ ν * (1 - X) ^ (n - ν) =
    ↑(n + 1) * ↑(choose n ν) * X ^ ν * (1 - X) ^ (n - ν)
[PROOFSTEP]
refine' congr (congr_arg (· * ·) (congr (congr_arg (· * ·) _) rfl)) rfl
[GOAL]
case refine'_1
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑(choose (n + 1) (ν + 1)) * ↑(ν + 1) = ↑(n + 1) * ↑(choose n ν)
[PROOFSTEP]
exact_mod_cast congr_arg (fun m : ℕ => (m : R[X])) (Nat.succ_mul_choose_eq n ν).symm
[GOAL]
case refine'_2
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑(choose (n + 1) (ν + 1)) * X ^ (ν + 1) * (↑(n - ν) * (1 - X) ^ (n - ν - 1)) =
    ↑(n + 1) * (↑(choose n (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n - (ν + 1)))
[PROOFSTEP]
rw [← tsub_add_eq_tsub_tsub, ← mul_assoc, ← mul_assoc]
[GOAL]
case refine'_2
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑(choose (n + 1) (ν + 1)) * X ^ (ν + 1) * ↑(n - ν) * (1 - X) ^ (n - (ν + 1)) =
    ↑(n + 1) * (↑(choose n (ν + 1)) * X ^ (ν + 1)) * (1 - X) ^ (n - (ν + 1))
[PROOFSTEP]
congr 1
[GOAL]
case refine'_2.e_a
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑(choose (n + 1) (ν + 1)) * X ^ (ν + 1) * ↑(n - ν) = ↑(n + 1) * (↑(choose n (ν + 1)) * X ^ (ν + 1))
[PROOFSTEP]
rw [mul_comm, ← mul_assoc, ← mul_assoc]
[GOAL]
case refine'_2.e_a
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑(n - ν) * ↑(choose (n + 1) (ν + 1)) * X ^ (ν + 1) = ↑(n + 1) * ↑(choose n (ν + 1)) * X ^ (ν + 1)
[PROOFSTEP]
congr 1
[GOAL]
case refine'_2.e_a.e_a
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑(n - ν) * ↑(choose (n + 1) (ν + 1)) = ↑(n + 1) * ↑(choose n (ν + 1))
[PROOFSTEP]
norm_cast
[GOAL]
case refine'_2.e_a.e_a
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑((n - ν) * choose (n + 1) (ν + 1)) = ↑((n + 1) * choose n (ν + 1))
[PROOFSTEP]
congr 1
[GOAL]
case refine'_2.e_a.e_a.e_a
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ (n - ν) * choose (n + 1) (ν + 1) = (n + 1) * choose n (ν + 1)
[PROOFSTEP]
convert (Nat.choose_mul_succ_eq n (ν + 1)).symm using 1
[GOAL]
case h.e'_2
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ (n - ν) * choose (n + 1) (ν + 1) = choose (n + 1) (ν + 1) * (n + 1 - (ν + 1))
[PROOFSTEP]
rw [mul_comm, Nat.succ_sub_succ_eq_sub]
[GOAL]
case h.e'_3
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ (n + 1) * choose n (ν + 1) = choose n (ν + 1) * (n + 1)
[PROOFSTEP]
apply mul_comm
[GOAL]
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑Polynomial.derivative (bernsteinPolynomial R n (ν + 1)) =
    ↑n * (bernsteinPolynomial R (n - 1) ν - bernsteinPolynomial R (n - 1) (ν + 1))
[PROOFSTEP]
cases n
[GOAL]
case zero
R : Type u_1
inst✝ : CommRing R
ν : ℕ
⊢ ↑Polynomial.derivative (bernsteinPolynomial R Nat.zero (ν + 1)) =
    ↑Nat.zero * (bernsteinPolynomial R (Nat.zero - 1) ν - bernsteinPolynomial R (Nat.zero - 1) (ν + 1))
[PROOFSTEP]
simp [bernsteinPolynomial]
[GOAL]
case succ
R : Type u_1
inst✝ : CommRing R
ν n✝ : ℕ
⊢ ↑Polynomial.derivative (bernsteinPolynomial R (Nat.succ n✝) (ν + 1)) =
    ↑(Nat.succ n✝) * (bernsteinPolynomial R (Nat.succ n✝ - 1) ν - bernsteinPolynomial R (Nat.succ n✝ - 1) (ν + 1))
[PROOFSTEP]
rw [Nat.cast_succ]
[GOAL]
case succ
R : Type u_1
inst✝ : CommRing R
ν n✝ : ℕ
⊢ ↑Polynomial.derivative (bernsteinPolynomial R (Nat.succ n✝) (ν + 1)) =
    (↑n✝ + 1) * (bernsteinPolynomial R (Nat.succ n✝ - 1) ν - bernsteinPolynomial R (Nat.succ n✝ - 1) (ν + 1))
[PROOFSTEP]
apply derivative_succ_aux
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ ↑Polynomial.derivative (bernsteinPolynomial R n 0) = -↑n * bernsteinPolynomial R (n - 1) 0
[PROOFSTEP]
simp [bernsteinPolynomial, Polynomial.derivative_pow]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n ν k : ℕ
⊢ k < ν → Polynomial.eval 0 ((↑Polynomial.derivative)^[k] (bernsteinPolynomial R n ν)) = 0
[PROOFSTEP]
cases' ν with ν
[GOAL]
case zero
R : Type u_1
inst✝ : CommRing R
n k : ℕ
⊢ k < Nat.zero → Polynomial.eval 0 ((↑Polynomial.derivative)^[k] (bernsteinPolynomial R n Nat.zero)) = 0
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case succ
R : Type u_1
inst✝ : CommRing R
n k ν : ℕ
⊢ k < Nat.succ ν → Polynomial.eval 0 ((↑Polynomial.derivative)^[k] (bernsteinPolynomial R n (Nat.succ ν))) = 0
[PROOFSTEP]
rw [Nat.lt_succ_iff]
[GOAL]
case succ
R : Type u_1
inst✝ : CommRing R
n k ν : ℕ
⊢ k ≤ ν → Polynomial.eval 0 ((↑Polynomial.derivative)^[k] (bernsteinPolynomial R n (Nat.succ ν))) = 0
[PROOFSTEP]
induction' k with k ih generalizing n ν
[GOAL]
case succ.zero
R : Type u_1
inst✝ : CommRing R
n✝ ν✝ n ν : ℕ
⊢ Nat.zero ≤ ν → Polynomial.eval 0 ((↑Polynomial.derivative)^[Nat.zero] (bernsteinPolynomial R n (Nat.succ ν))) = 0
[PROOFSTEP]
simp [eval_at_0]
[GOAL]
case succ.succ
R : Type u_1
inst✝ : CommRing R
n✝ ν✝ k : ℕ
ih : ∀ (n ν : ℕ), k ≤ ν → Polynomial.eval 0 ((↑Polynomial.derivative)^[k] (bernsteinPolynomial R n (Nat.succ ν))) = 0
n ν : ℕ
⊢ Nat.succ k ≤ ν → Polynomial.eval 0 ((↑Polynomial.derivative)^[Nat.succ k] (bernsteinPolynomial R n (Nat.succ ν))) = 0
[PROOFSTEP]
simp only [derivative_succ, Int.coe_nat_eq_zero, mul_eq_zero, Function.comp_apply, Function.iterate_succ,
  Polynomial.iterate_derivative_sub, Polynomial.iterate_derivative_nat_cast_mul, Polynomial.eval_mul,
  Polynomial.eval_nat_cast, Polynomial.eval_sub]
[GOAL]
case succ.succ
R : Type u_1
inst✝ : CommRing R
n✝ ν✝ k : ℕ
ih : ∀ (n ν : ℕ), k ≤ ν → Polynomial.eval 0 ((↑Polynomial.derivative)^[k] (bernsteinPolynomial R n (Nat.succ ν))) = 0
n ν : ℕ
⊢ Nat.succ k ≤ ν →
    ↑n *
        (Polynomial.eval 0 ((↑Polynomial.derivative)^[k] (bernsteinPolynomial R (n - 1) ν)) -
          Polynomial.eval 0 ((↑Polynomial.derivative)^[k] (bernsteinPolynomial R (n - 1) (ν + 1)))) =
      0
[PROOFSTEP]
intro h
[GOAL]
case succ.succ
R : Type u_1
inst✝ : CommRing R
n✝ ν✝ k : ℕ
ih : ∀ (n ν : ℕ), k ≤ ν → Polynomial.eval 0 ((↑Polynomial.derivative)^[k] (bernsteinPolynomial R n (Nat.succ ν))) = 0
n ν : ℕ
h : Nat.succ k ≤ ν
⊢ ↑n *
      (Polynomial.eval 0 ((↑Polynomial.derivative)^[k] (bernsteinPolynomial R (n - 1) ν)) -
        Polynomial.eval 0 ((↑Polynomial.derivative)^[k] (bernsteinPolynomial R (n - 1) (ν + 1)))) =
    0
[PROOFSTEP]
apply mul_eq_zero_of_right
[GOAL]
case succ.succ.h
R : Type u_1
inst✝ : CommRing R
n✝ ν✝ k : ℕ
ih : ∀ (n ν : ℕ), k ≤ ν → Polynomial.eval 0 ((↑Polynomial.derivative)^[k] (bernsteinPolynomial R n (Nat.succ ν))) = 0
n ν : ℕ
h : Nat.succ k ≤ ν
⊢ Polynomial.eval 0 ((↑Polynomial.derivative)^[k] (bernsteinPolynomial R (n - 1) ν)) -
      Polynomial.eval 0 ((↑Polynomial.derivative)^[k] (bernsteinPolynomial R (n - 1) (ν + 1))) =
    0
[PROOFSTEP]
rw [ih _ _ (Nat.le_of_succ_le h), sub_zero]
[GOAL]
case succ.succ.h
R : Type u_1
inst✝ : CommRing R
n✝ ν✝ k : ℕ
ih : ∀ (n ν : ℕ), k ≤ ν → Polynomial.eval 0 ((↑Polynomial.derivative)^[k] (bernsteinPolynomial R n (Nat.succ ν))) = 0
n ν : ℕ
h : Nat.succ k ≤ ν
⊢ Polynomial.eval 0 ((↑Polynomial.derivative)^[k] (bernsteinPolynomial R (n - 1) ν)) = 0
[PROOFSTEP]
convert ih _ _ (Nat.pred_le_pred h)
[GOAL]
case h.e'_2.h.e'_4.h.h.e'_4.h.e'_4
R : Type u_1
inst✝ : CommRing R
n✝ ν✝ k : ℕ
ih : ∀ (n ν : ℕ), k ≤ ν → Polynomial.eval 0 ((↑Polynomial.derivative)^[k] (bernsteinPolynomial R n (Nat.succ ν))) = 0
n ν : ℕ
h : Nat.succ k ≤ ν
e_2✝ : Ring.toSemiring = CommSemiring.toSemiring
⊢ ν = Nat.succ (Nat.pred ν)
[PROOFSTEP]
exact (Nat.succ_pred_eq_of_pos (k.succ_pos.trans_le h)).symm
[GOAL]
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ eval 0 ((↑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (pochhammer R ν)
[PROOFSTEP]
by_cases h : ν ≤ n
[GOAL]
case pos
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
⊢ eval 0 ((↑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (pochhammer R ν)
[PROOFSTEP]
induction' ν with ν ih generalizing n
[GOAL]
case pos.zero
R : Type u_1
inst✝ : CommRing R
n✝ ν : ℕ
h✝ : ν ≤ n✝
n : ℕ
h : Nat.zero ≤ n
⊢ eval 0 ((↑derivative)^[Nat.zero] (bernsteinPolynomial R n Nat.zero)) =
    eval (↑(n - (Nat.zero - 1))) (pochhammer R Nat.zero)
[PROOFSTEP]
simp [eval_at_0]
[GOAL]
case pos.succ
R : Type u_1
inst✝ : CommRing R
n✝ ν✝ : ℕ
h✝ : ν✝ ≤ n✝
ν : ℕ
ih : ∀ (n : ℕ), ν ≤ n → eval 0 ((↑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (pochhammer R ν)
n : ℕ
h : Nat.succ ν ≤ n
⊢ eval 0 ((↑derivative)^[Nat.succ ν] (bernsteinPolynomial R n (Nat.succ ν))) =
    eval (↑(n - (Nat.succ ν - 1))) (pochhammer R (Nat.succ ν))
[PROOFSTEP]
have h' : ν ≤ n - 1 := le_tsub_of_add_le_right h
[GOAL]
case pos.succ
R : Type u_1
inst✝ : CommRing R
n✝ ν✝ : ℕ
h✝ : ν✝ ≤ n✝
ν : ℕ
ih : ∀ (n : ℕ), ν ≤ n → eval 0 ((↑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (pochhammer R ν)
n : ℕ
h : Nat.succ ν ≤ n
h' : ν ≤ n - 1
⊢ eval 0 ((↑derivative)^[Nat.succ ν] (bernsteinPolynomial R n (Nat.succ ν))) =
    eval (↑(n - (Nat.succ ν - 1))) (pochhammer R (Nat.succ ν))
[PROOFSTEP]
simp only [derivative_succ, ih (n - 1) h', iterate_derivative_succ_at_0_eq_zero, Nat.succ_sub_succ_eq_sub, tsub_zero,
  sub_zero, iterate_derivative_sub, iterate_derivative_nat_cast_mul, eval_one, eval_mul, eval_add, eval_sub, eval_X,
  eval_comp, eval_nat_cast, Function.comp_apply, Function.iterate_succ, pochhammer_succ_left]
[GOAL]
case pos.succ
R : Type u_1
inst✝ : CommRing R
n✝ ν✝ : ℕ
h✝ : ν✝ ≤ n✝
ν : ℕ
ih : ∀ (n : ℕ), ν ≤ n → eval 0 ((↑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (pochhammer R ν)
n : ℕ
h : Nat.succ ν ≤ n
h' : ν ≤ n - 1
⊢ ↑n * eval (↑(n - 1 - (ν - 1))) (pochhammer R ν) = ↑(n - ν) * eval (↑(n - ν) + 1) (pochhammer R ν)
[PROOFSTEP]
obtain rfl | h'' := ν.eq_zero_or_pos
[GOAL]
case pos.succ.inl
R : Type u_1
inst✝ : CommRing R
n✝ ν : ℕ
h✝ : ν ≤ n✝
n : ℕ
ih : ∀ (n : ℕ), 0 ≤ n → eval 0 ((↑derivative)^[0] (bernsteinPolynomial R n 0)) = eval (↑(n - (0 - 1))) (pochhammer R 0)
h : Nat.succ 0 ≤ n
h' : 0 ≤ n - 1
⊢ ↑n * eval (↑(n - 1 - (0 - 1))) (pochhammer R 0) = ↑(n - 0) * eval (↑(n - 0) + 1) (pochhammer R 0)
[PROOFSTEP]
simp
[GOAL]
case pos.succ.inr
R : Type u_1
inst✝ : CommRing R
n✝ ν✝ : ℕ
h✝ : ν✝ ≤ n✝
ν : ℕ
ih : ∀ (n : ℕ), ν ≤ n → eval 0 ((↑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (pochhammer R ν)
n : ℕ
h : Nat.succ ν ≤ n
h' : ν ≤ n - 1
h'' : ν > 0
⊢ ↑n * eval (↑(n - 1 - (ν - 1))) (pochhammer R ν) = ↑(n - ν) * eval (↑(n - ν) + 1) (pochhammer R ν)
[PROOFSTEP]
have : n - 1 - (ν - 1) = n - ν := by
  rw [gt_iff_lt, ← Nat.succ_le_iff] at h''
  rw [← tsub_add_eq_tsub_tsub, add_comm, tsub_add_cancel_of_le h'']
[GOAL]
R : Type u_1
inst✝ : CommRing R
n✝ ν✝ : ℕ
h✝ : ν✝ ≤ n✝
ν : ℕ
ih : ∀ (n : ℕ), ν ≤ n → eval 0 ((↑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (pochhammer R ν)
n : ℕ
h : Nat.succ ν ≤ n
h' : ν ≤ n - 1
h'' : ν > 0
⊢ n - 1 - (ν - 1) = n - ν
[PROOFSTEP]
rw [gt_iff_lt, ← Nat.succ_le_iff] at h''
[GOAL]
R : Type u_1
inst✝ : CommRing R
n✝ ν✝ : ℕ
h✝ : ν✝ ≤ n✝
ν : ℕ
ih : ∀ (n : ℕ), ν ≤ n → eval 0 ((↑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (pochhammer R ν)
n : ℕ
h : Nat.succ ν ≤ n
h' : ν ≤ n - 1
h'' : Nat.succ 0 ≤ ν
⊢ n - 1 - (ν - 1) = n - ν
[PROOFSTEP]
rw [← tsub_add_eq_tsub_tsub, add_comm, tsub_add_cancel_of_le h'']
[GOAL]
case pos.succ.inr
R : Type u_1
inst✝ : CommRing R
n✝ ν✝ : ℕ
h✝ : ν✝ ≤ n✝
ν : ℕ
ih : ∀ (n : ℕ), ν ≤ n → eval 0 ((↑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (pochhammer R ν)
n : ℕ
h : Nat.succ ν ≤ n
h' : ν ≤ n - 1
h'' : ν > 0
this : n - 1 - (ν - 1) = n - ν
⊢ ↑n * eval (↑(n - 1 - (ν - 1))) (pochhammer R ν) = ↑(n - ν) * eval (↑(n - ν) + 1) (pochhammer R ν)
[PROOFSTEP]
rw [this, pochhammer_eval_succ]
[GOAL]
case pos.succ.inr
R : Type u_1
inst✝ : CommRing R
n✝ ν✝ : ℕ
h✝ : ν✝ ≤ n✝
ν : ℕ
ih : ∀ (n : ℕ), ν ≤ n → eval 0 ((↑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (pochhammer R ν)
n : ℕ
h : Nat.succ ν ≤ n
h' : ν ≤ n - 1
h'' : ν > 0
this : n - 1 - (ν - 1) = n - ν
⊢ ↑n * eval (↑(n - ν)) (pochhammer R ν) = (↑(n - ν) + ↑ν) * eval (↑(n - ν)) (pochhammer R ν)
[PROOFSTEP]
rw_mod_cast [tsub_add_cancel_of_le (h'.trans n.pred_le)]
[GOAL]
case neg
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ¬ν ≤ n
⊢ eval 0 ((↑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (pochhammer R ν)
[PROOFSTEP]
simp only [not_le] at h
[GOAL]
case neg
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : n < ν
⊢ eval 0 ((↑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (pochhammer R ν)
[PROOFSTEP]
rw [tsub_eq_zero_iff_le.mpr (Nat.le_pred_of_lt h), eq_zero_of_lt R h]
[GOAL]
case neg
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : n < ν
⊢ eval 0 ((↑derivative)^[ν] 0) = eval (↑0) (pochhammer R ν)
[PROOFSTEP]
simp [pos_iff_ne_zero.mp (pos_of_gt h)]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ eval 0 ((↑derivative)^[ν] (bernsteinPolynomial R n ν)) ≠ 0
[PROOFSTEP]
simp only [Int.coe_nat_eq_zero, bernsteinPolynomial.iterate_derivative_at_0, Ne.def, Nat.cast_eq_zero]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ ¬eval (↑(n - (ν - 1))) (pochhammer R ν) = 0
[PROOFSTEP]
simp only [← pochhammer_eval_cast]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ ¬↑(eval (n - (ν - 1)) (pochhammer ℕ ν)) = 0
[PROOFSTEP]
norm_cast
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ ¬eval (n - (ν - 1)) (pochhammer ℕ ν) = 0
[PROOFSTEP]
apply ne_of_gt
[GOAL]
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ 0 < eval (n - (ν - 1)) (pochhammer ℕ ν)
[PROOFSTEP]
obtain rfl | h' := Nat.eq_zero_or_pos ν
[GOAL]
case h.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n : ℕ
h : 0 ≤ n
⊢ 0 < eval (n - (0 - 1)) (pochhammer ℕ 0)
[PROOFSTEP]
simp
[GOAL]
case h.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
h' : ν > 0
⊢ 0 < eval (n - (ν - 1)) (pochhammer ℕ ν)
[PROOFSTEP]
rw [← Nat.succ_pred_eq_of_pos h'] at h
[GOAL]
case h.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : Nat.succ (Nat.pred ν) ≤ n
h' : ν > 0
⊢ 0 < eval (n - (ν - 1)) (pochhammer ℕ ν)
[PROOFSTEP]
exact pochhammer_pos _ _ (tsub_pos_of_lt (Nat.lt_of_succ_le h))
[GOAL]
R : Type u_1
inst✝ : CommRing R
n ν k : ℕ
⊢ k < n - ν → eval 1 ((↑derivative)^[k] (bernsteinPolynomial R n ν)) = 0
[PROOFSTEP]
intro w
[GOAL]
R : Type u_1
inst✝ : CommRing R
n ν k : ℕ
w : k < n - ν
⊢ eval 1 ((↑derivative)^[k] (bernsteinPolynomial R n ν)) = 0
[PROOFSTEP]
rw [flip' _ _ _ (tsub_pos_iff_lt.mp (pos_of_gt w)).le]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n ν k : ℕ
w : k < n - ν
⊢ eval 1 ((↑derivative)^[k] (comp (bernsteinPolynomial R n (n - ν)) (1 - X))) = 0
[PROOFSTEP]
simp [Polynomial.eval_comp, iterate_derivative_at_0_eq_zero_of_lt R n w]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
⊢ eval 1 ((↑derivative)^[n - ν] (bernsteinPolynomial R n ν)) = (-1) ^ (n - ν) * eval (↑ν + 1) (pochhammer R (n - ν))
[PROOFSTEP]
rw [flip' _ _ _ h]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
⊢ eval 1 ((↑derivative)^[n - ν] (comp (bernsteinPolynomial R n (n - ν)) (1 - X))) =
    (-1) ^ (n - ν) * eval (↑ν + 1) (pochhammer R (n - ν))
[PROOFSTEP]
simp [Polynomial.eval_comp, h]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
⊢ (-1) ^ (n - ν) * eval (↑(n - (n - ν - 1))) (pochhammer R (n - ν)) =
    (-1) ^ (n - ν) * eval (↑ν + 1) (pochhammer R (n - ν))
[PROOFSTEP]
obtain rfl | h' := h.eq_or_lt
[GOAL]
case inl
R : Type u_1
inst✝ : CommRing R
ν : ℕ
h : ν ≤ ν
⊢ (-1) ^ (ν - ν) * eval (↑(ν - (ν - ν - 1))) (pochhammer R (ν - ν)) =
    (-1) ^ (ν - ν) * eval (↑ν + 1) (pochhammer R (ν - ν))
[PROOFSTEP]
simp
[GOAL]
case inr
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
h' : ν < n
⊢ (-1) ^ (n - ν) * eval (↑(n - (n - ν - 1))) (pochhammer R (n - ν)) =
    (-1) ^ (n - ν) * eval (↑ν + 1) (pochhammer R (n - ν))
[PROOFSTEP]
congr
[GOAL]
case inr.e_a.e_a
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
h' : ν < n
⊢ ↑(n - (n - ν - 1)) = ↑ν + 1
[PROOFSTEP]
norm_cast
[GOAL]
case inr.e_a.e_a
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
h' : ν < n
⊢ ↑(n - (n - ν - 1)) = ↑(ν + 1)
[PROOFSTEP]
rw [← tsub_add_eq_tsub_tsub, tsub_tsub_cancel_of_le (Nat.succ_le_iff.mpr h')]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ eval 1 ((↑derivative)^[n - ν] (bernsteinPolynomial R n ν)) ≠ 0
[PROOFSTEP]
rw [bernsteinPolynomial.iterate_derivative_at_1 _ _ _ h, Ne.def, neg_one_pow_mul_eq_zero_iff, ← Nat.cast_succ, ←
  pochhammer_eval_cast, ← Nat.cast_zero, Nat.cast_inj]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ ¬eval (Nat.succ ν) (pochhammer ℕ (n - ν)) = 0
[PROOFSTEP]
exact (pochhammer_pos _ _ (Nat.succ_pos ν)).ne'
[GOAL]
R : Type u_1
inst✝ : CommRing R
n k : ℕ
h : k ≤ n + 1
⊢ LinearIndependent ℚ fun ν => bernsteinPolynomial ℚ n ↑ν
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u_1
inst✝ : CommRing R
n k : ℕ
h✝ : k ≤ n + 1
h : Nat.zero ≤ n + 1
⊢ LinearIndependent ℚ fun ν => bernsteinPolynomial ℚ n ↑ν
[PROOFSTEP]
simp [Nat.zero_eq]
[GOAL]
case zero
R : Type u_1
inst✝ : CommRing R
n k : ℕ
h✝ : k ≤ n + 1
h : Nat.zero ≤ n + 1
⊢ LinearIndependent ℚ fun ν => bernsteinPolynomial ℚ n ↑ν
[PROOFSTEP]
apply linearIndependent_empty_type
[GOAL]
case succ
R : Type u_1
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 ↑ν
[PROOFSTEP]
apply linearIndependent_fin_succ'.mpr
[GOAL]
case succ
R : Type u_1
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 ↑ν))
[PROOFSTEP]
fconstructor
[GOAL]
case succ.left
R : Type u_1
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 ↑ν)
[PROOFSTEP]
exact ih (le_of_lt h)
[GOAL]
case succ.right
R : Type u_1
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 ↑ν))
[PROOFSTEP]
clear ih
[GOAL]
case succ.right
R : Type u_1
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 ↑ν))
[PROOFSTEP]
simp only [Nat.succ_eq_add_one, add_le_add_iff_right] at h
[GOAL]
case succ.right
R : Type u_1
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 ↑ν))
[PROOFSTEP]
simp only [Fin.val_last, Fin.init_def]
[GOAL]
case succ.right
R : Type u_1
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))
[PROOFSTEP]
dsimp
[GOAL]
case succ.right
R : Type u_1
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)
[PROOFSTEP]
apply not_mem_span_of_apply_not_mem_span_image (@Polynomial.derivative ℚ _ ^ (n - k))
[GOAL]
case succ.right
R : Type u_1
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)
[PROOFSTEP]
simp only [not_exists, not_and, Submodule.mem_map, Submodule.span_image]
[GOAL]
case succ.right
R : Type u_1
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)
[PROOFSTEP]
intro p m
[GOAL]
case succ.right
R : Type u_1
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)
[PROOFSTEP]
apply_fun Polynomial.eval (1 : ℚ)
[GOAL]
R : Type u_1
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))
[PROOFSTEP]
simp only [LinearMap.pow_apply]
  -- The right hand side is nonzero,
        -- so it will suffice to show the left hand side is always zero.
[GOAL]
R : Type u_1
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))
[PROOFSTEP]
suffices (Polynomial.derivative^[n - k] p).eval 1 = 0 by
  rw [this]
  exact (iterate_derivative_at_1_ne_zero ℚ n k h).symm
[GOAL]
R : Type u_1
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))
[PROOFSTEP]
rw [this]
[GOAL]
R : Type u_1
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))
[PROOFSTEP]
exact (iterate_derivative_at_1_ne_zero ℚ n k h).symm
[GOAL]
R : Type u_1
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
[PROOFSTEP]
refine span_induction m ?_ ?_ ?_ ?_
[GOAL]
case refine_1
R : Type u_1
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
[PROOFSTEP]
simp
[GOAL]
case refine_1
R : Type u_1
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
[PROOFSTEP]
rintro ⟨a, w⟩
[GOAL]
case refine_1.mk
R : Type u_1
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
[PROOFSTEP]
simp only [Fin.val_mk]
[GOAL]
case refine_1.mk
R : Type u_1
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
[PROOFSTEP]
rw [iterate_derivative_at_1_eq_zero_of_lt ℚ n ((tsub_lt_tsub_iff_left_of_le h).mpr w)]
[GOAL]
case refine_2
R : Type u_1
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
[PROOFSTEP]
simp
[GOAL]
case refine_3
R : Type u_1
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
[PROOFSTEP]
intro x y hx hy
[GOAL]
case refine_3
R : Type u_1
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
[PROOFSTEP]
simp [hx, hy]
[GOAL]
case refine_4
R : Type u_1
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
[PROOFSTEP]
intro a x h
[GOAL]
case refine_4
R : Type u_1
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
[PROOFSTEP]
simp [h]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν = (X + (1 - X)) ^ n
[PROOFSTEP]
rw [add_pow]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν =
    ∑ m in Finset.range (n + 1), X ^ m * (1 - X) ^ (n - m) * ↑(choose n m)
[PROOFSTEP]
simp only [bernsteinPolynomial, mul_comm, mul_assoc, mul_left_comm]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ (X + (1 - X)) ^ n = 1
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν = n • X
[PROOFSTEP]
let x : MvPolynomial Bool R := MvPolynomial.X true
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
⊢ ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν = n • X
[PROOFSTEP]
let y : MvPolynomial Bool R := MvPolynomial.X false
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
⊢ ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν = n • X
[PROOFSTEP]
have pderiv_true_x : pderiv true x = 1 := by rw [pderiv_X]; rfl
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
⊢ ↑(pderiv true) x = 1
[PROOFSTEP]
rw [pderiv_X]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
⊢ Pi.single true 1 true = 1
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : ↑(pderiv true) x = 1
⊢ ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν = n • X
[PROOFSTEP]
have pderiv_true_y : pderiv true y = 0 := by rw [pderiv_X]; rfl
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : ↑(pderiv true) x = 1
⊢ ↑(pderiv true) y = 0
[PROOFSTEP]
rw [pderiv_X]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : ↑(pderiv true) x = 1
⊢ Pi.single true 1 false = 0
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : ↑(pderiv true) x = 1
pderiv_true_y : ↑(pderiv true) y = 0
⊢ ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν = n • X
[PROOFSTEP]
let e : Bool → R[X] := fun i =>
  cond i X
    (1 - X)
      -- Start with `(x+y)^n = (x+y)^n`,
        -- take the `x`-derivative, evaluate at `x=X, y=1-X`, and multiply by `X`:
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : ↑(pderiv true) x = 1
pderiv_true_y : ↑(pderiv true) y = 0
e : Bool → R[X] := fun i => bif i then X else 1 - X
⊢ ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν = n • X
[PROOFSTEP]
trans MvPolynomial.aeval e (pderiv true ((x + y) ^ n)) * X
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : ↑(pderiv true) x = 1
pderiv_true_y : ↑(pderiv true) y = 0
e : Bool → R[X] := fun i => bif i then X else 1 - X
⊢ ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν =
    ↑(MvPolynomial.aeval e) (↑(pderiv true) ((x + y) ^ n)) * X
[PROOFSTEP]
have w :
  ∀ k : ℕ,
    k • bernsteinPolynomial R n k =
      (k : R[X]) * Polynomial.X ^ (k - 1) * (1 - Polynomial.X) ^ (n - k) * (n.choose k : R[X]) * Polynomial.X :=
  by
  rintro (_ | k)
  · simp
  · rw [bernsteinPolynomial]
    simp only [← nat_cast_mul, Nat.succ_eq_add_one, Nat.add_succ_sub_one, add_zero, pow_succ]
    push_cast
    ring
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : ↑(pderiv true) x = 1
pderiv_true_y : ↑(pderiv true) y = 0
e : Bool → R[X] := fun i => bif i then X else 1 - X
⊢ ∀ (k : ℕ), k • bernsteinPolynomial R n k = ↑k * X ^ (k - 1) * (1 - X) ^ (n - k) * ↑(choose n k) * X
[PROOFSTEP]
rintro (_ | k)
[GOAL]
case zero
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : ↑(pderiv true) x = 1
pderiv_true_y : ↑(pderiv true) y = 0
e : Bool → R[X] := fun i => bif i then X else 1 - X
⊢ Nat.zero • bernsteinPolynomial R n Nat.zero =
    ↑Nat.zero * X ^ (Nat.zero - 1) * (1 - X) ^ (n - Nat.zero) * ↑(choose n Nat.zero) * X
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : ↑(pderiv true) x = 1
pderiv_true_y : ↑(pderiv true) y = 0
e : Bool → R[X] := fun i => bif i then X else 1 - X
k : ℕ
⊢ Nat.succ k • bernsteinPolynomial R n (Nat.succ k) =
    ↑(Nat.succ k) * X ^ (Nat.succ k - 1) * (1 - X) ^ (n - Nat.succ k) * ↑(choose n (Nat.succ k)) * X
[PROOFSTEP]
rw [bernsteinPolynomial]
[GOAL]
case succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : ↑(pderiv true) x = 1
pderiv_true_y : ↑(pderiv true) y = 0
e : Bool → R[X] := fun i => bif i then X else 1 - X
k : ℕ
⊢ Nat.succ k • (↑(choose n (Nat.succ k)) * X ^ Nat.succ k * (1 - X) ^ (n - Nat.succ k)) =
    ↑(Nat.succ k) * X ^ (Nat.succ k - 1) * (1 - X) ^ (n - Nat.succ k) * ↑(choose n (Nat.succ k)) * X
[PROOFSTEP]
simp only [← nat_cast_mul, Nat.succ_eq_add_one, Nat.add_succ_sub_one, add_zero, pow_succ]
[GOAL]
case succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : ↑(pderiv true) x = 1
pderiv_true_y : ↑(pderiv true) y = 0
e : Bool → R[X] := fun i => bif i then X else 1 - X
k : ℕ
⊢ ↑(k + 1) * (↑(choose n (k + 1)) * (X * X ^ k) * (1 - X) ^ (n - (k + 1))) =
    ↑(k + 1) * X ^ k * (1 - X) ^ (n - (k + 1)) * ↑(choose n (k + 1)) * X
[PROOFSTEP]
push_cast
[GOAL]
case succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : ↑(pderiv true) x = 1
pderiv_true_y : ↑(pderiv true) y = 0
e : Bool → R[X] := fun i => bif i then X else 1 - X
k : ℕ
⊢ (↑k + 1) * (↑(choose n (k + 1)) * (X * X ^ k) * (1 - X) ^ (n - (k + 1))) =
    (↑k + 1) * X ^ k * (1 - X) ^ (n - (k + 1)) * ↑(choose n (k + 1)) * X
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : ↑(pderiv true) x = 1
pderiv_true_y : ↑(pderiv true) y = 0
e : Bool → R[X] := fun i => bif i then X else 1 - X
w : ∀ (k : ℕ), k • bernsteinPolynomial R n k = ↑k * X ^ (k - 1) * (1 - X) ^ (n - k) * ↑(choose n k) * X
⊢ ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν =
    ↑(MvPolynomial.aeval e) (↑(pderiv true) ((x + y) ^ n)) * X
[PROOFSTEP]
rw [add_pow, (pderiv true).map_sum, (MvPolynomial.aeval e).map_sum, Finset.sum_mul]
  -- Step inside the sum:
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : ↑(pderiv true) x = 1
pderiv_true_y : ↑(pderiv true) y = 0
e : Bool → R[X] := fun i => bif i then X else 1 - X
w : ∀ (k : ℕ), k • bernsteinPolynomial R n k = ↑k * X ^ (k - 1) * (1 - X) ^ (n - k) * ↑(choose n k) * X
⊢ ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν =
    ∑ x_1 in Finset.range (n + 1),
      ↑(MvPolynomial.aeval e) (↑(pderiv true) (x ^ x_1 * y ^ (n - x_1) * ↑(choose n x_1))) * X
[PROOFSTEP]
refine' Finset.sum_congr rfl fun k _ => (w k).trans _
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : ↑(pderiv true) x = 1
pderiv_true_y : ↑(pderiv true) y = 0
e : Bool → R[X] := fun i => bif i then X else 1 - X
w : ∀ (k : ℕ), k • bernsteinPolynomial R n k = ↑k * X ^ (k - 1) * (1 - X) ^ (n - k) * ↑(choose n k) * X
k : ℕ
x✝ : k ∈ Finset.range (n + 1)
⊢ ↑k * X ^ (k - 1) * (1 - X) ^ (n - k) * ↑(choose n k) * X =
    ↑(MvPolynomial.aeval e) (↑(pderiv true) (x ^ k * y ^ (n - k) * ↑(choose n k))) * X
[PROOFSTEP]
simp only [pderiv_true_x, pderiv_true_y, Algebra.id.smul_eq_mul, nsmul_eq_mul, Bool.cond_true, Bool.cond_false,
  add_zero, mul_one, mul_zero, smul_zero, MvPolynomial.aeval_X, MvPolynomial.pderiv_mul, Derivation.leibniz_pow,
  Derivation.map_coe_nat, map_natCast, map_pow, map_mul]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : ↑(pderiv true) x = 1
pderiv_true_y : ↑(pderiv true) y = 0
e : Bool → R[X] := fun i => bif i then X else 1 - X
⊢ ↑(MvPolynomial.aeval e) (↑(pderiv true) ((x + y) ^ n)) * X = n • X
[PROOFSTEP]
rw [(pderiv true).leibniz_pow, (pderiv true).map_add, pderiv_true_x, pderiv_true_y]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : ↑(pderiv true) x = 1
pderiv_true_y : ↑(pderiv true) y = 0
e : Bool → R[X] := fun i => bif i then X else 1 - X
⊢ ↑(MvPolynomial.aeval e) (n • (x + y) ^ (n - 1) • (1 + 0)) * X = n • X
[PROOFSTEP]
simp only [Algebra.id.smul_eq_mul, nsmul_eq_mul, map_natCast, map_pow, map_add, map_mul, Bool.cond_true,
  Bool.cond_false, MvPolynomial.aeval_X, add_sub_cancel'_right, one_pow, add_zero, mul_one]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν = (n * (n - 1)) • X ^ 2
[PROOFSTEP]
let x : MvPolynomial Bool R := MvPolynomial.X true
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
⊢ ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν = (n * (n - 1)) • X ^ 2
[PROOFSTEP]
let y : MvPolynomial Bool R := MvPolynomial.X false
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
⊢ ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν = (n * (n - 1)) • X ^ 2
[PROOFSTEP]
have pderiv_true_x : pderiv true x = 1 := by rw [pderiv_X]; rfl
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
⊢ ↑(pderiv true) x = 1
[PROOFSTEP]
rw [pderiv_X]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
⊢ Pi.single true 1 true = 1
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : ↑(pderiv true) x = 1
⊢ ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν = (n * (n - 1)) • X ^ 2
[PROOFSTEP]
have pderiv_true_y : pderiv true y = 0 := by rw [pderiv_X]; rfl
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : ↑(pderiv true) x = 1
⊢ ↑(pderiv true) y = 0
[PROOFSTEP]
rw [pderiv_X]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : ↑(pderiv true) x = 1
⊢ Pi.single true 1 false = 0
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : ↑(pderiv true) x = 1
pderiv_true_y : ↑(pderiv true) y = 0
⊢ ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν = (n * (n - 1)) • X ^ 2
[PROOFSTEP]
let e : Bool → R[X] := fun i =>
  cond i X
    (1 - X)
      -- Start with `(x+y)^n = (x+y)^n`,
        -- take the second `x`-derivative, evaluate at `x=X, y=1-X`, and multiply by `X`:
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : ↑(pderiv true) x = 1
pderiv_true_y : ↑(pderiv true) y = 0
e : Bool → R[X] := fun i => bif i then X else 1 - X
⊢ ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν = (n * (n - 1)) • X ^ 2
[PROOFSTEP]
trans
  MvPolynomial.aeval e (pderiv true (pderiv true ((x + y) ^ n))) *
    X ^
      2
        -- On the left hand side we'll use the binomial theorem, then simplify.
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : ↑(pderiv true) x = 1
pderiv_true_y : ↑(pderiv true) y = 0
e : Bool → R[X] := fun i => bif i then X else 1 - X
⊢ ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν =
    ↑(MvPolynomial.aeval e) (↑(pderiv true) (↑(pderiv true) ((x + y) ^ n))) * X ^ 2
[PROOFSTEP]
have w :
  ∀ k : ℕ,
    (k * (k - 1)) • bernsteinPolynomial R n k =
      (n.choose k : R[X]) *
          ((1 - Polynomial.X) ^ (n - k) * ((k : R[X]) * ((↑(k - 1) : R[X]) * Polynomial.X ^ (k - 1 - 1)))) *
        Polynomial.X ^ 2 :=
  by
  rintro (_ | _ | k)
  · simp
  · simp
  · rw [bernsteinPolynomial]
    simp only [← nat_cast_mul, Nat.succ_eq_add_one, Nat.add_succ_sub_one, add_zero, pow_succ]
    push_cast
    ring
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : ↑(pderiv true) x = 1
pderiv_true_y : ↑(pderiv true) y = 0
e : Bool → R[X] := fun i => bif i then X else 1 - X
⊢ ∀ (k : ℕ),
    (k * (k - 1)) • bernsteinPolynomial R n k =
      ↑(choose n k) * ((1 - X) ^ (n - k) * (↑k * (↑(k - 1) * X ^ (k - 1 - 1)))) * X ^ 2
[PROOFSTEP]
rintro (_ | _ | k)
[GOAL]
case zero
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : ↑(pderiv true) x = 1
pderiv_true_y : ↑(pderiv true) y = 0
e : Bool → R[X] := fun i => bif i then X else 1 - X
⊢ (Nat.zero * (Nat.zero - 1)) • bernsteinPolynomial R n Nat.zero =
    ↑(choose n Nat.zero) * ((1 - X) ^ (n - Nat.zero) * (↑Nat.zero * (↑(Nat.zero - 1) * X ^ (Nat.zero - 1 - 1)))) * X ^ 2
[PROOFSTEP]
simp
[GOAL]
case succ.zero
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : ↑(pderiv true) x = 1
pderiv_true_y : ↑(pderiv true) y = 0
e : Bool → R[X] := fun i => bif i then X else 1 - X
⊢ (Nat.succ Nat.zero * (Nat.succ Nat.zero - 1)) • bernsteinPolynomial R n (Nat.succ Nat.zero) =
    ↑(choose n (Nat.succ Nat.zero)) *
        ((1 - X) ^ (n - Nat.succ Nat.zero) *
          (↑(Nat.succ Nat.zero) * (↑(Nat.succ Nat.zero - 1) * X ^ (Nat.succ Nat.zero - 1 - 1)))) *
      X ^ 2
[PROOFSTEP]
simp
[GOAL]
case succ.succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : ↑(pderiv true) x = 1
pderiv_true_y : ↑(pderiv true) y = 0
e : Bool → R[X] := fun i => bif i then X else 1 - X
k : ℕ
⊢ (Nat.succ (Nat.succ k) * (Nat.succ (Nat.succ k) - 1)) • bernsteinPolynomial R n (Nat.succ (Nat.succ k)) =
    ↑(choose n (Nat.succ (Nat.succ k))) *
        ((1 - X) ^ (n - Nat.succ (Nat.succ k)) *
          (↑(Nat.succ (Nat.succ k)) * (↑(Nat.succ (Nat.succ k) - 1) * X ^ (Nat.succ (Nat.succ k) - 1 - 1)))) *
      X ^ 2
[PROOFSTEP]
rw [bernsteinPolynomial]
[GOAL]
case succ.succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : ↑(pderiv true) x = 1
pderiv_true_y : ↑(pderiv true) y = 0
e : Bool → R[X] := fun i => bif i then X else 1 - X
k : ℕ
⊢ (Nat.succ (Nat.succ k) * (Nat.succ (Nat.succ k) - 1)) •
      (↑(choose n (Nat.succ (Nat.succ k))) * X ^ Nat.succ (Nat.succ k) * (1 - X) ^ (n - Nat.succ (Nat.succ k))) =
    ↑(choose n (Nat.succ (Nat.succ k))) *
        ((1 - X) ^ (n - Nat.succ (Nat.succ k)) *
          (↑(Nat.succ (Nat.succ k)) * (↑(Nat.succ (Nat.succ k) - 1) * X ^ (Nat.succ (Nat.succ k) - 1 - 1)))) *
      X ^ 2
[PROOFSTEP]
simp only [← nat_cast_mul, Nat.succ_eq_add_one, Nat.add_succ_sub_one, add_zero, pow_succ]
[GOAL]
case succ.succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : ↑(pderiv true) x = 1
pderiv_true_y : ↑(pderiv true) y = 0
e : Bool → R[X] := fun i => bif i then X else 1 - X
k : ℕ
⊢ ↑((k + 1 + 1) * (k + 1)) * (↑(choose n (k + 1 + 1)) * (X * (X * X ^ k)) * (1 - X) ^ (n - (k + 1 + 1))) =
    ↑(choose n (k + 1 + 1)) * ((1 - X) ^ (n - (k + 1 + 1)) * (↑(k + 1 + 1) * (↑(k + 1) * X ^ k))) * (X * (X * X ^ 0))
[PROOFSTEP]
push_cast
[GOAL]
case succ.succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : ↑(pderiv true) x = 1
pderiv_true_y : ↑(pderiv true) y = 0
e : Bool → R[X] := fun i => bif i then X else 1 - X
k : ℕ
⊢ (↑k + 1 + 1) * (↑k + 1) * (↑(choose n (k + 1 + 1)) * (X * (X * X ^ k)) * (1 - X) ^ (n - (k + 1 + 1))) =
    ↑(choose n (k + 1 + 1)) * ((1 - X) ^ (n - (k + 1 + 1)) * ((↑k + 1 + 1) * ((↑k + 1) * X ^ k))) * (X * (X * X ^ 0))
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : ↑(pderiv true) x = 1
pderiv_true_y : ↑(pderiv true) y = 0
e : Bool → R[X] := fun i => bif i then X else 1 - X
w :
  ∀ (k : ℕ),
    (k * (k - 1)) • bernsteinPolynomial R n k =
      ↑(choose n k) * ((1 - X) ^ (n - k) * (↑k * (↑(k - 1) * X ^ (k - 1 - 1)))) * X ^ 2
⊢ ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν =
    ↑(MvPolynomial.aeval e) (↑(pderiv true) (↑(pderiv true) ((x + y) ^ n))) * X ^ 2
[PROOFSTEP]
rw [add_pow, (pderiv true).map_sum, (pderiv true).map_sum, (MvPolynomial.aeval e).map_sum, Finset.sum_mul]
  -- Step inside the sum:
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : ↑(pderiv true) x = 1
pderiv_true_y : ↑(pderiv true) y = 0
e : Bool → R[X] := fun i => bif i then X else 1 - X
w :
  ∀ (k : ℕ),
    (k * (k - 1)) • bernsteinPolynomial R n k =
      ↑(choose n k) * ((1 - X) ^ (n - k) * (↑k * (↑(k - 1) * X ^ (k - 1 - 1)))) * X ^ 2
⊢ ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν =
    ∑ x_1 in Finset.range (n + 1),
      ↑(MvPolynomial.aeval e) (↑(pderiv true) (↑(pderiv true) (x ^ x_1 * y ^ (n - x_1) * ↑(choose n x_1)))) * X ^ 2
[PROOFSTEP]
refine' Finset.sum_congr rfl fun k _ => (w k).trans _
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : ↑(pderiv true) x = 1
pderiv_true_y : ↑(pderiv true) y = 0
e : Bool → R[X] := fun i => bif i then X else 1 - X
w :
  ∀ (k : ℕ),
    (k * (k - 1)) • bernsteinPolynomial R n k =
      ↑(choose n k) * ((1 - X) ^ (n - k) * (↑k * (↑(k - 1) * X ^ (k - 1 - 1)))) * X ^ 2
k : ℕ
x✝ : k ∈ Finset.range (n + 1)
⊢ ↑(choose n k) * ((1 - X) ^ (n - k) * (↑k * (↑(k - 1) * X ^ (k - 1 - 1)))) * X ^ 2 =
    ↑(MvPolynomial.aeval e) (↑(pderiv true) (↑(pderiv true) (x ^ k * y ^ (n - k) * ↑(choose n k)))) * X ^ 2
[PROOFSTEP]
simp only [pderiv_true_x, pderiv_true_y, Algebra.id.smul_eq_mul, nsmul_eq_mul, Bool.cond_true, Bool.cond_false,
  add_zero, zero_add, mul_zero, smul_zero, mul_one, MvPolynomial.aeval_X, MvPolynomial.pderiv_X_self,
  MvPolynomial.pderiv_X_of_ne, Derivation.leibniz_pow, Derivation.leibniz, Derivation.map_coe_nat, map_natCast, map_pow,
  map_mul, map_add]
  -- On the right hand side, we'll just simplify.
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : ↑(pderiv true) x = 1
pderiv_true_y : ↑(pderiv true) y = 0
e : Bool → R[X] := fun i => bif i then X else 1 - X
⊢ ↑(MvPolynomial.aeval e) (↑(pderiv true) (↑(pderiv true) ((x + y) ^ n))) * X ^ 2 = (n * (n - 1)) • X ^ 2
[PROOFSTEP]
simp only [pderiv_one, pderiv_mul, (pderiv _).leibniz_pow, (pderiv _).map_coe_nat, (pderiv true).map_add, pderiv_true_x,
  pderiv_true_y, Algebra.id.smul_eq_mul, add_zero, mul_one, Derivation.map_smul_of_tower, map_nsmul, map_pow, map_add,
  Bool.cond_true, Bool.cond_false, MvPolynomial.aeval_X, add_sub_cancel'_right, one_pow, smul_smul, smul_one_mul]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ ∑ ν in Finset.range (n + 1), (n • X - ↑ν) ^ 2 * bernsteinPolynomial R n ν = n • X * (1 - X)
[PROOFSTEP]
have p :
  ((((Finset.range (n + 1)).sum fun ν => (ν * (ν - 1)) • bernsteinPolynomial R n ν) +
        (1 - (2 * n) • Polynomial.X) * (Finset.range (n + 1)).sum fun ν => ν • bernsteinPolynomial R n ν) +
      n ^ 2 • X ^ 2 * (Finset.range (n + 1)).sum fun ν => bernsteinPolynomial R n ν) =
    _ :=
  rfl
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (↑1 - (2 * n) • X) * ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν =
    ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (↑1 - (2 * n) • X) * ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν
⊢ ∑ ν in Finset.range (n + 1), (n • X - ↑ν) ^ 2 * bernsteinPolynomial R n ν = n • X * (1 - X)
[PROOFSTEP]
conv at p =>
  lhs
  rw [Finset.mul_sum, Finset.mul_sum, ← Finset.sum_add_distrib, ← Finset.sum_add_distrib]
  simp only [← nat_cast_mul]
  simp only [← mul_assoc]
  simp only [← add_mul]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (↑1 - (2 * n) • X) * ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν =
    ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (↑1 - (2 * n) • X) * ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν
| ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (↑1 - (2 * n) • X) * ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν =
    ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (↑1 - (2 * n) • X) * ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν
[PROOFSTEP]
  lhs
  rw [Finset.mul_sum, Finset.mul_sum, ← Finset.sum_add_distrib, ← Finset.sum_add_distrib]
  simp only [← nat_cast_mul]
  simp only [← mul_assoc]
  simp only [← add_mul]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (↑1 - (2 * n) • X) * ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν =
    ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (↑1 - (2 * n) • X) * ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν
| ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (↑1 - (2 * n) • X) * ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν =
    ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (↑1 - (2 * n) • X) * ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν
[PROOFSTEP]
  lhs
  rw [Finset.mul_sum, Finset.mul_sum, ← Finset.sum_add_distrib, ← Finset.sum_add_distrib]
  simp only [← nat_cast_mul]
  simp only [← mul_assoc]
  simp only [← add_mul]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (↑1 - (2 * n) • X) * ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν =
    ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (↑1 - (2 * n) • X) * ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν
| ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (↑1 - (2 * n) • X) * ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν =
    ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (↑1 - (2 * n) • X) * ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν
[PROOFSTEP]
lhs
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (↑1 - (2 * n) • X) * ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν =
    ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (↑1 - (2 * n) • X) * ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν
| ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
      (↑1 - (2 * n) • X) * ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
    n ^ 2 • X ^ 2 * ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν
[PROOFSTEP]
rw [Finset.mul_sum, Finset.mul_sum, ← Finset.sum_add_distrib, ← Finset.sum_add_distrib]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (↑1 - (2 * n) • X) * ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν =
    ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (↑1 - (2 * n) • X) * ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν
| ∑ x in Finset.range (n + 1),
    ((x * (x - 1)) • bernsteinPolynomial R n x + (↑1 - (2 * n) • X) * x • bernsteinPolynomial R n x +
      n ^ 2 • X ^ 2 * bernsteinPolynomial R n x)
[PROOFSTEP]
simp only [← nat_cast_mul]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (↑1 - (2 * n) • X) * ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν =
    ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (↑1 - (2 * n) • X) * ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν
| ∑ x in Finset.range (n + 1),
    (↑(x * (x - 1)) * bernsteinPolynomial R n x + (↑1 - ↑(2 * n) * X) * (↑x * bernsteinPolynomial R n x) +
      ↑(n ^ 2) * X ^ 2 * bernsteinPolynomial R n x)
[PROOFSTEP]
simp only [← mul_assoc]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (↑1 - (2 * n) • X) * ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν =
    ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (↑1 - (2 * n) • X) * ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν
| ∑ x in Finset.range (n + 1),
    (↑(x * (x - 1)) * bernsteinPolynomial R n x + (↑1 - ↑(2 * n) * X) * ↑x * bernsteinPolynomial R n x +
      ↑(n ^ 2) * X ^ 2 * bernsteinPolynomial R n x)
[PROOFSTEP]
simp only [← add_mul]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ x in Finset.range (n + 1),
      (↑(x * (x - 1)) + (↑1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (↑1 - (2 * n) • X) * ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν
⊢ ∑ ν in Finset.range (n + 1), (n • X - ↑ν) ^ 2 * bernsteinPolynomial R n ν = n • X * (1 - X)
[PROOFSTEP]
conv at p =>
  rhs
  rw [sum, sum_smul, sum_mul_smul, ← nat_cast_mul]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ x in Finset.range (n + 1),
      (↑(x * (x - 1)) + (↑1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (↑1 - (2 * n) • X) * ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν
| ∑ x in Finset.range (n + 1),
      (↑(x * (x - 1)) + (↑1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (↑1 - (2 * n) • X) * ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν
[PROOFSTEP]
  rhs
  rw [sum, sum_smul, sum_mul_smul, ← nat_cast_mul]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ x in Finset.range (n + 1),
      (↑(x * (x - 1)) + (↑1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (↑1 - (2 * n) • X) * ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν
| ∑ x in Finset.range (n + 1),
      (↑(x * (x - 1)) + (↑1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (↑1 - (2 * n) • X) * ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν
[PROOFSTEP]
  rhs
  rw [sum, sum_smul, sum_mul_smul, ← nat_cast_mul]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ x in Finset.range (n + 1),
      (↑(x * (x - 1)) + (↑1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (↑1 - (2 * n) • X) * ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν
| ∑ x in Finset.range (n + 1),
      (↑(x * (x - 1)) + (↑1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (↑1 - (2 * n) • X) * ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν
[PROOFSTEP]
rhs
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ x in Finset.range (n + 1),
      (↑(x * (x - 1)) + (↑1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (↑1 - (2 * n) • X) * ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν
| ∑ ν in Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
      (↑1 - (2 * n) • X) * ∑ ν in Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
    n ^ 2 • X ^ 2 * ∑ ν in Finset.range (n + 1), bernsteinPolynomial R n ν
[PROOFSTEP]
rw [sum, sum_smul, sum_mul_smul, ← nat_cast_mul]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ x in Finset.range (n + 1),
      (↑(x * (x - 1)) + (↑1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ↑(n * (n - 1)) * X ^ 2 + (↑1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1
⊢ ∑ ν in Finset.range (n + 1), (n • X - ↑ν) ^ 2 * bernsteinPolynomial R n ν = n • X * (1 - X)
[PROOFSTEP]
calc
  _ = _ := Finset.sum_congr rfl fun k m => ?_
  _ = _ := p
  _ = _ := ?_
[GOAL]
case calc_1
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ x in Finset.range (n + 1),
      (↑(x * (x - 1)) + (↑1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ↑(n * (n - 1)) * X ^ 2 + (↑1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1
k : ℕ
m : k ∈ Finset.range (n + 1)
⊢ (n • X - ↑k) ^ 2 * bernsteinPolynomial R n k =
    (↑(k * (k - 1)) + (↑1 - ↑(2 * n) * X) * ↑k + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n k
[PROOFSTEP]
congr 1
[GOAL]
case calc_1.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ x in Finset.range (n + 1),
      (↑(x * (x - 1)) + (↑1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ↑(n * (n - 1)) * X ^ 2 + (↑1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1
k : ℕ
m : k ∈ Finset.range (n + 1)
⊢ (n • X - ↑k) ^ 2 = ↑(k * (k - 1)) + (↑1 - ↑(2 * n) * X) * ↑k + ↑(n ^ 2) * X ^ 2
[PROOFSTEP]
simp only [← nat_cast_mul, push_cast]
[GOAL]
case calc_1.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ x in Finset.range (n + 1),
      (↑(x * (x - 1)) + (↑1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ↑(n * (n - 1)) * X ^ 2 + (↑1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1
k : ℕ
m : k ∈ Finset.range (n + 1)
⊢ (↑n * X - ↑k) ^ 2 = ↑k * ↑(k - 1) + (1 - 2 * ↑n * X) * ↑k + ↑n ^ 2 * X ^ 2
[PROOFSTEP]
cases k
[GOAL]
case calc_1.e_a.zero
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ x in Finset.range (n + 1),
      (↑(x * (x - 1)) + (↑1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ↑(n * (n - 1)) * X ^ 2 + (↑1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1
m : Nat.zero ∈ Finset.range (n + 1)
⊢ (↑n * X - ↑Nat.zero) ^ 2 = ↑Nat.zero * ↑(Nat.zero - 1) + (1 - 2 * ↑n * X) * ↑Nat.zero + ↑n ^ 2 * X ^ 2
[PROOFSTEP]
simp
[GOAL]
case calc_1.e_a.zero
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ x in Finset.range (n + 1),
      (↑(x * (x - 1)) + (↑1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ↑(n * (n - 1)) * X ^ 2 + (↑1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1
m : Nat.zero ∈ Finset.range (n + 1)
⊢ (↑n * X) ^ 2 = ↑n ^ 2 * X ^ 2
[PROOFSTEP]
ring
[GOAL]
case calc_1.e_a.succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ x in Finset.range (n + 1),
      (↑(x * (x - 1)) + (↑1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ↑(n * (n - 1)) * X ^ 2 + (↑1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1
n✝ : ℕ
m : Nat.succ n✝ ∈ Finset.range (n + 1)
⊢ (↑n * X - ↑(Nat.succ n✝)) ^ 2 =
    ↑(Nat.succ n✝) * ↑(Nat.succ n✝ - 1) + (1 - 2 * ↑n * X) * ↑(Nat.succ n✝) + ↑n ^ 2 * X ^ 2
[PROOFSTEP]
simp
[GOAL]
case calc_1.e_a.succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ x in Finset.range (n + 1),
      (↑(x * (x - 1)) + (↑1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ↑(n * (n - 1)) * X ^ 2 + (↑1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1
n✝ : ℕ
m : Nat.succ n✝ ∈ Finset.range (n + 1)
⊢ (↑n * X - (↑n✝ + 1)) ^ 2 = (↑n✝ + 1) * ↑n✝ + (1 - 2 * ↑n * X) * (↑n✝ + 1) + ↑n ^ 2 * X ^ 2
[PROOFSTEP]
ring
[GOAL]
case calc_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ x in Finset.range (n + 1),
      (↑(x * (x - 1)) + (↑1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ↑(n * (n - 1)) * X ^ 2 + (↑1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1
⊢ ↑(n * (n - 1)) * X ^ 2 + (↑1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1 = n • X * (1 - X)
[PROOFSTEP]
simp only [← nat_cast_mul, push_cast]
[GOAL]
case calc_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ x in Finset.range (n + 1),
      (↑(x * (x - 1)) + (↑1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ↑(n * (n - 1)) * X ^ 2 + (↑1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1
⊢ ↑n * ↑(n - 1) * X ^ 2 + (1 - 2 * ↑n * X) * (↑n * X) + ↑n ^ 2 * X ^ 2 * 1 = ↑n * X * (1 - X)
[PROOFSTEP]
cases n
[GOAL]
case calc_2.zero
R : Type u_1
inst✝ : CommRing R
p :
  ∑ x in Finset.range (Nat.zero + 1),
      (↑(x * (x - 1)) + (↑1 - ↑(2 * Nat.zero) * X) * ↑x + ↑(Nat.zero ^ 2) * X ^ 2) * bernsteinPolynomial R Nat.zero x =
    ↑(Nat.zero * (Nat.zero - 1)) * X ^ 2 + (↑1 - (2 * Nat.zero) • X) * Nat.zero • X + Nat.zero ^ 2 • X ^ 2 * 1
⊢ ↑Nat.zero * ↑(Nat.zero - 1) * X ^ 2 + (1 - 2 * ↑Nat.zero * X) * (↑Nat.zero * X) + ↑Nat.zero ^ 2 * X ^ 2 * 1 =
    ↑Nat.zero * X * (1 - X)
[PROOFSTEP]
simp
[GOAL]
case calc_2.succ
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
p :
  ∑ x in Finset.range (Nat.succ n✝ + 1),
      (↑(x * (x - 1)) + (↑1 - ↑(2 * Nat.succ n✝) * X) * ↑x + ↑(Nat.succ n✝ ^ 2) * X ^ 2) *
        bernsteinPolynomial R (Nat.succ n✝) x =
    ↑(Nat.succ n✝ * (Nat.succ n✝ - 1)) * X ^ 2 + (↑1 - (2 * Nat.succ n✝) • X) * Nat.succ n✝ • X +
      Nat.succ n✝ ^ 2 • X ^ 2 * 1
⊢ ↑(Nat.succ n✝) * ↑(Nat.succ n✝ - 1) * X ^ 2 + (1 - 2 * ↑(Nat.succ n✝) * X) * (↑(Nat.succ n✝) * X) +
      ↑(Nat.succ n✝) ^ 2 * X ^ 2 * 1 =
    ↑(Nat.succ n✝) * X * (1 - X)
[PROOFSTEP]
simp
[GOAL]
case calc_2.succ
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
p :
  ∑ x in Finset.range (Nat.succ n✝ + 1),
      (↑(x * (x - 1)) + (↑1 - ↑(2 * Nat.succ n✝) * X) * ↑x + ↑(Nat.succ n✝ ^ 2) * X ^ 2) *
        bernsteinPolynomial R (Nat.succ n✝) x =
    ↑(Nat.succ n✝ * (Nat.succ n✝ - 1)) * X ^ 2 + (↑1 - (2 * Nat.succ n✝) • X) * Nat.succ n✝ • X +
      Nat.succ n✝ ^ 2 • X ^ 2 * 1
⊢ (↑n✝ + 1) * ↑n✝ * X ^ 2 + (1 - 2 * (↑n✝ + 1) * X) * ((↑n✝ + 1) * X) + (↑n✝ + 1) ^ 2 * X ^ 2 = (↑n✝ + 1) * X * (1 - X)
[PROOFSTEP]
ring


[GOAL]
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
a : S
⊢ ↑(RingHom.mapMatrix (algebraMap R Rₘ)) (↑(leftMulMatrix b) a) =
    ↑(leftMulMatrix (Basis.localizationLocalization Rₘ M Sₘ b)) (↑(algebraMap S Sₘ) a)
[PROOFSTEP]
ext i j
[GOAL]
case a.h
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
a : S
i j : ι
⊢ ↑(RingHom.mapMatrix (algebraMap R Rₘ)) (↑(leftMulMatrix b) a) i j =
    ↑(leftMulMatrix (Basis.localizationLocalization Rₘ M Sₘ b)) (↑(algebraMap S Sₘ) a) i j
[PROOFSTEP]
simp only [Matrix.map_apply, RingHom.mapMatrix_apply, leftMulMatrix_eq_repr_mul, ← map_mul,
  Basis.localizationLocalization_apply, Basis.localizationLocalization_repr_algebraMap]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
a : S
⊢ ↑(norm Rₘ) (↑(algebraMap S Sₘ) a) = ↑(algebraMap R Rₘ) (↑(norm R) a)
[PROOFSTEP]
cases subsingleton_or_nontrivial R
[GOAL]
case inl
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
a : S
h✝ : Subsingleton R
⊢ ↑(norm Rₘ) (↑(algebraMap S Sₘ) a) = ↑(algebraMap R Rₘ) (↑(norm R) a)
[PROOFSTEP]
haveI : Subsingleton Rₘ := Module.subsingleton R Rₘ
[GOAL]
case inl
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
a : S
h✝ : Subsingleton R
this : Subsingleton Rₘ
⊢ ↑(norm Rₘ) (↑(algebraMap S Sₘ) a) = ↑(algebraMap R Rₘ) (↑(norm R) a)
[PROOFSTEP]
simp
[GOAL]
case inr
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
a : S
h✝ : Nontrivial R
⊢ ↑(norm Rₘ) (↑(algebraMap S Sₘ) a) = ↑(algebraMap R Rₘ) (↑(norm R) a)
[PROOFSTEP]
let b := Module.Free.chooseBasis R S
[GOAL]
case inr
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
a : S
h✝ : Nontrivial R
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
⊢ ↑(norm Rₘ) (↑(algebraMap S Sₘ) a) = ↑(algebraMap R Rₘ) (↑(norm R) a)
[PROOFSTEP]
letI := Classical.decEq (Module.Free.ChooseBasisIndex R S)
[GOAL]
case inr
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
a : S
h✝ : Nontrivial R
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
this : DecidableEq (Module.Free.ChooseBasisIndex R S) := Classical.decEq (Module.Free.ChooseBasisIndex R S)
⊢ ↑(norm Rₘ) (↑(algebraMap S Sₘ) a) = ↑(algebraMap R Rₘ) (↑(norm R) a)
[PROOFSTEP]
rw [Algebra.norm_eq_matrix_det (b.localizationLocalization Rₘ M Sₘ), Algebra.norm_eq_matrix_det b, RingHom.map_det, ←
  Algebra.map_leftMulMatrix_localization]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
a : S
⊢ ↑(trace Rₘ Sₘ) (↑(algebraMap S Sₘ) a) = ↑(algebraMap R Rₘ) (↑(trace R S) a)
[PROOFSTEP]
cases subsingleton_or_nontrivial R
[GOAL]
case inl
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
a : S
h✝ : Subsingleton R
⊢ ↑(trace Rₘ Sₘ) (↑(algebraMap S Sₘ) a) = ↑(algebraMap R Rₘ) (↑(trace R S) a)
[PROOFSTEP]
haveI : Subsingleton Rₘ := Module.subsingleton R Rₘ
[GOAL]
case inl
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
a : S
h✝ : Subsingleton R
this : Subsingleton Rₘ
⊢ ↑(trace Rₘ Sₘ) (↑(algebraMap S Sₘ) a) = ↑(algebraMap R Rₘ) (↑(trace R S) a)
[PROOFSTEP]
simp
[GOAL]
case inr
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
a : S
h✝ : Nontrivial R
⊢ ↑(trace Rₘ Sₘ) (↑(algebraMap S Sₘ) a) = ↑(algebraMap R Rₘ) (↑(trace R S) a)
[PROOFSTEP]
let b := Module.Free.chooseBasis R S
[GOAL]
case inr
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
a : S
h✝ : Nontrivial R
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
⊢ ↑(trace Rₘ Sₘ) (↑(algebraMap S Sₘ) a) = ↑(algebraMap R Rₘ) (↑(trace R S) a)
[PROOFSTEP]
letI := Classical.decEq (Module.Free.ChooseBasisIndex R S)
[GOAL]
case inr
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
a : S
h✝ : Nontrivial R
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
this : DecidableEq (Module.Free.ChooseBasisIndex R S) := Classical.decEq (Module.Free.ChooseBasisIndex R S)
⊢ ↑(trace Rₘ Sₘ) (↑(algebraMap S Sₘ) a) = ↑(algebraMap R Rₘ) (↑(trace R S) a)
[PROOFSTEP]
rw [Algebra.trace_eq_matrix_trace (b.localizationLocalization Rₘ M Sₘ), Algebra.trace_eq_matrix_trace b, ←
  Algebra.map_leftMulMatrix_localization]
[GOAL]
case inr
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
a : S
h✝ : Nontrivial R
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
this : DecidableEq (Module.Free.ChooseBasisIndex R S) := Classical.decEq (Module.Free.ChooseBasisIndex R S)
⊢ Matrix.trace (↑(RingHom.mapMatrix (algebraMap R Rₘ)) (↑(leftMulMatrix b) a)) =
    ↑(algebraMap R Rₘ) (Matrix.trace (↑(leftMulMatrix b) a))
[PROOFSTEP]
exact (AddMonoidHom.map_trace (algebraMap R Rₘ).toAddMonoidHom _).symm
[GOAL]
R : Type u_1
S : Type u_2
inst✝²¹ : CommRing R
inst✝²⁰ : CommRing S
inst✝¹⁹ : Algebra R S
Rₘ : Type u_3
Sₘ✝ : Type u_4
inst✝¹⁸ : CommRing Rₘ
inst✝¹⁷ : Algebra R Rₘ
inst✝¹⁶ : CommRing Sₘ✝
inst✝¹⁵ : Algebra S Sₘ✝
M : Submonoid R
inst✝¹⁴ : IsLocalization M Rₘ
inst✝¹³ : IsLocalization (algebraMapSubmonoid S M) Sₘ✝
inst✝¹² : Algebra Rₘ Sₘ✝
inst✝¹¹ : Algebra R Sₘ✝
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ✝
inst✝⁹ : IsScalarTower R S Sₘ✝
Sₘ : Type u_5
inst✝⁸ : CommRing Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
⊢ traceMatrix Rₘ ↑(Basis.localizationLocalization Rₘ M Sₘ b) = ↑(RingHom.mapMatrix (algebraMap R Rₘ)) (traceMatrix R ↑b)
[PROOFSTEP]
have : Module.Finite R S := Module.Finite.of_basis b
[GOAL]
R : Type u_1
S : Type u_2
inst✝²¹ : CommRing R
inst✝²⁰ : CommRing S
inst✝¹⁹ : Algebra R S
Rₘ : Type u_3
Sₘ✝ : Type u_4
inst✝¹⁸ : CommRing Rₘ
inst✝¹⁷ : Algebra R Rₘ
inst✝¹⁶ : CommRing Sₘ✝
inst✝¹⁵ : Algebra S Sₘ✝
M : Submonoid R
inst✝¹⁴ : IsLocalization M Rₘ
inst✝¹³ : IsLocalization (algebraMapSubmonoid S M) Sₘ✝
inst✝¹² : Algebra Rₘ Sₘ✝
inst✝¹¹ : Algebra R Sₘ✝
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ✝
inst✝⁹ : IsScalarTower R S Sₘ✝
Sₘ : Type u_5
inst✝⁸ : CommRing Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
this : Module.Finite R S
⊢ traceMatrix Rₘ ↑(Basis.localizationLocalization Rₘ M Sₘ b) = ↑(RingHom.mapMatrix (algebraMap R Rₘ)) (traceMatrix R ↑b)
[PROOFSTEP]
have : Module.Free R S := Module.Free.of_basis b
[GOAL]
R : Type u_1
S : Type u_2
inst✝²¹ : CommRing R
inst✝²⁰ : CommRing S
inst✝¹⁹ : Algebra R S
Rₘ : Type u_3
Sₘ✝ : Type u_4
inst✝¹⁸ : CommRing Rₘ
inst✝¹⁷ : Algebra R Rₘ
inst✝¹⁶ : CommRing Sₘ✝
inst✝¹⁵ : Algebra S Sₘ✝
M : Submonoid R
inst✝¹⁴ : IsLocalization M Rₘ
inst✝¹³ : IsLocalization (algebraMapSubmonoid S M) Sₘ✝
inst✝¹² : Algebra Rₘ Sₘ✝
inst✝¹¹ : Algebra R Sₘ✝
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ✝
inst✝⁹ : IsScalarTower R S Sₘ✝
Sₘ : Type u_5
inst✝⁸ : CommRing Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
this✝ : Module.Finite R S
this : Module.Free R S
⊢ traceMatrix Rₘ ↑(Basis.localizationLocalization Rₘ M Sₘ b) = ↑(RingHom.mapMatrix (algebraMap R Rₘ)) (traceMatrix R ↑b)
[PROOFSTEP]
ext i j : 2
[GOAL]
case a.h
R : Type u_1
S : Type u_2
inst✝²¹ : CommRing R
inst✝²⁰ : CommRing S
inst✝¹⁹ : Algebra R S
Rₘ : Type u_3
Sₘ✝ : Type u_4
inst✝¹⁸ : CommRing Rₘ
inst✝¹⁷ : Algebra R Rₘ
inst✝¹⁶ : CommRing Sₘ✝
inst✝¹⁵ : Algebra S Sₘ✝
M : Submonoid R
inst✝¹⁴ : IsLocalization M Rₘ
inst✝¹³ : IsLocalization (algebraMapSubmonoid S M) Sₘ✝
inst✝¹² : Algebra Rₘ Sₘ✝
inst✝¹¹ : Algebra R Sₘ✝
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ✝
inst✝⁹ : IsScalarTower R S Sₘ✝
Sₘ : Type u_5
inst✝⁸ : CommRing Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
this✝ : Module.Finite R S
this : Module.Free R S
i j : ι
⊢ traceMatrix Rₘ (↑(Basis.localizationLocalization Rₘ M Sₘ b)) i j =
    ↑(RingHom.mapMatrix (algebraMap R Rₘ)) (traceMatrix R ↑b) i j
[PROOFSTEP]
simp_rw [RingHom.mapMatrix_apply, Matrix.map_apply, traceMatrix_apply, traceForm_apply,
  Basis.localizationLocalization_apply, ← map_mul]
[GOAL]
case a.h
R : Type u_1
S : Type u_2
inst✝²¹ : CommRing R
inst✝²⁰ : CommRing S
inst✝¹⁹ : Algebra R S
Rₘ : Type u_3
Sₘ✝ : Type u_4
inst✝¹⁸ : CommRing Rₘ
inst✝¹⁷ : Algebra R Rₘ
inst✝¹⁶ : CommRing Sₘ✝
inst✝¹⁵ : Algebra S Sₘ✝
M : Submonoid R
inst✝¹⁴ : IsLocalization M Rₘ
inst✝¹³ : IsLocalization (algebraMapSubmonoid S M) Sₘ✝
inst✝¹² : Algebra Rₘ Sₘ✝
inst✝¹¹ : Algebra R Sₘ✝
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ✝
inst✝⁹ : IsScalarTower R S Sₘ✝
Sₘ : Type u_5
inst✝⁸ : CommRing Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
this✝ : Module.Finite R S
this : Module.Free R S
i j : ι
⊢ ↑(trace Rₘ Sₘ) (↑(algebraMap S Sₘ) (↑b i * ↑b j)) = ↑(algebraMap R Rₘ) (↑(trace R S) (↑b i * ↑b j))
[PROOFSTEP]
exact Algebra.trace_localization R M _
[GOAL]
R : Type u_1
S : Type u_2
inst✝²¹ : CommRing R
inst✝²⁰ : CommRing S
inst✝¹⁹ : Algebra R S
Rₘ : Type u_3
Sₘ✝ : Type u_4
inst✝¹⁸ : CommRing Rₘ
inst✝¹⁷ : Algebra R Rₘ
inst✝¹⁶ : CommRing Sₘ✝
inst✝¹⁵ : Algebra S Sₘ✝
M : Submonoid R
inst✝¹⁴ : IsLocalization M Rₘ
inst✝¹³ : IsLocalization (algebraMapSubmonoid S M) Sₘ✝
inst✝¹² : Algebra Rₘ Sₘ✝
inst✝¹¹ : Algebra R Sₘ✝
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ✝
inst✝⁹ : IsScalarTower R S Sₘ✝
Sₘ : Type u_5
inst✝⁸ : CommRing Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
⊢ discr Rₘ ↑(Basis.localizationLocalization Rₘ M Sₘ b) = ↑(algebraMap R Rₘ) (discr R ↑b)
[PROOFSTEP]
rw [Algebra.discr_def, Algebra.discr_def, RingHom.map_det, Algebra.traceMatrix_localizationLocalization]