awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
n k : ℕ
h : k ≤ n
p : ℚ[X]
m : Membership.mem (γ := Submodule ℚ ℚ[X]) (span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ))) p
refine_1 :
  ∀ (x : ℚ[X])
    (h : Membership.mem (γ := Set ℚ[X]) (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ)) x),
    eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] x) = 0
refine_2 : Eq (α := ℚ) (eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] 0)) 0
⊢ eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] p) = 0
have refine_3 : ∀ (x y : ℚ[X])
  (hx :
    Membership.mem (γ := Submodule ℚ ℚ[X]) (span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ)))
      x)
  (hy :
    Membership.mem (γ := Submodule ℚ ℚ[X]) (span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ)))
      y),
  eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] x) = 0 →
    eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] y) = 0 →
      eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] (x + y)) = 0
Tactic: refine span_induction ?_ ?_ ?_ ?_ m
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
n k : ℕ
h : k ≤ n
p : ℚ[X]
m : Membership.mem (γ := Submodule ℚ ℚ[X]) (span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ))) p
refine_1 :
  ∀ (x : ℚ[X])
    (h : Membership.mem (γ := Set ℚ[X]) (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ)) x),
    eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] x) = 0
refine_2 : Eq (α := ℚ) (eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] 0)) 0
refine_3 :
  ∀ (x y : ℚ[X])
    (hx :
      Membership.mem (γ := Submodule ℚ ℚ[X]) (span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ)))
        x)
    (hy :
      Membership.mem (γ := Submodule ℚ ℚ[X]) (span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ)))
        y),
    eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] x) = 0 →
      eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] y) = 0 →
        eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] (x + y)) = 0
⊢ eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] p) = 0
have refine_4 : ∀ (a : ℚ) (x : ℚ[X])
  (hx :
    Membership.mem (γ := Submodule ℚ ℚ[X]) (span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ)))
      x),
  eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] x) = 0 →
    eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] (a • x)) = 0
Tactic: refine span_induction ?_ ?_ ?_ ?_ m
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
n k : ℕ
h : k ≤ n
p : ℚ[X]
m : Membership.mem (γ := Submodule ℚ ℚ[X]) (span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ))) p
⊢ ∀ (x : ℚ[X])
    (h : Membership.mem (γ := Set ℚ[X]) (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ)) x),
    eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] x) = 0
