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
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 + 1) * HAdd.hAdd (α := R[X]) (↑k : R[X]) 1 *
      ((↑(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)) *
          ((HAdd.hAdd (α := R[X]) (↑k : R[X]) 1 + 1) *
            (HAdd.hAdd (α := R[X]) (↑k : R[X]) 1 * HPow.hPow (α := R[X]) X k))) *
      (HPow.hPow (α := R[X]) (β := ℕ) X 0 * X * X)
⊢ (↑((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)

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 + 1) * HAdd.hAdd (α := R[X]) (↑k : R[X]) 1 *
      ((↑(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)) *
          ((HAdd.hAdd (α := R[X]) (↑k : R[X]) 1 + 1) *
            (HAdd.hAdd (α := R[X]) (↑k : R[X]) 1 * HPow.hPow (α := R[X]) X k))) *
      (HPow.hPow (α := R[X]) (β := ℕ) X 0 * 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 * (k - 1)) (bernsteinPolynomial R n k) =
      (↑(n.choose k) : R[X]) *
          (HSub.hSub (α := R[X]) 1 X ^ (n - k) *
            ((↑k : R[X]) * ((↑(k - 1) : R[X]) * HPow.hPow (α := R[X]) X (k - 1 - 1)))) *
        HPow.hPow (α := R[X]) (β := ℕ) X 2

Tactic:
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 [← 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 * (k - 1)) (bernsteinPolynomial R n k) =
      (↑(n.choose k) : R[X]) *
          (HSub.hSub (α := R[X]) 1 X ^ (n - k) *
            ((↑k : R[X]) * ((↑(k - 1) : R[X]) * HPow.hPow (α := R[X]) X (k - 1 - 1)))) *
        HPow.hPow (α := R[X]) (β := ℕ) X 2
rw :
  Eq.{u_1 + 1} (α := R[X])
    (∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) (ν * (ν - 1)) (bernsteinPolynomial R n ν))
    (∑ i ∈ Finset.range (n + 1),
      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 ^ i * y ^ (n - i) * (↑(n.choose i) : MvPolynomial Bool R)))) :
          R[X])
        (HPow.hPow (α := R[X]) (β := ℕ) X 2))
⊢ ∑ ν ∈ 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)

Tactic:
rw [add_pow, map_sum (pderiv true), 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 * (k - 1)) (bernsteinPolynomial R n k) =
      (↑(n.choose k) : R[X]) *
          (HSub.hSub (α := R[X]) 1 X ^ (n - k) *
            ((↑k : R[X]) * ((↑(k - 1) : R[X]) * HPow.hPow (α := R[X]) X (k - 1 - 1)))) *
        HPow.hPow (α := R[X]) (β := ℕ) X 2
⊢ Eq.{u_1 + 1} (α := R[X])
    (∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) (ν * (ν - 1)) (bernsteinPolynomial R n ν))
    (∑ i ∈ Finset.range (n + 1),
      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 ^ i * y ^ (n - i) * (↑(n.choose i) : MvPolynomial Bool R)))) :
          R[X])
        (HPow.hPow (α := R[X]) (β := ℕ) X 2))

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 * (k - 1)) (bernsteinPolynomial R n k) =
      (↑(n.choose k) : R[X]) *
          (HSub.hSub (α := R[X]) 1 X ^ (n - k) *
            ((↑k : R[X]) * ((↑(k - 1) : R[X]) * HPow.hPow (α := R[X]) X (k - 1 - 1)))) *
        HPow.hPow (α := R[X]) (β := ℕ) X 2
refine :
  ∀ k ∈ Finset.range (n + 1),
    (↑(n.choose k) : R[X]) *
          (HSub.hSub (α := R[X]) 1 X ^ (n - k) *
            ((↑k : R[X]) * ((↑(k - 1) : R[X]) * HPow.hPow (α := R[X]) X (k - 1 - 1)))) *
        HPow.hPow (α := R[X]) (β := ℕ) X 2 =
      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 ^ k * y ^ (n - k) * (↑(n.choose k) : MvPolynomial Bool R)))) :
          R[X])
        (HPow.hPow (α := R[X]) (β := ℕ) X 2)
⊢ Eq.{u_1 + 1} (α := R[X])
    (∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) (ν * (ν - 1)) (bernsteinPolynomial R n ν))
    (∑ i ∈ Finset.range (n + 1),
      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 ^ i * y ^ (n - i) * (↑(n.choose i) : MvPolynomial Bool R)))) :
          R[X])
        (HPow.hPow (α := R[X]) (β := ℕ) X 2))

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 * (k - 1)) (bernsteinPolynomial R n k) =
      (↑(n.choose k) : R[X]) *
          (HSub.hSub (α := R[X]) 1 X ^ (n - k) *
            ((↑k : R[X]) * ((↑(k - 1) : R[X]) * HPow.hPow (α := R[X]) X (k - 1 - 1)))) *
        HPow.hPow (α := R[X]) (β := ℕ) X 2
