awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
⊢ Eq.{u_1 + 1} (α := MvPolynomial Bool R)
    (Pi.single (M := fun (x : Bool) ↦ MvPolynomial Bool R) true 1 true : MvPolynomial Bool R) (1 : MvPolynomial Bool R)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
⊢ Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) x : MvPolynomial Bool R) (1 : MvPolynomial Bool R)

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

Tactic:
rw [pderiv_X]

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

Tactic:
rfl
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x :
  Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) x : MvPolynomial Bool R) (1 : MvPolynomial Bool R)
⊢ Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) y : MvPolynomial Bool R) (0 : MvPolynomial Bool R)

Tactic:
have pderiv_true_y : pderiv true y = 0 := by rw [pderiv_X]; rfl
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x :
  Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) x : MvPolynomial Bool R) (1 : MvPolynomial Bool R)
pderiv_true_y :
  Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) y : MvPolynomial Bool R) (0 : MvPolynomial Bool R)
e : Bool → R[X] := fun (i : Bool) ↦ bif i then X else HSub.hSub (α := R[X]) 1 X
trans :
  ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) ν (bernsteinPolynomial R n ν) =
    HMul.hMul (α := R[X]) (β := R[X])
      ((MvPolynomial.aeval e : (a : MvPolynomial Bool R) → R[X])
          ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) ((x + y) ^ n)) :
        R[X])
      X
trans₁ :
  HMul.hMul (α := R[X]) (β := R[X])
      ((MvPolynomial.aeval e : (a : MvPolynomial Bool R) → R[X])
          ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) ((x + y) ^ n)) :
        R[X])
      X =
    HSMul.hSMul (β := R[X]) n X
⊢ ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) ν (bernsteinPolynomial R n ν) = HSMul.hSMul (β := R[X]) n X

Tactic:
trans MvPolynomial.aeval e (pderiv true ((x + y) ^ n)) * X

Premises used: MvPolynomial.aeval, MvPolynomial.pderiv, Bool.true, HPow.hPow, HAdd.hAdd, Polynomial.X, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x :
  Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) x : MvPolynomial Bool R) (1 : MvPolynomial Bool R)
pderiv_true_y :
  Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) y : MvPolynomial Bool R) (0 : MvPolynomial Bool R)
e : Bool → R[X] := fun (i : Bool) ↦ bif i then X else HSub.hSub (α := R[X]) 1 X
⊢ HSMul.hSMul (α := ℕ) (β := R[X]) 0 (bernsteinPolynomial R n 0) =
    (↑0 : R[X]) * HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 0 1) * HSub.hSub (α := R[X]) 1 X ^ (n - 0) *
        (↑(n.choose 0) : R[X]) *
      X

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x :
  Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) x : MvPolynomial Bool R) (1 : MvPolynomial Bool R)
pderiv_true_y :
  Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) y : MvPolynomial Bool R) (0 : MvPolynomial Bool R)
e : Bool → R[X] := fun (i : Bool) ↦ bif i then X else HSub.hSub (α := R[X]) 1 X
k : ℕ
succ :
  (↑(k + 1) : R[X]) *
      ((↑(n.choose (k + 1)) : R[X]) * (HPow.hPow (α := R[X]) X k * X) * HSub.hSub (α := R[X]) 1 X ^ (n - (k + 1))) =
    (↑(k + 1) : R[X]) * HPow.hPow (α := R[X]) X k * HSub.hSub (α := R[X]) 1 X ^ (n - (k + 1)) *
        (↑(n.choose (k + 1)) : R[X]) *
      X
⊢ (k + 1) •
      ((↑(n.choose (k + 1)) : R[X]) * HPow.hPow (α := R[X]) X (k + 1) * HSub.hSub (α := R[X]) 1 X ^ (n - (k + 1))) =
    (↑(k + 1) : R[X]) * HPow.hPow (α := R[X]) X (k + 1 - 1) * HSub.hSub (α := R[X]) 1 X ^ (n - (k + 1)) *
        (↑(n.choose (k + 1)) : R[X]) *
      X

Tactic:
simp only [← natCast_mul, Nat.add_succ_sub_one, add_zero, pow_succ]

Premises used: pow_succ, Polynomial.natCast_mul, Nat.add_succ_sub_one, add_zero
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x :
  Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) x : MvPolynomial Bool R) (1 : MvPolynomial Bool R)
pderiv_true_y :
  Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) y : MvPolynomial Bool R) (0 : MvPolynomial Bool R)