have refine_1 : ∀ (a : Fin k), eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] (bernsteinPolynomial ℚ n (↑a : ℕ))) = 0
Tactic: simp only [Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
n k : ℕ
h : k ≤ n
p : ℚ[X]
m : Membership.mem (γ := Submodule ℚ ℚ[X]) (span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ))) p
a : ℕ
w : a < k
⊢ eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] (bernsteinPolynomial ℚ n (↑(⟨a, w⟩ : Fin k) : ℕ))) = 0
have refine_1 : eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] (bernsteinPolynomial ℚ n a)) = 0
Tactic: simp only
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
n k : ℕ
h : k ≤ n
p : ℚ[X]
m : Membership.mem (γ := Submodule ℚ ℚ[X]) (span ℚ (Set.range fun (k_1 : Fin k) ↦ bernsteinPolynomial ℚ n (↑k_1 : ℕ))) p
a : ℕ
w : a < k
⊢ eval 1 ((⇑derivative : (a : ℚ[X]) → ℚ[X])^[n - k] (bernsteinPolynomial ℚ n a)) = 0
have refine_1 : Eq (α := ℚ) 0 0
Tactic: rw [iterate_derivative_at_1_eq_zero_of_lt ℚ n ((tsub_lt_tsub_iff_left_of_le h).mpr w)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
n k : ℕ
h : k ≤ n + 1
⊢ LinearIndependent ℚ (M := ℚ[X]) fun (ν : Fin k) ↦ bernsteinPolynomial ℚ n (↑ν : ℕ)
have zero : ∀ (h : 0 ≤ n + 1), LinearIndependent ℚ (M := ℚ[X]) fun (ν : Fin 0) ↦ bernsteinPolynomial ℚ n (↑ν : ℕ)
Tactic: induction k with
  | zero => apply linearIndependent_empty_type
  | succ k ih =>
    apply linearIndependent_finSucc'.mpr
    fconstructor
    · exact ih (le_of_lt h)
    · -- The actual work!
      -- We show that the (n-k)-th derivative at 1 doesn't vanish,
      -- but vanishes for everything in the span.
      clear ih
      simp only [add_le_add_iff_right] at h
      simp only [Fin.val_last, Fin.init_def]
      dsimp
      apply notMem_span_of_apply_notMem_span_image (@Polynomial.derivative ℚ _ ^ (n - k))
      -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to change `span_image` into `span_image _`
      simp only [not_exists, not_and, Submodule.mem_map, Submodule.span_image _]
      intro p m
      apply_fun Polynomial.eval (1 : ℚ)
      simp only [Module.End.pow_apply]
      -- The right-hand side is nonzero,
      -- so it will suffice to show the left-hand side is always zero.
      suffices (Polynomial.derivative^[n - k] p).eval 1 = 0 by
        rw [this]
        exact (iterate_derivative_at_1_ne_zero ℚ n k h).symm
      refine span_induction ?_ ?_ ?_ ?_ m
      · simp only [Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff]
        rintro ⟨a, w⟩; simp only
        rw [iterate_derivative_at_1_eq_zero_of_lt ℚ n ((tsub_lt_tsub_iff_left_of_le h).mpr w)]
      · simp
      · intro x y _ _ hx hy; simp [hx, hy]
      · intro a x _ h; simp [h]
Cleared hypotheses: k, h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
n k : ℕ
h : k ≤ n + 1
zero : ∀ (h : 0 ≤ n + 1), LinearIndependent ℚ (M := ℚ[X]) fun (ν : Fin 0) ↦ bernsteinPolynomial ℚ n (↑ν : ℕ)
⊢ LinearIndependent ℚ (M := ℚ[X]) fun (ν : Fin k) ↦ bernsteinPolynomial ℚ n (↑ν : ℕ)
have succ : ∀ (k : ℕ) (ih : ∀ (h : k ≤ n + 1), LinearIndependent ℚ (M := ℚ[X]) fun (ν : Fin k) ↦ bernsteinPolynomial ℚ n (↑ν : ℕ))
  (h : k + 1 ≤ n + 1), LinearIndependent ℚ (M := ℚ[X]) fun (ν : Fin (k + 1)) ↦ bernsteinPolynomial ℚ n (↑ν : ℕ)
Tactic: induction k with
  | zero => apply linearIndependent_empty_type
  | succ k ih =>
    apply linearIndependent_finSucc'.mpr
    fconstructor
    · exact ih (le_of_lt h)
    · -- The actual work!
      -- We show that the (n-k)-th derivative at 1 doesn't vanish,
      -- but vanishes for everything in the span.
      clear ih
      simp only [add_le_add_iff_right] at h
      simp only [Fin.val_last, Fin.init_def]
      dsimp
      apply notMem_span_of_apply_notMem_span_image (@Polynomial.derivative ℚ _ ^ (n - k))
      -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to change `span_image` into `span_image _`
      simp only [not_exists, not_and, Submodule.mem_map, Submodule.span_image _]
      intro p m
      apply_fun Polynomial.eval (1 : ℚ)
      simp only [Module.End.pow_apply]
      -- The right-hand side is nonzero,
      -- so it will suffice to show the left-hand side is always zero.
      suffices (Polynomial.derivative^[n - k] p).eval 1 = 0 by
        rw [this]
        exact (iterate_derivative_at_1_ne_zero ℚ n k h).symm
      refine span_induction ?_ ?_ ?_ ?_ m
      · simp only [Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff]
        rintro ⟨a, w⟩; simp only
        rw [iterate_derivative_at_1_eq_zero_of_lt ℚ n ((tsub_lt_tsub_iff_left_of_le h).mpr w)]
      · simp
      · intro x y _ _ hx hy; simp [hx, hy]
      · intro a x _ h; simp [h]
Cleared hypotheses: k, h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
⊢ ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν = (X + HSub.hSub (α := R[X]) 1 X) ^ n
have rw : Eq.{u_1 + 1} (α := R[X]) (∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν)
  (∑ m ∈ Finset.range (n + 1), HPow.hPow (α := R[X]) X m * HSub.hSub (α := R[X]) 1 X ^ (n - m) * (↑(n.choose m) : R[X]))
Tactic: rw [add_pow]
-- 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
⊢ Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) x : MvPolynomial Bool R) (1 : MvPolynomial Bool R)
have rw : Eq.{u_1 + 1} (α := MvPolynomial Bool R)
  (Pi.single (M := fun (x : Bool) ↦ MvPolynomial Bool R) true 1 true : MvPolynomial Bool R) (1 : MvPolynomial Bool R)
Tactic: rw [pderiv_X]
-- 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
⊢ ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) ν (bernsteinPolynomial R n ν) = HSMul.hSMul (β := R[X]) n X
have pderiv_true_x : Eq (α := MvPolynomial Bool R) ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) x : MvPolynomial Bool R)
  (1 : MvPolynomial Bool R)
Tactic: have pderiv_true_x : pderiv true x = 1 := by rw [pderiv_X]; rfl
-- 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)
⊢ Eq (α := MvPolynomial Bool R)
    ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) y : MvPolynomial Bool R) (0 : MvPolynomial Bool R)
