awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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),
    ((↑(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
| ∑ ν ∈ 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
    rw [Finset.mul_sum, Finset.mul_sum, ← Finset.sum_add_distrib, ← Finset.sum_add_distrib]
    simp only [← natCast_mul]
    simp only [← mul_assoc]
    simp only [← add_mul]

Premises used: add_mul, Finset.mul_sum, Finset.sum_add_distrib, Polynomial.natCast_mul, 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 ν
⊢ ∑ 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 =
    ∑ ν ∈ 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:
conv at p =>
    lhs
    rw [Finset.mul_sum, Finset.mul_sum, ← Finset.sum_add_distrib, ← Finset.sum_add_distrib]
    simp only [← natCast_mul]
    simp only [← mul_assoc]
    simp only [← add_mul]

Premises used: add_mul, Finset.mul_sum, Finset.sum_add_distrib, Polynomial.natCast_mul, mul_assoc
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
p :
  ∑ 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 =
    ∑ ν ∈ 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 ν
rhs :
  ∑ ν ∈ 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 ν
| ∑ 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 =
    ∑ ν ∈ 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:
rhs
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
p :
  ∑ 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 =
    ∑ ν ∈ 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 :
  (↑(n * (n - 1)) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
      (1 - HSMul.hSMul (β := R[X]) (2 * n) X) * HSMul.hSMul (β := R[X]) n X +
    HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 * 1
| ∑ ν ∈ 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 [sum, sum_smul, sum_mul_smul, ← natCast_mul]

Premises used: Polynomial.natCast_mul, bernsteinPolynomial.sum_smul, bernsteinPolynomial.sum_mul_smul, bernsteinPolynomial.sum
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
p :
  ∑ 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 =
    ∑ ν ∈ 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 :
  (↑(n * (n - 1)) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
      (1 - HSMul.hSMul (β := R[X]) (2 * n) X) * HSMul.hSMul (β := R[X]) n X +
    HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 * 1
| ∑ 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 =
    ∑ ν ∈ 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:
rhs
    rw [sum, sum_smul, sum_mul_smul, ← natCast_mul]

Premises used: Polynomial.natCast_mul, bernsteinPolynomial.sum_smul, bernsteinPolynomial.sum_mul_smul, bernsteinPolynomial.sum
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
p :
  ∑ 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 =
    ∑ ν ∈ 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 ν
⊢ ∑ 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 =
    (↑(n * (n - 1)) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (1 - HSMul.hSMul (β := R[X]) (2 * n) X) * HSMul.hSMul (β := R[X]) n X +
      HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 * 1

Tactic:
conv at p =>
    rhs
    rw [sum, sum_smul, sum_mul_smul, ← natCast_mul]

Premises used: Polynomial.natCast_mul, bernsteinPolynomial.sum_smul, bernsteinPolynomial.sum_mul_smul, bernsteinPolynomial.sum
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
p :
  ∑ 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 =
    (↑(n * (n - 1)) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (1 - HSMul.hSMul (β := R[X]) (2 * n) X) * HSMul.hSMul (β := R[X]) n X +
      HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 * 1
⊢ Eq.{u_1 + 1} (α := R[X])
    (∑ ν ∈ Finset.range (n + 1),
      HPow.hPow (β := ℕ) (HSMul.hSMul (β := R[X]) n X - (↑ν : R[X])) 2 * bernsteinPolynomial R n ν)
    (∑ 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)

Tactic:
Finset.sum_congr rfl fun k m => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
p :
  ∑ 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 =
    (↑(n * (n - 1)) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (1 - HSMul.hSMul (β := R[X]) (2 * n) X) * HSMul.hSMul (β := R[X]) n X +
      HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 * 1
⊢ ∑ 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 =
    (↑(n * (n - 1)) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (1 - HSMul.hSMul (β := R[X]) (2 * n) X) * HSMul.hSMul (β := R[X]) n X +
      HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 * 1

Tactic:
p
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
p :
  ∑ 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 =
    (↑(n * (n - 1)) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (1 - HSMul.hSMul (β := R[X]) (2 * n) X) * HSMul.hSMul (β := R[X]) n X +
      HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 * 1
⊢ (↑(n * (n - 1)) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (1 - HSMul.hSMul (β := R[X]) (2 * n) X) * HSMul.hSMul (β := R[X]) n X +
      HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 * 1 =
    HSMul.hSMul (β := R[X]) n X * HSub.hSub (α := R[X]) 1 X

Tactic:
?_
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
p :
  ∑ 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 =
    (↑(n * (n - 1)) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (1 - HSMul.hSMul (β := R[X]) (2 * n) X) * HSMul.hSMul (β := R[X]) n X +
      HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 * 1
calc_1 :
  ∀ (k : ℕ) (m : k ∈ Finset.range (n + 1)),
    HPow.hPow (β := ℕ) (HSMul.hSMul (β := R[X]) n X - (↑k : R[X])) 2 * bernsteinPolynomial R n k =
      ((↑(k * (k - 1)) : R[X]) + (1 - HMul.hMul (α := R[X]) (↑(2 * n) : R[X]) X) * (↑k : R[X]) +
          (↑(HPow.hPow (β := ℕ) n 2) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2) *
        bernsteinPolynomial R n k
calc_2 :
  (↑(n * (n - 1)) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (1 - HSMul.hSMul (β := R[X]) (2 * n) X) * HSMul.hSMul (β := R[X]) n X +
      HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 * 1 =
    HSMul.hSMul (β := R[X]) n X * HSub.hSub (α := R[X]) 1 X
⊢ ∑ ν ∈ Finset.range (n + 1),
      HPow.hPow (β := ℕ) (HSMul.hSMul (β := R[X]) n X - (↑ν : R[X])) 2 * bernsteinPolynomial R n ν =
    HSMul.hSMul (β := R[X]) n X * HSub.hSub (α := R[X]) 1 X

Tactic:
calc
    _ = _ := Finset.sum_congr rfl fun k m => ?_
    _ = _ := p
    _ = _ := ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
p :
  ∑ 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 =
    (↑(n * (n - 1)) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (1 - HSMul.hSMul (β := R[X]) (2 * n) X) * HSMul.hSMul (β := R[X]) n X +
      HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 * 1
k : ℕ
m : k ∈ Finset.range (n + 1)
calc_1 :
  HPow.hPow (β := ℕ) (HSMul.hSMul (β := R[X]) n X - (↑k : R[X])) 2 =
    (↑(k * (k - 1)) : R[X]) + (1 - HMul.hMul (α := R[X]) (↑(2 * n) : R[X]) X) * (↑k : R[X]) +
      (↑(HPow.hPow (β := ℕ) n 2) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2
⊢ HPow.hPow (β := ℕ) (HSMul.hSMul (β := R[X]) n X - (↑k : R[X])) 2 * bernsteinPolynomial R n k =
    ((↑(k * (k - 1)) : R[X]) + (1 - HMul.hMul (α := R[X]) (↑(2 * n) : R[X]) X) * (↑k : R[X]) +
        (↑(HPow.hPow (β := ℕ) n 2) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2) *
      bernsteinPolynomial R n k

Tactic:
congr 1
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
p :
  ∑ 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 =
    (↑(n * (n - 1)) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (1 - HSMul.hSMul (β := R[X]) (2 * n) X) * HSMul.hSMul (β := R[X]) n X +
      HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 * 1
k : ℕ
m : k ∈ Finset.range (n + 1)
calc_1 :
  HPow.hPow (β := ℕ) (HMul.hMul (α := R[X]) (↑n : R[X]) X - (↑k : R[X])) 2 =
    HMul.hMul (α := R[X]) (↑k : R[X]) (↑(k - 1) : R[X]) + (1 - HMul.hMul (α := R[X]) 2 (↑n : R[X]) * X) * (↑k : R[X]) +
      HPow.hPow (α := R[X]) (β := ℕ) (↑n : R[X]) 2 * HPow.hPow (α := R[X]) (β := ℕ) X 2
⊢ HPow.hPow (β := ℕ) (HSMul.hSMul (β := R[X]) n X - (↑k : R[X])) 2 =
    (↑(k * (k - 1)) : R[X]) + (1 - HMul.hMul (α := R[X]) (↑(2 * n) : R[X]) X) * (↑k : R[X]) +
      (↑(HPow.hPow (β := ℕ) n 2) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2

Tactic:
simp only [← natCast_mul, push_cast]

Premises used: Polynomial.natCast_mul
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
p :
  ∑ 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 =
    (↑(n * (n - 1)) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (1 - HSMul.hSMul (β := R[X]) (2 * n) X) * HSMul.hSMul (β := R[X]) n X +
      HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 * 1
k : ℕ
m : k ∈ Finset.range (n + 1)
calc_1 :
  ∀ (m : 0 ∈ Finset.range (n + 1)),
    HPow.hPow (β := ℕ) (HMul.hMul (α := R[X]) (↑n : R[X]) X - (↑0 : R[X])) 2 =
      HMul.hMul (α := R[X]) (↑0 : R[X]) (↑(HSub.hSub (α := ℕ) 0 1) : R[X]) +
          (1 - HMul.hMul (α := R[X]) 2 (↑n : R[X]) * X) * (↑0 : R[X]) +
        HPow.hPow (α := R[X]) (β := ℕ) (↑n : R[X]) 2 * HPow.hPow (α := R[X]) (β := ℕ) X 2
calc_1₁ :
  ∀ (n_1 : ℕ) (m : n_1 + 1 ∈ Finset.range (n + 1)),
    HPow.hPow (β := ℕ) (HMul.hMul (α := R[X]) (↑n : R[X]) X - (↑(n_1 + 1) : R[X])) 2 =
      HMul.hMul (α := R[X]) (↑(n_1 + 1) : R[X]) (↑(n_1 + 1 - 1) : R[X]) +
          (1 - HMul.hMul (α := R[X]) 2 (↑n : R[X]) * X) * (↑(n_1 + 1) : R[X]) +
        HPow.hPow (α := R[X]) (β := ℕ) (↑n : R[X]) 2 * HPow.hPow (α := R[X]) (β := ℕ) X 2
⊢ HPow.hPow (β := ℕ) (HMul.hMul (α := R[X]) (↑n : R[X]) X - (↑k : R[X])) 2 =
    HMul.hMul (α := R[X]) (↑k : R[X]) (↑(k - 1) : R[X]) + (1 - HMul.hMul (α := R[X]) 2 (↑n : R[X]) * X) * (↑k : R[X]) +
      HPow.hPow (α := R[X]) (β := ℕ) (↑n : R[X]) 2 * HPow.hPow (α := R[X]) (β := ℕ) X 2

Tactic:
cases k
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
p :
  ∑ 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 =
    (↑(n * (n - 1)) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (1 - HSMul.hSMul (β := R[X]) (2 * n) X) * HSMul.hSMul (β := R[X]) n X +
      HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 * 1
m : 0 ∈ Finset.range (n + 1)
calc_1 :
  HPow.hPow (β := ℕ) (HMul.hMul (α := R[X]) (↑n : R[X]) X) 2 =
    HPow.hPow (α := R[X]) (β := ℕ) (↑n : R[X]) 2 * HPow.hPow (α := R[X]) (β := ℕ) X 2
⊢ HPow.hPow (β := ℕ) (HMul.hMul (α := R[X]) (↑n : R[X]) X - (↑0 : R[X])) 2 =
    HMul.hMul (α := R[X]) (↑0 : R[X]) (↑(HSub.hSub (α := ℕ) 0 1) : R[X]) +
        (1 - HMul.hMul (α := R[X]) 2 (↑n : R[X]) * X) * (↑0 : R[X]) +
      HPow.hPow (α := R[X]) (β := ℕ) (↑n : R[X]) 2 * HPow.hPow (α := R[X]) (β := ℕ) X 2

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

Tactic:
ring
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
p :
  ∑ 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 =
    (↑(n * (n - 1)) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (1 - HSMul.hSMul (β := R[X]) (2 * n) X) * HSMul.hSMul (β := R[X]) n X +
      HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 * 1
n_1 : ℕ
m : n_1 + 1 ∈ Finset.range (n + 1)
calc_1 :
  HPow.hPow (β := ℕ) (HMul.hMul (α := R[X]) (↑n : R[X]) X - HAdd.hAdd (α := R[X]) (↑n_1 : R[X]) 1) 2 =
    HAdd.hAdd (α := R[X]) (↑n_1 : R[X]) 1 * (↑n_1 : R[X]) +
        (1 - HMul.hMul (α := R[X]) 2 (↑n : R[X]) * X) * HAdd.hAdd (α := R[X]) (↑n_1 : R[X]) 1 +
      HPow.hPow (α := R[X]) (β := ℕ) (↑n : R[X]) 2 * HPow.hPow (α := R[X]) (β := ℕ) X 2
⊢ HPow.hPow (β := ℕ) (HMul.hMul (α := R[X]) (↑n : R[X]) X - (↑(n_1 + 1) : R[X])) 2 =
    HMul.hMul (α := R[X]) (↑(n_1 + 1) : R[X]) (↑(n_1 + 1 - 1) : R[X]) +
        (1 - HMul.hMul (α := R[X]) 2 (↑n : R[X]) * X) * (↑(n_1 + 1) : R[X]) +
      HPow.hPow (α := R[X]) (β := ℕ) (↑n : R[X]) 2 * HPow.hPow (α := R[X]) (β := ℕ) X 2

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
p :
  ∑ 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 =
    (↑(n * (n - 1)) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (1 - HSMul.hSMul (β := R[X]) (2 * n) X) * HSMul.hSMul (β := R[X]) n X +
      HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 * 1
n_1 : ℕ
m : n_1 + 1 ∈ Finset.range (n + 1)
⊢ HPow.hPow (β := ℕ) (HMul.hMul (α := R[X]) (↑n : R[X]) X - HAdd.hAdd (α := R[X]) (↑n_1 : R[X]) 1) 2 =
    HAdd.hAdd (α := R[X]) (↑n_1 : R[X]) 1 * (↑n_1 : R[X]) +
        (1 - HMul.hMul (α := R[X]) 2 (↑n : R[X]) * X) * HAdd.hAdd (α := R[X]) (↑n_1 : R[X]) 1 +
      HPow.hPow (α := R[X]) (β := ℕ) (↑n : R[X]) 2 * HPow.hPow (α := R[X]) (β := ℕ) X 2

Tactic:
ring
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
p :
  ∑ 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 =
    (↑(n * (n - 1)) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (1 - HSMul.hSMul (β := R[X]) (2 * n) X) * HSMul.hSMul (β := R[X]) n X +
      HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 * 1
calc_2 :
  HMul.hMul (α := R[X]) (↑n : R[X]) (↑(n - 1) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (1 - HMul.hMul (α := R[X]) 2 (↑n : R[X]) * X) * HMul.hMul (α := R[X]) (↑n : R[X]) X +
      HPow.hPow (α := R[X]) (β := ℕ) (↑n : R[X]) 2 * HPow.hPow (α := R[X]) (β := ℕ) X 2 * 1 =
    HMul.hMul (α := R[X]) (↑n : R[X]) X * HSub.hSub (α := R[X]) 1 X
⊢ (↑(n * (n - 1)) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (1 - HSMul.hSMul (β := R[X]) (2 * n) X) * HSMul.hSMul (β := R[X]) n X +
      HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 * 1 =
    HSMul.hSMul (β := R[X]) n X * HSub.hSub (α := R[X]) 1 X

Tactic:
simp only [← natCast_mul, push_cast]

Premises used: Polynomial.natCast_mul