e : Bool → R[X] := fun (i : Bool) ↦ bif i then X else HSub.hSub (α := R[X]) 1 X
k : ℕ
succ :
  HAdd.hAdd (α := R[X]) (↑k : R[X]) 1 *
      ((↑(n.choose (k + 1)) : R[X]) * (HPow.hPow (α := R[X]) X k * X) * HSub.hSub (α := R[X]) 1 X ^ (n - (k + 1))) =
    HAdd.hAdd (α := R[X]) (↑k : R[X]) 1 * HPow.hPow (α := R[X]) X k * HSub.hSub (α := R[X]) 1 X ^ (n - (k + 1)) *
        (↑(n.choose (k + 1)) : R[X]) *
      X
⊢ (↑(k + 1) : R[X]) *
      ((↑(n.choose (k + 1)) : R[X]) * (HPow.hPow (α := R[X]) X k * X) * HSub.hSub (α := R[X]) 1 X ^ (n - (k + 1))) =
    (↑(k + 1) : R[X]) * HPow.hPow (α := R[X]) X k * HSub.hSub (α := R[X]) 1 X ^ (n - (k + 1)) *
        (↑(n.choose (k + 1)) : R[X]) *
      X

Tactic:
push_cast
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x :
  Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) x : MvPolynomial Bool R) (1 : MvPolynomial Bool R)
pderiv_true_y :
  Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) y : MvPolynomial Bool R) (0 : MvPolynomial Bool R)
e : Bool → R[X] := fun (i : Bool) ↦ bif i then X else HSub.hSub (α := R[X]) 1 X
k : ℕ
⊢ HAdd.hAdd (α := R[X]) (↑k : R[X]) 1 *
      ((↑(n.choose (k + 1)) : R[X]) * (HPow.hPow (α := R[X]) X k * X) * HSub.hSub (α := R[X]) 1 X ^ (n - (k + 1))) =
    HAdd.hAdd (α := R[X]) (↑k : R[X]) 1 * HPow.hPow (α := R[X]) X k * HSub.hSub (α := R[X]) 1 X ^ (n - (k + 1)) *
        (↑(n.choose (k + 1)) : R[X]) *
      X

Tactic:
ring
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x :
  Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) x : MvPolynomial Bool R) (1 : MvPolynomial Bool R)
pderiv_true_y :
  Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) y : MvPolynomial Bool R) (0 : MvPolynomial Bool R)
e : Bool → R[X] := fun (i : Bool) ↦ bif i then X else HSub.hSub (α := R[X]) 1 X
⊢ ∀ (k : ℕ),
    HSMul.hSMul (β := R[X]) k (bernsteinPolynomial R n k) =
      (↑k : R[X]) * HPow.hPow (α := R[X]) X (k - 1) * HSub.hSub (α := R[X]) 1 X ^ (n - k) * (↑(n.choose k) : R[X]) * X

Tactic:
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 [← natCast_mul, Nat.add_succ_sub_one, add_zero, pow_succ]
        push_cast
        ring
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x :
  Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) x : MvPolynomial Bool R) (1 : MvPolynomial Bool R)
pderiv_true_y :
  Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) y : MvPolynomial Bool R) (0 : MvPolynomial Bool R)
e : Bool → R[X] := fun (i : Bool) ↦ bif i then X else HSub.hSub (α := R[X]) 1 X
w :
  ∀ (k : ℕ),
    HSMul.hSMul (β := R[X]) k (bernsteinPolynomial R n k) =
      (↑k : R[X]) * HPow.hPow (α := R[X]) X (k - 1) * HSub.hSub (α := R[X]) 1 X ^ (n - k) * (↑(n.choose k) : R[X]) * X
rw :
  Eq.{u_1 + 1} (α := R[X]) (∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) ν (bernsteinPolynomial R n ν))
    (∑ i ∈ Finset.range (n + 1),
      HMul.hMul (α := R[X]) (β := R[X])
        ((MvPolynomial.aeval e : (a : MvPolynomial Bool R) → R[X])
            ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R)
              (x ^ i * y ^ (n - i) * (↑(n.choose i) : MvPolynomial Bool R))) :
          R[X])
        X)
⊢ ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) ν (bernsteinPolynomial R n ν) =
    HMul.hMul (α := R[X]) (β := R[X])
      ((MvPolynomial.aeval e : (a : MvPolynomial Bool R) → R[X])
          ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) ((x + y) ^ n)) :
        R[X])
      X

Tactic:
rw [add_pow, map_sum (pderiv true), map_sum (MvPolynomial.aeval e), Finset.sum_mul]

