awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : ∀ (m : σ →₀ ℕ), coeff m f ∈ I
m : σ →₀ ℕ
h : m ∈ f.support
⊢ Membership.mem (α := MvPolynomial σ R) (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I)
    ((monomial m : (a : R) → MvPolynomial σ R) (coeff m f) : MvPolynomial σ R)
have mpr : Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I)
  (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) (coeff m f) : MvPolynomial σ R)
    ((monomial m : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R))
Tactic: rw [← mul_one (coeff m f), ← C_mul_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : ∀ (m : σ →₀ ℕ), coeff m f ∈ I
m : σ →₀ ℕ
h : m ∈ f.support
⊢ Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I)
    (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) (coeff m f) : MvPolynomial σ R)
      ((monomial m : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R))
have mpr : Membership.mem (α := MvPolynomial σ R) (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I)
  ((C : (a : R) → MvPolynomial σ R) (coeff m f) : MvPolynomial σ R)
Tactic: suffices C (coeff m f) ∈ (Ideal.map C I : Ideal (MvPolynomial σ R)) by
      exact Ideal.mul_mem_right _ _ this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : ∀ (m : σ →₀ ℕ), coeff m f ∈ I
m : σ →₀ ℕ
h : m ∈ f.support
⊢ Membership.mem (α := MvPolynomial σ R) (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I)
    ((C : (a : R) → MvPolynomial σ R) (coeff m f) : MvPolynomial σ R)
have mpr : coeff m f ∈ I
Tactic: apply Ideal.mem_map_of_mem _
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal R
f : MvPolynomial σ R
⊢ Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) f ↔
    ∀ (m : σ →₀ ℕ), coeff m f ∈ I
have mp : Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) f →
  ∀ (m : σ →₀ ℕ), coeff m f ∈ I
Tactic: classical
  constructor
  · intro hf
    refine Submodule.span_induction ?_ ?_ ?_ ?_ hf
    · intro f hf n
      obtain ⟨x, hx⟩ := (Set.mem_image _ _ _).mp hf
      rw [← hx.right, coeff_C]
      by_cases h : n = 0
      · simpa [h] using hx.left
      · simp [Ne.symm h]
    · simp
    · exact fun f g _ _ hf hg n => by simp [I.add_mem (hf n) (hg n)]
    · refine fun f g _ hg n => ?_
      rw [smul_eq_mul, coeff_mul]
      exact I.sum_mem fun c _ => I.mul_mem_left (f.coeff c.fst) (hg c.snd)
  · intro hf
    rw [as_sum f]
    suffices ∀ m ∈ f.support, monomial m (coeff m f) ∈ (Ideal.map C I : Ideal (MvPolynomial σ R)) by
      exact Submodule.sum_mem _ this
    intro m _
    rw [← mul_one (coeff m f), ← C_mul_monomial]
    suffices C (coeff m f) ∈ (Ideal.map C I : Ideal (MvPolynomial σ R)) by
      exact Ideal.mul_mem_right _ _ this
    apply Ideal.mem_map_of_mem _
    exact hf m
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal R
f : MvPolynomial σ R
mp :
  Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) f →
    ∀ (m : σ →₀ ℕ), coeff m f ∈ I
⊢ Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) f ↔
    ∀ (m : σ →₀ ℕ), coeff m f ∈ I
have mpr : (∀ (m : σ →₀ ℕ), coeff m f ∈ I) →
  Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) f
