awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal R
f_1 : MvPolynomial σ R
hf : Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) f_1
f g : MvPolynomial σ R
h :
  Membership.mem (γ := Submodule (MvPolynomial σ R) (MvPolynomial σ R))
    (Submodule.span (MvPolynomial σ R) ((⇑C : (a : R) → MvPolynomial σ R) '' (↑I : Set R))) g
hg : ∀ (m : σ →₀ ℕ), coeff m g ∈ I
n : σ →₀ ℕ
⊢ ∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n, coeff x.1 f * coeff x.2 g ∈ I

Tactic:
exact I.sum_mem fun c _ => I.mul_mem_left (f.coeff c.fst) (hg c.snd)

Premises used: Submodule.sum_mem
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : ∀ (m : σ →₀ ℕ), coeff m f ∈ I
mpr :
  Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I)
    (∑ v ∈ f.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v f))
⊢ Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) f

Tactic:
rw [as_sum f]

Premises used: MvPolynomial.as_sum
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : ∀ (m : σ →₀ ℕ), coeff m f ∈ I
this :
  ∀ 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)
⊢ Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I)
    (∑ v ∈ f.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v f))

Tactic:
Submodule.sum_mem _ this

Premises used: Set.Mem, Submodule.sum_mem
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : ∀ (m : σ →₀ ℕ), coeff m f ∈ I
this :
  ∀ 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)
⊢ Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I)
    (∑ v ∈ f.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v f))

Tactic:
exact Submodule.sum_mem _ this

Premises used: Submodule.sum_mem
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : ∀ (m : σ →₀ ℕ), coeff m f ∈ I
mpr :
  ∀ 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)
⊢ Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I)
    (∑ v ∈ f.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v f))

Tactic:
suffices ∀ m ∈ f.support, monomial m (coeff m f) ∈ (Ideal.map C I : Ideal (MvPolynomial σ R)) by
      exact Submodule.sum_mem _ this
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : ∀ (m : σ →₀ ℕ), coeff m f ∈ I
m : σ →₀ ℕ
mpr :
  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)
⊢ 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)

Tactic:
_
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
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))
⊢ 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)

Tactic:
rw [← mul_one (coeff m f), ← C_mul_monomial]

Premises used: MvPolynomial.C_mul_monomial, MvPolynomial.coeff, mul_one
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
this :
  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)
⊢ 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:
Ideal.mul_mem_right _ _ this

Premises used: Set.Mem, Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
this :
  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)
⊢ 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:
exact Ideal.mul_mem_right _ _ this

Premises used: Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
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)
⊢ 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:
suffices C (coeff m f) ∈ (Ideal.map C I : Ideal (MvPolynomial σ R)) by
      exact Ideal.mul_mem_right _ _ this
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
mpr : coeff m f ∈ I
⊢ 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:
apply Ideal.mem_map_of_mem _

Premises used: Ideal.mem_map_of_mem
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
⊢ coeff m f ∈ I

Tactic:
hf m
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
⊢ coeff m f ∈ I

Tactic:
exact hf m
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
mpr mpr₁ :
  (∀ (m : σ →₀ ℕ), coeff m f ∈ I) →
    Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) f
⊢ 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

Premises used: Ideal.mem_map_of_mem, MvPolynomial.coeff_C, MvPolynomial.C_mul_monomial, MvPolynomial.as_sum, smul_eq_mul, MvPolynomial.coeff_mul
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
S : Type u_1
σ : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
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
⊢ Eq (α := Ideal (MvPolynomial σ R)) (RingHom.ker (F := MvPolynomial σ R →+* MvPolynomial σ S) (map f))
    (Ideal.map (F := R →+* MvPolynomial σ R) C (RingHom.ker f))

Tactic:
ext
-- Module: Mathlib.RingTheory.Polynomial.Basic
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) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) x)) (coeff m 0)) ↔
    ∀ (m : σ →₀ ℕ), Membership.mem (γ := Ideal R) (RingHom.ker f) (coeff m x)
⊢ 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:
rw [MvPolynomial.mem_map_C_iff, RingHom.mem_ker, MvPolynomial.ext_iff]