Premises used: MvPolynomial.aeval, MvPolynomial.pderiv, map_sum, Bool.true, add_pow, Finset.sum_mul
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x :
  Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) x : MvPolynomial Bool R) (1 : MvPolynomial Bool R)
pderiv_true_y :
  Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) y : MvPolynomial Bool R) (0 : MvPolynomial Bool R)
e : Bool → R[X] := fun (i : Bool) ↦ bif i then X else HSub.hSub (α := R[X]) 1 X
w :
  ∀ (k : ℕ),
    HSMul.hSMul (β := R[X]) k (bernsteinPolynomial R n k) =
      (↑k : R[X]) * HPow.hPow (α := R[X]) X (k - 1) * HSub.hSub (α := R[X]) 1 X ^ (n - k) * (↑(n.choose k) : R[X]) * X
⊢ Eq.{u_1 + 1} (α := R[X]) (∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) ν (bernsteinPolynomial R n ν))
    (∑ i ∈ Finset.range (n + 1),
      HMul.hMul (α := R[X]) (β := R[X])
        ((MvPolynomial.aeval e : (a : MvPolynomial Bool R) → R[X])
            ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R)
              (x ^ i * y ^ (n - i) * (↑(n.choose i) : MvPolynomial Bool R))) :
          R[X])
        X)

Tactic:
Finset.sum_congr rfl fun k _ => (w k).trans ?_

Premises used: Finset.sum_congr, rfl, Eq.trans
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x :
  Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) x : MvPolynomial Bool R) (1 : MvPolynomial Bool R)
pderiv_true_y :
  Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) y : MvPolynomial Bool R) (0 : MvPolynomial Bool R)
e : Bool → R[X] := fun (i : Bool) ↦ bif i then X else HSub.hSub (α := R[X]) 1 X
w :
  ∀ (k : ℕ),
    HSMul.hSMul (β := R[X]) k (bernsteinPolynomial R n k) =
      (↑k : R[X]) * HPow.hPow (α := R[X]) X (k - 1) * HSub.hSub (α := R[X]) 1 X ^ (n - k) * (↑(n.choose k) : R[X]) * X
refine :
  ∀ k ∈ Finset.range (n + 1),
    (↑k : R[X]) * HPow.hPow (α := R[X]) X (k - 1) * HSub.hSub (α := R[X]) 1 X ^ (n - k) * (↑(n.choose k) : R[X]) * X =
      HMul.hMul (α := R[X]) (β := R[X])
        ((MvPolynomial.aeval e : (a : MvPolynomial Bool R) → R[X])
            ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R)
              (x ^ k * y ^ (n - k) * (↑(n.choose k) : MvPolynomial Bool R))) :
          R[X])
        X
⊢ Eq.{u_1 + 1} (α := R[X]) (∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) ν (bernsteinPolynomial R n ν))
    (∑ i ∈ Finset.range (n + 1),
      HMul.hMul (α := R[X]) (β := R[X])
        ((MvPolynomial.aeval e : (a : MvPolynomial Bool R) → R[X])
            ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R)
              (x ^ i * y ^ (n - i) * (↑(n.choose i) : MvPolynomial Bool R))) :
          R[X])
        X)

Tactic:
refine Finset.sum_congr rfl fun k _ => (w k).trans ?_

Premises used: Finset.sum_congr, rfl, Eq.trans
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x :
  Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) x : MvPolynomial Bool R) (1 : MvPolynomial Bool R)
pderiv_true_y :
  Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) y : MvPolynomial Bool R) (0 : MvPolynomial Bool R)
e : Bool → R[X] := fun (i : Bool) ↦ bif i then X else HSub.hSub (α := R[X]) 1 X
w :
  ∀ (k : ℕ),
    HSMul.hSMul (β := R[X]) k (bernsteinPolynomial R n k) =
      (↑k : R[X]) * HPow.hPow (α := R[X]) X (k - 1) * HSub.hSub (α := R[X]) 1 X ^ (n - k) * (↑(n.choose k) : R[X]) * X
k : ℕ
h : k ∈ Finset.range (n + 1)
⊢ (↑k : R[X]) * HPow.hPow (α := R[X]) X (k - 1) * HSub.hSub (α := R[X]) 1 X ^ (n - k) * (↑(n.choose k) : R[X]) * X =
    HMul.hMul (α := R[X]) (β := R[X])
      ((MvPolynomial.aeval e : (a : MvPolynomial Bool R) → R[X])
          ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R)
            (x ^ k * y ^ (n - k) * (↑(n.choose k) : MvPolynomial Bool R))) :
        R[X])
      X

