awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
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
⊢ ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) (ν * (ν - 1)) (bernsteinPolynomial R n ν) =
    (n * (n - 1)) • HPow.hPow (α := R[X]) (β := ℕ) X 2
have 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)
Tactic: trans MvPolynomial.aeval e (pderiv true (pderiv true ((x + y) ^ n))) * X ^ 2
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
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)
⊢ ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) (ν * (ν - 1)) (bernsteinPolynomial R n ν) =
    (n * (n - 1)) • HPow.hPow (α := R[X]) (β := ℕ) X 2
have 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
Tactic: trans MvPolynomial.aeval e (pderiv true (pderiv true ((x + y) ^ n))) * X ^ 2
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
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 : ℕ
⊢ ((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
have 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)
Tactic: simp only [← natCast_mul, Nat.add_succ_sub_one, add_zero, pow_succ]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
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 : ℕ
⊢ (↑((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)
have 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)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (hypothesis)
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
⊢ ∑ ν ∈ 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)
have 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
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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
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
⊢ ∑ ν ∈ 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)
have 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))
Tactic: rw [add_pow, map_sum (pderiv true), map_sum (pderiv true), map_sum (MvPolynomial.aeval e),
      Finset.sum_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
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))
have 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)
Tactic: refine Finset.sum_congr rfl fun k _ => (w k).trans ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (hypothesis)
Goal:
R : Type u_1
inst : CommRing 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 : ∑ ν ∈ 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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
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), 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 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 ν
Tactic: lhs
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
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), 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 : ∑ 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: rw [Finset.mul_sum, Finset.mul_sum, ← Finset.sum_add_distrib, ← Finset.sum_add_distrib]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
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),
    (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)
have 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)
Tactic: simp only [← natCast_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
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),
    (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)
have 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)
Tactic: simp only [← mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
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),
    (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)
have 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
Tactic: simp only [← add_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
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), 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 : ∑ 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: 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]