k : ℕ
h : k ∈ Finset.range (n + 1)
⊢ (↑(n.choose k) : R[X]) *
        (HSub.hSub (α := R[X]) 1 X ^ (n - k) *
          ((↑k : R[X]) * ((↑(k - 1) : R[X]) * HPow.hPow (α := R[X]) X (k - 1 - 1)))) *
      HPow.hPow (α := R[X]) (β := ℕ) X 2 =
    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 ^ k * y ^ (n - k) * (↑(n.choose k) : MvPolynomial Bool R)))) :
        R[X])
      (HPow.hPow (α := R[X]) (β := ℕ) X 2)

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, zero_add, mul_zero, mul_one,
      MvPolynomial.aeval_X,
      Derivation.leibniz_pow, Derivation.leibniz, Derivation.map_natCast, map_natCast, map_pow,
      map_mul]

Premises used: Derivation.map_natCast, Bool.cond_true, MvPolynomial.aeval_X, map_pow, zero_add, MulZeroClass.mul_zero, Derivation.leibniz, 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
⊢ 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

Tactic:
simp only [x, y, e, (pderiv _).leibniz_pow,
      (pderiv true).map_add, pderiv_true_x, pderiv_true_y, smul_eq_mul, add_zero,
      mul_one, map_nsmul, map_pow, map_add, Bool.cond_true,
      Bool.cond_false, MvPolynomial.aeval_X, add_sub_cancel, one_pow, smul_smul,
      smul_one_mul]

Premises used: one_pow, Bool.cond_true, MvPolynomial.aeval_X, smul_smul, map_add, MvPolynomial.pderiv, map_pow, Bool.true, add_sub_cancel, smul_one_mul, Derivation.leibniz_pow, Bool.cond_false, Derivation.map_add, smul_eq_mul, mul_one, add_zero, map_nsmul
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
⊢ ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) (ν * (ν - 1)) (bernsteinPolynomial R n ν) +
        (1 - HSMul.hSMul (β := R[X]) (2 * n) X) *
          ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) ν (bernsteinPolynomial R n ν) +
      HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 *
        ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν =
    ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) (ν * (ν - 1)) (bernsteinPolynomial R n ν) +
        (1 - HSMul.hSMul (β := R[X]) (2 * n) X) *
          ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) ν (bernsteinPolynomial R n ν) +
      HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 *
        ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν

Tactic:
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
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
p :
  ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) (ν * (ν - 1)) (bernsteinPolynomial R n ν) +
        (1 - HSMul.hSMul (β := R[X]) (2 * n) X) *
          ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) ν (bernsteinPolynomial R n ν) +
      HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 *
        ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν =
    ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) (ν * (ν - 1)) (bernsteinPolynomial R n ν) +
        (1 - HSMul.hSMul (β := R[X]) (2 * n) X) *
          ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) ν (bernsteinPolynomial R n ν) +
      HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 *
        ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν
lhs :
  ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) (ν * (ν - 1)) (bernsteinPolynomial R n ν) +
      (1 - HSMul.hSMul (β := R[X]) (2 * n) X) *
        ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) ν (bernsteinPolynomial R n ν) +
    HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 * ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν
| ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) (ν * (ν - 1)) (bernsteinPolynomial R n ν) +
        (1 - HSMul.hSMul (β := R[X]) (2 * n) X) *
          ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) ν (bernsteinPolynomial R n ν) +
      HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 *
        ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν =
    ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) (ν * (ν - 1)) (bernsteinPolynomial R n ν) +
        (1 - HSMul.hSMul (β := R[X]) (2 * n) X) *
          ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) ν (bernsteinPolynomial R n ν) +
      HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 *
        ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν

Tactic:
lhs
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
p :
  ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) (ν * (ν - 1)) (bernsteinPolynomial R n ν) +
        (1 - HSMul.hSMul (β := R[X]) (2 * n) X) *
          ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) ν (bernsteinPolynomial R n ν) +
      HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 *
        ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν =
    ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) (ν * (ν - 1)) (bernsteinPolynomial R n ν) +
        (1 - HSMul.hSMul (β := R[X]) (2 * n) X) *
          ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) ν (bernsteinPolynomial R n ν) +
      HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 *
        ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν
rw :
  ∑ x ∈ Finset.range (n + 1),
    (HSMul.hSMul (β := R[X]) (x * (x - 1)) (bernsteinPolynomial R n x) +
        (1 - HSMul.hSMul (β := R[X]) (2 * n) X) * HSMul.hSMul (β := R[X]) x (bernsteinPolynomial R n x) +
      HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 * bernsteinPolynomial R n x)
| ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) (ν * (ν - 1)) (bernsteinPolynomial R n ν) +
      (1 - HSMul.hSMul (β := R[X]) (2 * n) X) *
        ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) ν (bernsteinPolynomial R n ν) +
    HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 * ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν

Tactic:
rw [Finset.mul_sum, Finset.mul_sum, ← Finset.sum_add_distrib, ← Finset.sum_add_distrib]

Premises used: Finset.mul_sum, Finset.sum_add_distrib
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
p :
  ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) (ν * (ν - 1)) (bernsteinPolynomial R n ν) +
        (1 - HSMul.hSMul (β := R[X]) (2 * n) X) *
          ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) ν (bernsteinPolynomial R n ν) +
      HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 *
        ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν =
    ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) (ν * (ν - 1)) (bernsteinPolynomial R n ν) +
        (1 - HSMul.hSMul (β := R[X]) (2 * n) X) *
          ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) ν (bernsteinPolynomial R n ν) +
      HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 *
        ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν
simp :
  ∑ x ∈ Finset.range (n + 1),
    (HMul.hMul (α := R[X]) (↑(x * (x - 1)) : R[X]) (bernsteinPolynomial R n x) +
        (1 - HMul.hMul (α := R[X]) (↑(2 * n) : R[X]) X) *
          HMul.hMul (α := R[X]) (↑x : R[X]) (bernsteinPolynomial R n x) +
      (↑(HPow.hPow (β := ℕ) n 2) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 * bernsteinPolynomial R n x)
| ∑ x ∈ Finset.range (n + 1),
    (HSMul.hSMul (β := R[X]) (x * (x - 1)) (bernsteinPolynomial R n x) +
        (1 - HSMul.hSMul (β := R[X]) (2 * n) X) * HSMul.hSMul (β := R[X]) x (bernsteinPolynomial R n x) +
      HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 * bernsteinPolynomial R n x)

Tactic:
simp only [← natCast_mul]

Premises used: Polynomial.natCast_mul
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
p :
  ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) (ν * (ν - 1)) (bernsteinPolynomial R n ν) +
        (1 - HSMul.hSMul (β := R[X]) (2 * n) X) *
          ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) ν (bernsteinPolynomial R n ν) +
      HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 *
        ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν =
    ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) (ν * (ν - 1)) (bernsteinPolynomial R n ν) +
        (1 - HSMul.hSMul (β := R[X]) (2 * n) X) *
          ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) ν (bernsteinPolynomial R n ν) +
      HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 *
        ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν
simp :
  ∑ x ∈ Finset.range (n + 1),
    (HMul.hMul (α := R[X]) (↑(x * (x - 1)) : R[X]) (bernsteinPolynomial R n x) +
        (1 - HMul.hMul (α := R[X]) (↑(2 * n) : R[X]) X) * (↑x : R[X]) * bernsteinPolynomial R n x +
      (↑(HPow.hPow (β := ℕ) n 2) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 * bernsteinPolynomial R n x)
| ∑ x ∈ Finset.range (n + 1),
    (HMul.hMul (α := R[X]) (↑(x * (x - 1)) : R[X]) (bernsteinPolynomial R n x) +
        (1 - HMul.hMul (α := R[X]) (↑(2 * n) : R[X]) X) *
          HMul.hMul (α := R[X]) (↑x : R[X]) (bernsteinPolynomial R n x) +
      (↑(HPow.hPow (β := ℕ) n 2) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 * bernsteinPolynomial R n x)

Tactic:
simp only [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
p :
  ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) (ν * (ν - 1)) (bernsteinPolynomial R n ν) +
        (1 - HSMul.hSMul (β := R[X]) (2 * n) X) *
          ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) ν (bernsteinPolynomial R n ν) +
      HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 *
        ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν =
    ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) (ν * (ν - 1)) (bernsteinPolynomial R n ν) +
        (1 - HSMul.hSMul (β := R[X]) (2 * n) X) *
          ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) ν (bernsteinPolynomial R n ν) +
      HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 *
        ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν
simp :
  ∑ x ∈ Finset.range (n + 1),
    ((↑(x * (x - 1)) : R[X]) + (1 - HMul.hMul (α := R[X]) (↑(2 * n) : R[X]) X) * (↑x : R[X]) +
        (↑(HPow.hPow (β := ℕ) n 2) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2) *
      bernsteinPolynomial R n x
| ∑ x ∈ Finset.range (n + 1),
    (HMul.hMul (α := R[X]) (↑(x * (x - 1)) : R[X]) (bernsteinPolynomial R n x) +
        (1 - HMul.hMul (α := R[X]) (↑(2 * n) : R[X]) X) * (↑x : R[X]) * bernsteinPolynomial R n x +
      (↑(HPow.hPow (β := ℕ) n 2) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 * bernsteinPolynomial R n x)

Tactic:
simp only [← add_mul]

Premises used: add_mul