Tactic:
simp only [x, y, e, pderiv_true_x, pderiv_true_y, smul_eq_mul, nsmul_eq_mul,
      Bool.cond_true, Bool.cond_false, add_zero, mul_one, mul_zero, MvPolynomial.aeval_X,
      MvPolynomial.pderiv_mul, Derivation.leibniz_pow, Derivation.map_natCast, map_natCast, map_pow,
      map_mul]

Premises used: Derivation.map_natCast, Bool.cond_true, MvPolynomial.aeval_X, MvPolynomial.pderiv_mul, map_pow, MulZeroClass.mul_zero, map_mul, map_natCast, Derivation.leibniz_pow, Bool.cond_false, nsmul_eq_mul, smul_eq_mul, mul_one, add_zero
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x :
  Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) x : MvPolynomial Bool R) (1 : MvPolynomial Bool R)
pderiv_true_y :
  Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) y : MvPolynomial Bool R) (0 : MvPolynomial Bool R)
e : Bool → R[X] := fun (i : Bool) ↦ bif i then X else HSub.hSub (α := R[X]) 1 X
rw :
  HMul.hMul (α := R[X]) (β := R[X])
      ((MvPolynomial.aeval e : (a : MvPolynomial Bool R) → R[X])
          (n • (x + y) ^ (n - 1) • HAdd.hAdd (α := MvPolynomial Bool R) 1 0) :
        R[X])
      X =
    HSMul.hSMul (β := R[X]) n X
⊢ HMul.hMul (α := R[X]) (β := R[X])
      ((MvPolynomial.aeval e : (a : MvPolynomial Bool R) → R[X])
          ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) ((x + y) ^ n)) :
        R[X])
      X =
    HSMul.hSMul (β := R[X]) n X

Tactic:
rw [(pderiv true).leibniz_pow, (pderiv true).map_add, pderiv_true_x, pderiv_true_y]

Premises used: MvPolynomial.pderiv, Bool.true, Derivation.leibniz_pow, Derivation.map_add
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x :
  Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) x : MvPolynomial Bool R) (1 : MvPolynomial Bool R)
pderiv_true_y :
  Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) y : MvPolynomial Bool R) (0 : MvPolynomial Bool R)
e : Bool → R[X] := fun (i : Bool) ↦ bif i then X else HSub.hSub (α := R[X]) 1 X
⊢ HMul.hMul (α := R[X]) (β := R[X])
      ((MvPolynomial.aeval e : (a : MvPolynomial Bool R) → R[X])
          (n • (x + y) ^ (n - 1) • HAdd.hAdd (α := MvPolynomial Bool R) 1 0) :
        R[X])
      X =
    HSMul.hSMul (β := R[X]) n X

Tactic:
simp only [x, y, e, 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,
      one_pow, add_zero, mul_one]

Premises used: one_pow, Bool.cond_true, MvPolynomial.aeval_X, map_add, map_pow, map_mul, map_natCast, add_sub_cancel, Bool.cond_false, nsmul_eq_mul, smul_eq_mul, mul_one, add_zero
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x :
  Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) x : MvPolynomial Bool R) (1 : MvPolynomial Bool R)
pderiv_true_y :
  Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) y : MvPolynomial Bool R) (0 : MvPolynomial Bool R)
e : Bool → R[X] := fun (i : Bool) ↦ bif i then X else HSub.hSub (α := R[X]) 1 X
trans :
  ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) (ν * (ν - 1)) (bernsteinPolynomial R n ν) =
    HMul.hMul (α := R[X])
      ((MvPolynomial.aeval e : (a : MvPolynomial Bool R) → R[X])
          ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R)
            ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) ((x + y) ^ n))) :
        R[X])
      (HPow.hPow (α := R[X]) (β := ℕ) X 2)
trans₁ :
  HMul.hMul (α := R[X])
      ((MvPolynomial.aeval e : (a : MvPolynomial Bool R) → R[X])
          ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R)
            ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) ((x + y) ^ n))) :
        R[X])
      (HPow.hPow (α := R[X]) (β := ℕ) X 2) =
    (n * (n - 1)) • HPow.hPow (α := R[X]) (β := ℕ) X 2
⊢ ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) (ν * (ν - 1)) (bernsteinPolynomial R n ν) =
    (n * (n - 1)) • HPow.hPow (α := R[X]) (β := ℕ) X 2