have rw : Eq.{u_1 + 1} (α := MvPolynomial Bool R)
  (Pi.single (M := fun (x : Bool) ↦ MvPolynomial Bool R) true 1 false : MvPolynomial Bool R) (0 : MvPolynomial Bool R)
Tactic: rw [pderiv_X]
-- 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)
⊢ ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) ν (bernsteinPolynomial R n ν) = HSMul.hSMul (β := R[X]) n X
have pderiv_true_y : Eq (α := MvPolynomial Bool R) ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) y : MvPolynomial Bool R)
  (0 : MvPolynomial Bool R)
Tactic: have pderiv_true_y : pderiv true y = 0 := by rw [pderiv_X]; rfl
-- 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]) ν (bernsteinPolynomial R n ν) = HSMul.hSMul (β := R[X]) n X
have trans : ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) ν (bernsteinPolynomial R n ν) =
  HMul.hMul (α := R[X]) (β := R[X])
    ((MvPolynomial.aeval e : (a : MvPolynomial Bool R) → R[X])
        ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) ((x + y) ^ n)) :
      R[X])
    X
Tactic: trans MvPolynomial.aeval e (pderiv true ((x + y) ^ n)) * X
-- 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]) ν (bernsteinPolynomial R n ν) =
    HMul.hMul (α := R[X]) (β := R[X])
      ((MvPolynomial.aeval e : (a : MvPolynomial Bool R) → R[X])
          ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) ((x + y) ^ n)) :
        R[X])
      X
⊢ ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) ν (bernsteinPolynomial R n ν) = HSMul.hSMul (β := R[X]) n X
have trans₁ : HMul.hMul (α := R[X]) (β := R[X])
    ((MvPolynomial.aeval e : (a : MvPolynomial Bool R) → R[X])
        ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) ((x + y) ^ n)) :
      R[X])
    X =
  HSMul.hSMul (β := R[X]) n X
Tactic: trans MvPolynomial.aeval e (pderiv true ((x + y) ^ n)) * X
-- 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) •
      ((↑(n.choose (k + 1)) : R[X]) * HPow.hPow (α := R[X]) X (k + 1) * HSub.hSub (α := R[X]) 1 X ^ (n - (k + 1))) =
    (↑(k + 1) : R[X]) * HPow.hPow (α := R[X]) X (k + 1 - 1) * HSub.hSub (α := R[X]) 1 X ^ (n - (k + 1)) *
        (↑(n.choose (k + 1)) : R[X]) *
      X
have succ : (↑(k + 1) : R[X]) *
    ((↑(n.choose (k + 1)) : R[X]) * (HPow.hPow (α := R[X]) X k * X) * HSub.hSub (α := R[X]) 1 X ^ (n - (k + 1))) =
  (↑(k + 1) : R[X]) * HPow.hPow (α := R[X]) X k * HSub.hSub (α := R[X]) 1 X ^ (n - (k + 1)) *
      (↑(n.choose (k + 1)) : R[X]) *
    X
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) : R[X]) *
      ((↑(n.choose (k + 1)) : R[X]) * (HPow.hPow (α := R[X]) X k * X) * HSub.hSub (α := R[X]) 1 X ^ (n - (k + 1))) =
    (↑(k + 1) : R[X]) * HPow.hPow (α := R[X]) X k * HSub.hSub (α := R[X]) 1 X ^ (n - (k + 1)) *
        (↑(n.choose (k + 1)) : R[X]) *
      X
have succ : HAdd.hAdd (α := R[X]) (↑k : R[X]) 1 *
    ((↑(n.choose (k + 1)) : R[X]) * (HPow.hPow (α := R[X]) X k * X) * HSub.hSub (α := R[X]) 1 X ^ (n - (k + 1))) =
  HAdd.hAdd (α := R[X]) (↑k : R[X]) 1 * HPow.hPow (α := R[X]) X k * HSub.hSub (α := R[X]) 1 X ^ (n - (k + 1)) *
      (↑(n.choose (k + 1)) : R[X]) *
    X
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]) ν (bernsteinPolynomial R n ν) =
    HMul.hMul (α := R[X]) (β := R[X])
      ((MvPolynomial.aeval e : (a : MvPolynomial Bool R) → R[X])
          ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) ((x + y) ^ n)) :
        R[X])
      X
have w : ∀ (k : ℕ),
  HSMul.hSMul (β := R[X]) k (bernsteinPolynomial R n k) =
    (↑k : R[X]) * HPow.hPow (α := R[X]) X (k - 1) * HSub.hSub (α := R[X]) 1 X ^ (n - k) * (↑(n.choose k) : R[X]) * X
