awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (hypothesis)
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 ν
⊢ ∑ ν ∈ 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
have 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 ν
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]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
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 =
    ∑ ν ∈ 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 ν
have 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 ν
Tactic: rhs
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
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 ν
| ∑ ν ∈ 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 ν
have 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
Tactic: rw [sum, sum_smul, sum_mul_smul, ← natCast_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
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 =
    ∑ ν ∈ 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 ν
have 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
Tactic: rhs
    rw [sum, sum_smul, sum_mul_smul, ← natCast_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (hypothesis)
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 ν
⊢ ∑ ν ∈ 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
have 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
Tactic: conv at p =>
    rhs
    rw [sum, sum_smul, sum_mul_smul, ← natCast_mul]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
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
⊢ ∑ ν ∈ 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
have 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
Tactic: calc
    _ = _ := Finset.sum_congr rfl fun k m => ?_
    _ = _ := p
    _ = _ := ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
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
⊢ ∑ ν ∈ 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
have 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
Tactic: calc
    _ = _ := Finset.sum_congr rfl fun k m => ?_
    _ = _ := p
    _ = _ := ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
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)
⊢ 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
have 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
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
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)
⊢ 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
have 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
Tactic: simp only [← natCast_mul, push_cast]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
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)
⊢ 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
have 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
Tactic: cases k
Cleared hypotheses: k, m
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
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
⊢ 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
have 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
Tactic: cases k
Cleared hypotheses: k, m
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
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 - (↑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
have 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
Tactic: simp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
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 - (↑(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
have 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
Tactic: simp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
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
have 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
Tactic: simp only [← natCast_mul, push_cast]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
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
⊢ 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
have calc_2 : ∀
  (p :
    ∑ x ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1),
        ((↑(x * (x - 1)) : R[X]) + (1 - HMul.hMul (α := R[X]) (↑(HMul.hMul (α := ℕ) 2 0) : R[X]) X) * (↑x : R[X]) +
            (↑(HPow.hPow (α := ℕ) (β := ℕ) 0 2) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2) *
          bernsteinPolynomial R 0 x =
      (↑(0 * HSub.hSub (α := ℕ) 0 1) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
          (1 - HSMul.hSMul (β := R[X]) (HMul.hMul (α := ℕ) 2 0) X) * HSMul.hSMul (α := ℕ) (β := R[X]) 0 X +
        HPow.hPow (α := ℕ) (β := ℕ) 0 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 * 1),
  HMul.hMul (α := R[X]) (↑0 : R[X]) (↑(HSub.hSub (α := ℕ) 0 1) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (1 - HMul.hMul (α := R[X]) 2 (↑0 : R[X]) * X) * HMul.hMul (α := R[X]) (↑0 : R[X]) X +
      HPow.hPow (α := R[X]) (β := ℕ) (↑0 : R[X]) 2 * HPow.hPow (α := R[X]) (β := ℕ) X 2 * 1 =
    HMul.hMul (α := R[X]) (↑0 : R[X]) X * HSub.hSub (α := R[X]) 1 X
Tactic: cases n
Cleared hypotheses: n, p