Tactic:
trans MvPolynomial.aeval e (pderiv true (pderiv true ((x + y) ^ n))) * X ^ 2

Premises used: MvPolynomial.aeval, MvPolynomial.pderiv, Bool.true, HPow.hPow, HAdd.hAdd, Polynomial.X, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x :
  Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) x : MvPolynomial Bool R) (1 : MvPolynomial Bool R)
pderiv_true_y :
  Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) y : MvPolynomial Bool R) (0 : MvPolynomial Bool R)
e : Bool → R[X] := fun (i : Bool) ↦ bif i then X else HSub.hSub (α := R[X]) 1 X
⊢ HSMul.hSMul (β := R[X]) (0 * HSub.hSub (α := ℕ) 0 1) (bernsteinPolynomial R n 0) =
    (↑(n.choose 0) : R[X]) *
        (HSub.hSub (α := R[X]) 1 X ^ (n - 0) *
          ((↑0 : R[X]) * ((↑(HSub.hSub (α := ℕ) 0 1) : R[X]) * HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 0 1 - 1)))) *
      HPow.hPow (α := R[X]) (β := ℕ) X 2

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x :
  Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) x : MvPolynomial Bool R) (1 : MvPolynomial Bool R)
pderiv_true_y :
  Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) y : MvPolynomial Bool R) (0 : MvPolynomial Bool R)
e : Bool → R[X] := fun (i : Bool) ↦ bif i then X else HSub.hSub (α := R[X]) 1 X
⊢ HSMul.hSMul (β := R[X]) (HAdd.hAdd (α := ℕ) 0 1 * (HAdd.hAdd (α := ℕ) 0 1 - 1))
      (bernsteinPolynomial R n (HAdd.hAdd (α := ℕ) 0 1)) =
    (↑(n.choose (HAdd.hAdd (α := ℕ) 0 1)) : R[X]) *
        (HSub.hSub (α := R[X]) 1 X ^ (n - HAdd.hAdd (α := ℕ) 0 1) *
          ((↑(HAdd.hAdd (α := ℕ) 0 1) : R[X]) *
            ((↑(HAdd.hAdd (α := ℕ) 0 1 - 1) : R[X]) * HPow.hPow (α := R[X]) X (HAdd.hAdd (α := ℕ) 0 1 - 1 - 1)))) *
      HPow.hPow (α := R[X]) (β := ℕ) X 2

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x :
  Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) x : MvPolynomial Bool R) (1 : MvPolynomial Bool R)
pderiv_true_y :
  Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) y : MvPolynomial Bool R) (0 : MvPolynomial Bool R)
e : Bool → R[X] := fun (i : Bool) ↦ bif i then X else HSub.hSub (α := R[X]) 1 X
k : ℕ
succ :
  (↑((k + 1 + 1) * (k + 1)) : R[X]) *
      ((↑(n.choose (k + 1 + 1)) : R[X]) * (HPow.hPow (α := R[X]) X k * X * X) *
        HSub.hSub (α := R[X]) 1 X ^ (n - (k + 1 + 1))) =
    (↑(n.choose (k + 1 + 1)) : R[X]) *
        (HSub.hSub (α := R[X]) 1 X ^ (n - (k + 1 + 1)) *
          ((↑(k + 1 + 1) : R[X]) * ((↑(k + 1) : R[X]) * HPow.hPow (α := R[X]) X k))) *
      (HPow.hPow (α := R[X]) (β := ℕ) X 0 * X * X)
⊢ ((k + 1 + 1) * (k + 1 + 1 - 1)) •
      ((↑(n.choose (k + 1 + 1)) : R[X]) * HPow.hPow (α := R[X]) X (k + 1 + 1) *
        HSub.hSub (α := R[X]) 1 X ^ (n - (k + 1 + 1))) =
    (↑(n.choose (k + 1 + 1)) : R[X]) *
        (HSub.hSub (α := R[X]) 1 X ^ (n - (k + 1 + 1)) *
          ((↑(k + 1 + 1) : R[X]) * ((↑(k + 1 + 1 - 1) : R[X]) * HPow.hPow (α := R[X]) X (k + 1 + 1 - 1 - 1)))) *
      HPow.hPow (α := R[X]) (β := ℕ) X 2

Tactic:
simp only [← natCast_mul, Nat.add_succ_sub_one, add_zero, pow_succ]

Premises used: pow_succ, Polynomial.natCast_mul, Nat.add_succ_sub_one, add_zero