Tactic: classical
  constructor
  · intro hf
    refine Submodule.span_induction ?_ ?_ ?_ ?_ hf
    · intro f hf n
      obtain ⟨x, hx⟩ := (Set.mem_image _ _ _).mp hf
      rw [← hx.right, coeff_C]
      by_cases h : n = 0
      · simpa [h] using hx.left
      · simp [Ne.symm h]
    · simp
    · exact fun f g _ _ hf hg n => by simp [I.add_mem (hf n) (hg n)]
    · refine fun f g _ hg n => ?_
      rw [smul_eq_mul, coeff_mul]
      exact I.sum_mem fun c _ => I.mul_mem_left (f.coeff c.fst) (hg c.snd)
  · intro hf
    rw [as_sum f]
    suffices ∀ m ∈ f.support, monomial m (coeff m f) ∈ (Ideal.map C I : Ideal (MvPolynomial σ R)) by
      exact Submodule.sum_mem _ this
    intro m _
    rw [← mul_one (coeff m f), ← C_mul_monomial]
    suffices C (coeff m f) ∈ (Ideal.map C I : Ideal (MvPolynomial σ R)) by
      exact Ideal.mul_mem_right _ _ this
    apply Ideal.mem_map_of_mem _
    exact hf m
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
S : Type u_1
σ : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
⊢ Eq (α := Ideal (MvPolynomial σ R)) (RingHom.ker (F := MvPolynomial σ R →+* MvPolynomial σ S) (map f))
    (Ideal.map (F := R →+* MvPolynomial σ R) C (RingHom.ker f))
have h : ∀ (x : MvPolynomial σ R),
  Membership.mem (γ := Ideal (MvPolynomial σ R)) (RingHom.ker (F := MvPolynomial σ R →+* MvPolynomial σ S) (map f)) x ↔
    Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C (RingHom.ker f)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
S : Type u_1
σ : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
x : MvPolynomial σ R
⊢ Membership.mem (γ := Ideal (MvPolynomial σ R)) (RingHom.ker (F := MvPolynomial σ R →+* MvPolynomial σ S) (map f)) x ↔
    Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C (RingHom.ker f)) x
have h : (∀ (m : σ →₀ ℕ), Eq.{u_1 + 1} (α := S) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) x)) (coeff m 0)) ↔
  ∀ (m : σ →₀ ℕ), Membership.mem (γ := Ideal R) (RingHom.ker f) (coeff m x)
Tactic: rw [MvPolynomial.mem_map_C_iff, RingHom.mem_ker, MvPolynomial.ext_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
S : Type u_1
σ : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
x : MvPolynomial σ R
⊢ (∀ (m : σ →₀ ℕ),
      Eq.{u_1 + 1} (α := S) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) x)) (coeff m 0)) ↔
    ∀ (m : σ →₀ ℕ), Membership.mem (γ := Ideal R) (RingHom.ker f) (coeff m x)
have h : (∀ (m : σ →₀ ℕ), Eq.{u_1 + 1} (α := S) ((f : (a : R) → S) (coeff m x) : S) (coeff m 0 : S)) ↔
  ∀ (m : σ →₀ ℕ), Membership.mem (γ := Ideal R) (RingHom.ker f) (coeff m x)
Tactic: simp_rw [coeff_map, coeff_zero, RingHom.mem_ker]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
S : Type u_1
σ : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
x : MvPolynomial σ R
h :
  (∀ (m : σ →₀ ℕ), Eq.{u_1 + 1} (α := S) ((f : (a : R) → S) (coeff m x) : S) (coeff m 0 : S)) ↔
    ∀ (m : σ →₀ ℕ), Membership.mem (γ := Ideal R) (RingHom.ker f) (coeff m x)
⊢ (∀ (m : σ →₀ ℕ),
      Eq.{u_1 + 1} (α := S) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) x)) (coeff m 0)) ↔
    ∀ (m : σ →₀ ℕ), Membership.mem (γ := Ideal R) (RingHom.ker f) (coeff m x)
have h₁ : (∀ (m : σ →₀ ℕ), Eq.{u_1 + 1} (α := S) ((f : (a : R) → S) (coeff m x) : S) (0 : S)) ↔
  ∀ (m : σ →₀ ℕ), Membership.mem (γ := Ideal R) (RingHom.ker f) (coeff m x)