Premises used: RingHom.mem_ker, MvPolynomial.ext_iff, MvPolynomial.mem_map_C_iff
-- Module: Mathlib.RingTheory.Polynomial.Basic
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)
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)
⊢ (∀ (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:
simp_rw [coeff_map, coeff_zero, RingHom.mem_ker]

Premises used: RingHom.mem_ker, MvPolynomial.coeff_map, MvPolynomial.coeff_zero
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
S₁ : Type u_2
S₂ : Type u_3
σ : Type u_4
inst_1 : CommRing S₁
inst_2 : CommRing S₂
inst_3 : Algebra R S₁
inst_4 : Algebra R S₂
f : S₁ →ₐ[R] S₂
⊢ Eq (α := Ideal (MvPolynomial σ S₁)) (RingHom.ker (F := MvPolynomial σ S₁ →ₐ[R] MvPolynomial σ S₂) (mapAlgHom f))
    (Ideal.map (F := S₁ →+* MvPolynomial σ S₁) C (RingHom.ker f))

Tactic:
MvPolynomial.ker_map (f.toRingHom : S₁ →+* S₂)

Premises used: MvPolynomial.ker_map, AddMonoidAlgebra.mapRingHom, AddMonoidAlgebra.mapAlgHom, MvPolynomial.mapAlgHom, MonoidHomClass.toMonoidHom, AlgHom.toRingHom, RingHomClass.toRingHom, Ideal.comap, MvPolynomial.map, RingHom.ker
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
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
⊢ bernsteinPolynomial ℤ 3 2 = 3 * HPow.hPow (α := ℤ[X]) (β := ℕ) X 2 - 3 * HPow.hPow (α := ℤ[X]) (β := ℕ) X 3

Tactic:
norm_num [bernsteinPolynomial, choose]

Premises used: Nat.choose, bernsteinPolynomial
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
⊢ 3 * HPow.hPow (α := ℤ[X]) (β := ℕ) X 2 * HSub.hSub (α := ℤ[X]) 1 X =
    3 * HPow.hPow (α := ℤ[X]) (β := ℕ) X 2 - 3 * HPow.hPow (α := ℤ[X]) (β := ℕ) X 3

Tactic:
ring
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
h : n < ν
⊢ Eq (α := R[X]) (bernsteinPolynomial R n ν) 0

Tactic:
simp [bernsteinPolynomial, Nat.choose_eq_zero_of_lt h]

Premises used: bernsteinPolynomial, Nat.choose_eq_zero_of_lt
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
n ν : ℕ
⊢ Polynomial.map f (bernsteinPolynomial R n ν) = bernsteinPolynomial S n ν

Tactic:
simp [bernsteinPolynomial]

Premises used: bernsteinPolynomial
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
h : ν ≤ n
⊢ Polynomial.comp (bernsteinPolynomial R n ν) (HSub.hSub (α := R[X]) 1 X) = bernsteinPolynomial R n (n - ν)

Tactic:
simp [bernsteinPolynomial, h, tsub_tsub_assoc, mul_right_comm]

Premises used: bernsteinPolynomial, tsub_tsub_assoc, mul_right_comm
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
h : ν ≤ n
⊢ bernsteinPolynomial R n ν = Polynomial.comp (bernsteinPolynomial R n (n - ν)) (HSub.hSub (α := R[X]) 1 X)

Tactic:
simp [← flip _ _ _ h, Polynomial.comp_assoc]

Premises used: Polynomial.comp_assoc, bernsteinPolynomial.flip
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
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
neg :
  ∀ (h : ¬ν = 0),
    Polynomial.eval 0 ((↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (n - ν)) = 0
⊢ 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

Tactic:
split_ifs with h
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
h : ν = 0
pos :
  Polynomial.eval 0
      ((↑(n.choose 0) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 0 * HSub.hSub (α := R[X]) 1 X ^ (n - 0)) =
    1
⊢ Polynomial.eval 0 ((↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (n - ν)) = 1

Tactic:
subst h
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
⊢ Polynomial.eval 0
      ((↑(n.choose 0) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 0 * HSub.hSub (α := R[X]) 1 X ^ (n - 0)) =
    1

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
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 - ν)) = 0

Tactic:
simp [zero_pow h]

Premises used: zero_pow
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
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
neg :
  ∀ (h : ¬ν = 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 - ν)) =
    if ν = n then 1 else 0

Tactic:
split_ifs with h
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
h : ν = n
pos : Polynomial.eval 1 ((↑(ν.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (ν - ν)) = 1
⊢ Polynomial.eval 1 ((↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (n - ν)) = 1

Tactic:
subst h
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
ν : ℕ
⊢ Polynomial.eval 1 ((↑(ν.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (ν - ν)) = 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
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
neg₁ :
  ∀ (hnν : 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

Tactic:
obtain hνn | hnν := Ne.lt_or_gt h

Premises used: Ne.lt_or_gt
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
h : ¬ν = n
hνn : ν < n
⊢ Polynomial.eval 1 ((↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (n - ν)) = 0

Tactic:
simp [zero_pow <| Nat.sub_ne_zero_of_lt hνn]

Premises used: Nat.sub_ne_zero_of_lt, zero_pow
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
h : ¬ν = n
hnν : n < ν
⊢ Polynomial.eval 1 ((↑(n.choose ν) : R[X]) * HPow.hPow (α := R[X]) X ν * HSub.hSub (α := R[X]) 1 X ^ (n - ν)) = 0

Tactic:
simp [Nat.choose_eq_zero_of_lt hnν]

Premises used: Nat.choose_eq_zero_of_lt
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
this :
  (↑((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)))
⊢ (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))

Tactic:
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]

Premises used: algebraMap.coe_one, Polynomial.derivative_mul, Polynomial.derivative_X, MulZeroClass.zero_mul, sub_eq_add_neg, map_add, zero_add, bernsteinPolynomial, Nat.cast_add, map_natCast, Polynomial.derivative_pow, Polynomial.derivative_sub, Nat.sub_zero, mul_one, Polynomial.derivative_natCast, Nat.cast_one, Nat.succ_sub_succ_eq_sub, Polynomial.derivative_one, zero_sub, mul_neg
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
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)))
⊢ (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))

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]
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
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)))
| (↑(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:
rw [mul_sub]

Premises used: mul_sub
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n ν : ℕ
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)))
⊢ (↑((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:
conv_rhs => rw [mul_sub]

Premises used: mul_sub
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
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)))

Tactic:
congr (congr_arg Sub.sub ?_) ?_

Premises used: congr_arg, congr, Sub.sub