Tactic: have w : ∀ k : ℕ, k • bernsteinPolynomial R n k =
        (k : R[X]) * Polynomial.X ^ (k - 1) * (1 - Polynomial.X) ^ (n - k) * (n.choose k : R[X]) *
          Polynomial.X := by
      rintro (_ | k)
      · simp
      · rw [bernsteinPolynomial]
        simp only [← natCast_mul, Nat.add_succ_sub_one, add_zero, pow_succ]
        push_cast
        ring
-- 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 (bernsteinPolynomial R n k) =
      (↑k : R[X]) * HPow.hPow (α := R[X]) X (k - 1) * HSub.hSub (α := R[X]) 1 X ^ (n - k) * (↑(n.choose k) : R[X]) * X
⊢ ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) ν (bernsteinPolynomial R n ν) =
    HMul.hMul (α := R[X]) (β := R[X])
      ((MvPolynomial.aeval e : (a : MvPolynomial Bool R) → R[X])
          ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) ((x + y) ^ n)) :
        R[X])
      X
have rw : Eq.{u_1 + 1} (α := R[X]) (∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) ν (bernsteinPolynomial R n ν))
  (∑ i ∈ Finset.range (n + 1),
    HMul.hMul (α := R[X]) (β := R[X])
      ((MvPolynomial.aeval e : (a : MvPolynomial Bool R) → R[X])
          ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R)
            (x ^ i * y ^ (n - i) * (↑(n.choose i) : MvPolynomial Bool R))) :
        R[X])
      X)
Tactic: rw [add_pow, 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 (bernsteinPolynomial R n k) =
      (↑k : R[X]) * HPow.hPow (α := R[X]) X (k - 1) * HSub.hSub (α := R[X]) 1 X ^ (n - k) * (↑(n.choose k) : R[X]) * X
⊢ Eq.{u_1 + 1} (α := R[X]) (∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) ν (bernsteinPolynomial R n ν))
    (∑ i ∈ Finset.range (n + 1),
      HMul.hMul (α := R[X]) (β := R[X])
        ((MvPolynomial.aeval e : (a : MvPolynomial Bool R) → R[X])
            ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R)
              (x ^ i * y ^ (n - i) * (↑(n.choose i) : MvPolynomial Bool R))) :
          R[X])
        X)
have refine : ∀ k ∈ Finset.range (n + 1),
  (↑k : R[X]) * HPow.hPow (α := R[X]) X (k - 1) * HSub.hSub (α := R[X]) 1 X ^ (n - k) * (↑(n.choose k) : R[X]) * X =
    HMul.hMul (α := R[X]) (β := R[X])
      ((MvPolynomial.aeval e : (a : MvPolynomial Bool R) → R[X])
          ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R)
            (x ^ k * y ^ (n - k) * (↑(n.choose k) : MvPolynomial Bool R))) :
        R[X])
      X
Tactic: refine Finset.sum_congr rfl fun k _ => (w k).trans ?_
-- 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
⊢ HMul.hMul (α := R[X]) (β := R[X])
      ((MvPolynomial.aeval e : (a : MvPolynomial Bool R) → R[X])
          ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) ((x + y) ^ n)) :
        R[X])
      X =
    HSMul.hSMul (β := R[X]) n X
have rw : HMul.hMul (α := R[X]) (β := R[X])
    ((MvPolynomial.aeval e : (a : MvPolynomial Bool R) → R[X])
        (n • (x + y) ^ (n - 1) • HAdd.hAdd (α := MvPolynomial Bool R) 1 0) :
      R[X])
    X =
  HSMul.hSMul (β := R[X]) n X
Tactic: rw [(pderiv true).leibniz_pow, (pderiv true).map_add, pderiv_true_x, pderiv_true_y]
-- 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
⊢ ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) (ν * (ν - 1)) (bernsteinPolynomial R n ν) =
    (n * (n - 1)) • HPow.hPow (α := R[X]) (β := ℕ) X 2
have pderiv_true_x : Eq (α := MvPolynomial Bool R) ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) x : MvPolynomial Bool R)
  (1 : MvPolynomial Bool R)
Tactic: have pderiv_true_x : pderiv true x = 1 := by rw [pderiv_X]; rfl
-- 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)
⊢ ∑ ν ∈ Finset.range (n + 1), HSMul.hSMul (β := R[X]) (ν * (ν - 1)) (bernsteinPolynomial R n ν) =
    (n * (n - 1)) • HPow.hPow (α := R[X]) (β := ℕ) X 2
have pderiv_true_y : Eq (α := MvPolynomial Bool R) ((pderiv true : (a : MvPolynomial Bool R) → MvPolynomial Bool R) y : MvPolynomial Bool R)
  (0 : MvPolynomial Bool R)
Tactic: have pderiv_true_y : pderiv true y = 0 := by rw [pderiv_X]; rfl