Tactic: simp_rw [coeff_map, coeff_zero, RingHom.mem_ker]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ bernsteinPolynomial ℤ 3 2 = 3 * HPow.hPow (α := ℤ[X]) (β := ℕ) X 2 - 3 * HPow.hPow (α := ℤ[X]) (β := ℕ) X 3
have norm_num : 3 * HPow.hPow (α := ℤ[X]) (β := ℕ) X 2 * HSub.hSub (α := ℤ[X]) 1 X =
  3 * HPow.hPow (α := ℤ[X]) (β := ℕ) X 2 - 3 * HPow.hPow (α := ℤ[X]) (β := ℕ) X 3
Tactic: norm_num [bernsteinPolynomial, choose]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
⊢ Polynomial.eval 0 ((↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (n - ν)) =
    if ν = 0 then 1 else 0
have pos : ∀ (h : ν = 0),
  Polynomial.eval 0 ((↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (n - ν)) = 1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
pos :
  ∀ (h : ν = 0),
    Polynomial.eval 0 ((↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (n - ν)) = 1
⊢ Polynomial.eval 0 ((↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (n - ν)) =
    if ν = 0 then 1 else 0
have neg : ∀ (h : ¬ν = 0),
  Polynomial.eval 0 ((↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (n - ν)) = 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
h : ν = 0
⊢ Polynomial.eval 0 ((↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (n - ν)) = 1
have pos : Polynomial.eval 0 ((↑(n.choose 0) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 0 * HSub.hSub (α := R[X]) 1 X ^ (n - 0)) =
  1
Tactic: subst h
Cleared hypotheses: ν, h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
⊢ Polynomial.eval 1 ((↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (n - ν)) =
    if ν = n then 1 else 0
have pos : ∀ (h : ν = n),
  Polynomial.eval 1 ((↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (n - ν)) = 1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
pos :
  ∀ (h : ν = n),
    Polynomial.eval 1 ((↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (n - ν)) = 1
⊢ Polynomial.eval 1 ((↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (n - ν)) =
    if ν = n then 1 else 0
have neg : ∀ (h : ¬ν = n),
  Polynomial.eval 1 ((↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (n - ν)) = 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
h : ν = n
⊢ Polynomial.eval 1 ((↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (n - ν)) = 1
have pos : Polynomial.eval 1 ((↑(ν.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (ν - ν)) = 1
Tactic: subst h
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
h : ¬ν = n
⊢ Polynomial.eval 1 ((↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (n - ν)) = 0
have neg : ∀ (hνn : ν < n),
  Polynomial.eval 1 ((↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (n - ν)) = 0
Tactic: obtain hνn | hnν := Ne.lt_or_gt h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
h : ¬ν = n
neg :
  ∀ (hνn : ν < n),
    Polynomial.eval 1 ((↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (n - ν)) = 0
⊢ Polynomial.eval 1 ((↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (n - ν)) = 0
have neg₁ : ∀ (hnν : n < ν),
  Polynomial.eval 1 ((↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (n - ν)) = 0
Tactic: obtain hνn | hnν := Ne.lt_or_gt h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
⊢ (Polynomial.derivative : (a : R[X]) → R[X])
      ((↑((n + 1).choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1) *
        HSub.hSub (α := R[X]) 1 X ^ (n + 1 - (ν + 1))) =
    HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 *
      HSub.hSub (α := R[X]) (bernsteinPolynomial R n ν) (bernsteinPolynomial R n (ν + 1))
have suffices : (↑((n + 1).choose (ν + 1)) : R[X]) * ((↑(ν + 1) : R[X]) * HPow.hPow (α := R[X]) X ν) *
      HSub.hSub (α := R[X]) 1 X ^ (n - ν) -
    (↑((n + 1).choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1) *
      ((↑(n - ν) : R[X]) * HSub.hSub (α := R[X]) 1 X ^ (n - ν - 1)) =
  (↑(n + 1) : R[X]) *
    ((↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (n - ν) -
      (↑(n.choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1) * HSub.hSub (α := R[X]) 1 X ^ (n - (ν + 1)))
Tactic: suffices ((n + 1).choose (ν + 1) : R[X]) * ((↑(ν + 1 : ℕ) : R[X]) * X ^ ν) * (1 - X) ^ (n - ν) -
      ((n + 1).choose (ν + 1) : R[X]) * X ^ (ν + 1) * ((↑(n - ν) : R[X]) * (1 - X) ^ (n - ν - 1)) =
      (↑(n + 1) : R[X]) * ((n.choose ν : R[X]) * X ^ ν * (1 - X) ^ (n - ν) -
        (n.choose (ν + 1) : R[X]) * X ^ (ν + 1) * (1 - X) ^ (n - (ν + 1))) by
    simpa [Polynomial.derivative_pow, ← sub_eq_add_neg, Nat.succ_sub_succ_eq_sub,
      Polynomial.derivative_mul, Polynomial.derivative_natCast, zero_mul,
      Nat.cast_add, algebraMap.coe_one, Polynomial.derivative_X, mul_one, zero_add,
      Polynomial.derivative_sub, Polynomial.derivative_one, zero_sub, mul_neg, Nat.sub_zero,
      bernsteinPolynomial, map_add, map_natCast, Nat.cast_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
| (↑(n + 1) : R[X]) *
    ((↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (n - ν) -
      (↑(n.choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1) * HSub.hSub (α := R[X]) 1 X ^ (n - (ν + 1)))
have rw : (↑(n + 1) : R[X]) * ((↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (n - ν)) -
  (↑(n + 1) : R[X]) *
    ((↑(n.choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1) * HSub.hSub (α := R[X]) 1 X ^ (n - (ν + 1)))
Tactic: rw [mul_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
⊢ (↑((n + 1).choose (ν + 1)) : R[X]) * ((↑(ν + 1) : R[X]) * HPow.hPow (α := R[X]) X ν) *
        HSub.hSub (α := R[X]) 1 X ^ (n - ν) -
      (↑((n + 1).choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1) *
        ((↑(n - ν) : R[X]) * HSub.hSub (α := R[X]) 1 X ^ (n - ν - 1)) =
    (↑(n + 1) : R[X]) *
      ((↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (n - ν) -
        (↑(n.choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1) * HSub.hSub (α := R[X]) 1 X ^ (n - (ν + 1)))
have conv_rhs : (↑((n + 1).choose (ν + 1)) : R[X]) * ((↑(ν + 1) : R[X]) * HPow.hPow (α := R[X]) X ν) *
      HSub.hSub (α := R[X]) 1 X ^ (n - ν) -
    (↑((n + 1).choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1) *
      ((↑(n - ν) : R[X]) * HSub.hSub (α := R[X]) 1 X ^ (n - ν - 1)) =
  (↑(n + 1) : R[X]) * ((↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (n - ν)) -
    (↑(n + 1) : R[X]) *
      ((↑(n.choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1) * HSub.hSub (α := R[X]) 1 X ^ (n - (ν + 1)))
Tactic: conv_rhs => rw [mul_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
⊢ (↑((n + 1).choose (ν + 1)) : R[X]) * ((↑(ν + 1) : R[X]) * HPow.hPow (α := R[X]) X ν) *
        HSub.hSub (α := R[X]) 1 X ^ (n - ν) -
      (↑((n + 1).choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1) *
        ((↑(n - ν) : R[X]) * HSub.hSub (α := R[X]) 1 X ^ (n - ν - 1)) =
    (↑(n + 1) : R[X]) * ((↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (n - ν)) -
      (↑(n + 1) : R[X]) *
        ((↑(n.choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1) * HSub.hSub (α := R[X]) 1 X ^ (n - (ν + 1)))
have refine_1 : (↑((n + 1).choose (ν + 1)) : R[X]) * ((↑(ν + 1) : R[X]) * HPow.hPow (α := R[X]) X ν) *
    HSub.hSub (α := R[X]) 1 X ^ (n - ν) =
  (↑(n + 1) : R[X]) * ((↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (n - ν))
Tactic: refine congr (congr_arg Sub.sub ?_) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
refine_1 :
  (↑((n + 1).choose (ν + 1)) : R[X]) * ((↑(ν + 1) : R[X]) * HPow.hPow (α := R[X]) X ν) *
      HSub.hSub (α := R[X]) 1 X ^ (n - ν) =
    (↑(n + 1) : R[X]) * ((↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (n - ν))
⊢ (↑((n + 1).choose (ν + 1)) : R[X]) * ((↑(ν + 1) : R[X]) * HPow.hPow (α := R[X]) X ν) *
        HSub.hSub (α := R[X]) 1 X ^ (n - ν) -
      (↑((n + 1).choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1) *
        ((↑(n - ν) : R[X]) * HSub.hSub (α := R[X]) 1 X ^ (n - ν - 1)) =
    (↑(n + 1) : R[X]) * ((↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (n - ν)) -
      (↑(n + 1) : R[X]) *
        ((↑(n.choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1) * HSub.hSub (α := R[X]) 1 X ^ (n - (ν + 1)))
have refine_2 : (↑((n + 1).choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1) *
    ((↑(n - ν) : R[X]) * HSub.hSub (α := R[X]) 1 X ^ (n - ν - 1)) =
  (↑(n + 1) : R[X]) *
    ((↑(n.choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1) * HSub.hSub (α := R[X]) 1 X ^ (n - (ν + 1)))
Tactic: refine congr (congr_arg Sub.sub ?_) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
⊢ (↑((n + 1).choose (ν + 1)) : R[X]) * ((↑(ν + 1) : R[X]) * HPow.hPow (α := R[X]) X ν) *
      HSub.hSub (α := R[X]) 1 X ^ (n - ν) =
    (↑(n + 1) : R[X]) * ((↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (n - ν))
have refine_1 : HMul.hMul (α := R[X]) (↑((n + 1).choose (ν + 1)) : R[X]) (↑(ν + 1) : R[X]) * HPow.hPow (α := R[X]) X ν *
    HSub.hSub (α := R[X]) 1 X ^ (n - ν) =
  HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν *
    HSub.hSub (α := R[X]) 1 X ^ (n - ν)
Tactic: simp only [← mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
⊢ HMul.hMul (α := R[X]) (↑((n + 1).choose (ν + 1)) : R[X]) (↑(ν + 1) : R[X]) * HPow.hPow (α := R[X]) X ν *
      HSub.hSub (α := R[X]) 1 X ^ (n - ν) =
    HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν *
      HSub.hSub (α := R[X]) 1 X ^ (n - ν)
have apply : HMul.hMul (α := R[X]) (↑((n + 1).choose (ν + 1)) : R[X]) (↑(ν + 1) : R[X]) =
  HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (↑(n.choose ν) : R[X])
Tactic: apply congr (congr_arg (· * ·) (congr (congr_arg (· * ·) _) rfl)) rfl
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
⊢ (↑((n + 1).choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1) *
      ((↑(n - ν) : R[X]) * HSub.hSub (α := R[X]) 1 X ^ (n - ν - 1)) =
    (↑(n + 1) : R[X]) *
      ((↑(n.choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1) * HSub.hSub (α := R[X]) 1 X ^ (n - (ν + 1)))
have refine_2 : (↑((n + 1).choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1) * (↑(n - ν) : R[X]) *
    HSub.hSub (α := R[X]) 1 X ^ (n - (ν + 1)) =
  (↑(n + 1) : R[X]) * ((↑(n.choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1)) *
    HSub.hSub (α := R[X]) 1 X ^ (n - (ν + 1))
Tactic: rw [← tsub_add_eq_tsub_tsub, ← mul_assoc, ← mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
⊢ (↑((n + 1).choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1) * (↑(n - ν) : R[X]) *
      HSub.hSub (α := R[X]) 1 X ^ (n - (ν + 1)) =
    (↑(n + 1) : R[X]) * ((↑(n.choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1)) *
      HSub.hSub (α := R[X]) 1 X ^ (n - (ν + 1))
have refine_2 : (↑((n + 1).choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1) * (↑(n - ν) : R[X]) =
  (↑(n + 1) : R[X]) * ((↑(n.choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
⊢ (↑((n + 1).choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1) * (↑(n - ν) : R[X]) =
    (↑(n + 1) : R[X]) * ((↑(n.choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1))
have refine_2 : HMul.hMul (α := R[X]) (↑(n - ν) : R[X]) (↑((n + 1).choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1) =
  HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (↑(n.choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1)
Tactic: rw [mul_comm, ← mul_assoc, ← mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
⊢ HMul.hMul (α := R[X]) (↑(n - ν) : R[X]) (↑((n + 1).choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1) =
    HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (↑(n.choose (ν + 1)) : R[X]) * HPow.hPow (α := R[X]) X (ν + 1)
have refine_2 : HMul.hMul (α := R[X]) (↑(n - ν) : R[X]) (↑((n + 1).choose (ν + 1)) : R[X]) =
  HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (↑(n.choose (ν + 1)) : R[X])
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
⊢ HMul.hMul (α := R[X]) (↑(n - ν) : R[X]) (↑((n + 1).choose (ν + 1)) : R[X]) =
    HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (↑(n.choose (ν + 1)) : R[X])
have refine_2 : Eq.{u_1 + 1} (α := R[X]) (↑((n - ν) * (n + 1).choose (ν + 1)) : R[X]) (↑((n + 1) * n.choose (ν + 1)) : R[X])
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
⊢ Eq.{u_1 + 1} (α := R[X]) (↑((n - ν) * (n + 1).choose (ν + 1)) : R[X]) (↑((n + 1) * n.choose (ν + 1)) : R[X])
have refine_2 : (n - ν) * (n + 1).choose (ν + 1) = (n + 1) * n.choose (ν + 1)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
⊢ (n - ν) * (n + 1).choose (ν + 1) = (n + 1) * n.choose (ν + 1)
have h : (n - ν) * (n + 1).choose (ν + 1) = (n + 1).choose (ν + 1) * (n + 1 - (ν + 1))
Tactic: convert! (Nat.choose_mul_succ_eq n (ν + 1)).symm using 1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
h : (n - ν) * (n + 1).choose (ν + 1) = (n + 1).choose (ν + 1) * (n + 1 - (ν + 1))
⊢ (n - ν) * (n + 1).choose (ν + 1) = (n + 1) * n.choose (ν + 1)
have h₁ : (n + 1) * n.choose (ν + 1) = n.choose (ν + 1) * (n + 1)
Tactic: convert! (Nat.choose_mul_succ_eq n (ν + 1)).symm using 1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
⊢ (n - ν) * (n + 1).choose (ν + 1) = (n + 1).choose (ν + 1) * (n + 1 - (ν + 1))
have h : n + 1 - (ν + 1) = n - ν
Tactic: convert! mul_comm _ _ using 2
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
⊢ (Polynomial.derivative : (a : R[X]) → R[X]) (bernsteinPolynomial R n (ν + 1)) =
    (↑n : R[X]) * HSub.hSub (α := R[X]) (bernsteinPolynomial R (n - 1) ν) (bernsteinPolynomial R (n - 1) (ν + 1))
have zero : (Polynomial.derivative : (a : R[X]) → R[X]) (bernsteinPolynomial R 0 (ν + 1)) =
  (↑0 : R[X]) *
    HSub.hSub (α := R[X]) (bernsteinPolynomial R (HSub.hSub (α := ℕ) 0 1) ν)
      (bernsteinPolynomial R (HSub.hSub (α := ℕ) 0 1) (ν + 1))
Tactic: cases n
Cleared hypotheses: n