awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
r : R
⊢ Eq.{u_1 + 1} (α := R[X]) (eraseLead ((C : (a : R) → R[X]) r)) 0

Tactic:
eraseLead_monomial _ _

Premises used: Polynomial.eraseLead_monomial
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := R[X]) (eraseLead X) 0

Tactic:
eraseLead_monomial _ _

Premises used: Polynomial.eraseLead_monomial, Polynomial.X
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
rw : Eq.{u_1 + 1} (α := R[X]) (eraseLead ((monomial n : (a : R) → R[X]) 1)) 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := R[X]) 0 0
⊢ (HPow.hPow (α := R[X]) X n).eraseLead = 0

Tactic:
rw [X_pow_eq_monomial, eraseLead_monomial]

Premises used: Polynomial.eraseLead_monomial, Polynomial.X_pow_eq_monomial
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
r : R
n : ℕ
rw : Eq.{u_1 + 1} (α := R[X]) (eraseLead ((monomial n : (a : R) → R[X]) r)) 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := R[X]) 0 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)).eraseLead = 0

Tactic:
rw [C_mul_X_pow_eq_monomial, eraseLead_monomial]

Premises used: Polynomial.eraseLead_monomial, Polynomial.C_mul_X_pow_eq_monomial
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
r : R
⊢ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X).eraseLead = 0

Tactic:
simpa using eraseLead_C_mul_X_pow _ 1

Premises used: Polynomial.eraseLead_C_mul_X_pow, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
pq : q.degree < p.degree
a : ∀ (n : ℕ), (p + q).eraseLead.coeff n = (p.eraseLead + q).coeff n
⊢ (p + q).eraseLead = p.eraseLead + q

Tactic:
ext n
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
pos : ∀ (nd : n = p.natDegree), (p + q).eraseLead.coeff n = (p.eraseLead + q).coeff n
neg : ∀ (nd : ¬n = p.natDegree), (p + q).eraseLead.coeff n = (p.eraseLead + q).coeff n
⊢ (p + q).eraseLead.coeff n = (p.eraseLead + q).coeff n

Tactic:
by_cases nd : n = p.natDegree

Premises used: Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
nd : n = p.natDegree
pos : 0 = (p.eraseLead + q).coeff p.natDegree
⊢ (p + q).eraseLead.coeff n = (p.eraseLead + q).coeff n

Tactic:
rw [nd, eraseLead_coeff, if_pos (natDegree_add_eq_left_of_degree_lt pq).symm]

Premises used: Polynomial.eraseLead_coeff, Polynomial.natDegree_add_eq_left_of_degree_lt, if_pos, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
nd : n = p.natDegree
⊢ 0 = (p.eraseLead + q).coeff p.natDegree

Tactic:
simpa using (coeff_eq_zero_of_degree_lt (lt_of_lt_of_le pq degree_le_natDegree)).symm

Premises used: Polynomial.degree_le_natDegree, Eq.symm, lt_of_lt_of_le, Polynomial.coeff_eq_zero_of_degree_lt
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
nd : ¬n = p.natDegree
neg : ¬n = (p + q).natDegree
⊢ (p + q).eraseLead.coeff n = (p.eraseLead + q).coeff n

Tactic:
rw [eraseLead_coeff, coeff_add, coeff_add, eraseLead_coeff, if_neg, if_neg nd]

Premises used: Polynomial.eraseLead_coeff, Polynomial.coeff_add, if_neg
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
pq : q.degree < p.degree
nd : ¬(p + q).natDegree = p.natDegree
⊢ False

Tactic:
nd (natDegree_add_eq_left_of_degree_lt pq)

Premises used: Polynomial.natDegree_add_eq_left_of_degree_lt
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
pq : q.degree < p.degree
nd : ¬(p + q).natDegree = p.natDegree
⊢ False

Tactic:
exact nd (natDegree_add_eq_left_of_degree_lt pq)

Premises used: Polynomial.natDegree_add_eq_left_of_degree_lt
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
pq : q.natDegree < p.natDegree
⊢ (p + q).eraseLead = p.eraseLead + q

Tactic:
eraseLead_add_of_degree_lt_left (degree_lt_degree pq)

Premises used: Polynomial.eraseLead_add_of_degree_lt_left, Polynomial.degree_lt_degree
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
pq : p.degree < q.degree
a : ∀ (n : ℕ), (p + q).eraseLead.coeff n = (p + q.eraseLead).coeff n
⊢ (p + q).eraseLead = p + q.eraseLead

Tactic:
ext n
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
pos : ∀ (nd : n = q.natDegree), (p + q).eraseLead.coeff n = (p + q.eraseLead).coeff n
neg : ∀ (nd : ¬n = q.natDegree), (p + q).eraseLead.coeff n = (p + q.eraseLead).coeff n
⊢ (p + q).eraseLead.coeff n = (p + q.eraseLead).coeff n

Tactic:
by_cases nd : n = q.natDegree

Premises used: Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : n = q.natDegree
pos : 0 = (p + q.eraseLead).coeff q.natDegree
⊢ (p + q).eraseLead.coeff n = (p + q.eraseLead).coeff n

Tactic:
rw [nd, eraseLead_coeff, if_pos (natDegree_add_eq_right_of_degree_lt pq).symm]

Premises used: Polynomial.eraseLead_coeff, if_pos, Polynomial.natDegree_add_eq_right_of_degree_lt, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : n = q.natDegree
⊢ 0 = (p + q.eraseLead).coeff q.natDegree

Tactic:
simpa using (coeff_eq_zero_of_degree_lt (lt_of_lt_of_le pq degree_le_natDegree)).symm

Premises used: Polynomial.degree_le_natDegree, Eq.symm, lt_of_lt_of_le, Polynomial.coeff_eq_zero_of_degree_lt
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : ¬n = q.natDegree
neg : ¬n = (p + q).natDegree
⊢ (p + q).eraseLead.coeff n = (p + q.eraseLead).coeff n

Tactic:
rw [eraseLead_coeff, coeff_add, coeff_add, eraseLead_coeff, if_neg, if_neg nd]

Premises used: Polynomial.eraseLead_coeff, Polynomial.coeff_add, if_neg
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
pq : p.degree < q.degree
nd : ¬(p + q).natDegree = q.natDegree
⊢ False

Tactic:
nd (natDegree_add_eq_right_of_degree_lt pq)

Premises used: Polynomial.natDegree_add_eq_right_of_degree_lt
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
pq : p.degree < q.degree
nd : ¬(p + q).natDegree = q.natDegree
⊢ False

Tactic:
exact nd (natDegree_add_eq_right_of_degree_lt pq)

Premises used: Polynomial.natDegree_add_eq_right_of_degree_lt
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
pq : p.natDegree < q.natDegree
⊢ (p + q).eraseLead = p + q.eraseLead

Tactic:
eraseLead_add_of_degree_lt_right (degree_lt_degree pq)

Premises used: Polynomial.eraseLead_add_of_degree_lt_right, Polynomial.degree_lt_degree
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
⊢ f.eraseLead.degree ≤ f.degree

Tactic:
f.degree_erase_le _

Premises used: Polynomial.eraseLead, Polynomial.degree_erase_le
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : f ≠ 0
⊢ f.eraseLead.degree < f.degree

Tactic:
f.degree_erase_lt hf

Premises used: Polynomial.degree_erase_lt, Polynomial.eraseLead
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
⊢ f.eraseLead.natDegree ≤ f.natDegree

Tactic:
natDegree_le_natDegree eraseLead_degree_le

Premises used: Polynomial.natDegree_le_natDegree, Polynomial.eraseLead_degree_le
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
f0 : 2 ≤ #f.support
⊢ f.eraseLead.natDegree < f.natDegree

Tactic:
lt_of_le_of_ne eraseLead_natDegree_le_aux <|
    ne_natDegree_of_mem_eraseLead_support <|
      natDegree_mem_support_of_nonzero <| eraseLead_ne_zero f0

Premises used: Polynomial.ne_natDegree_of_mem_eraseLead_support, Polynomial.natDegree_mem_support_of_nonzero, Polynomial.eraseLead_natDegree_le_aux, Polynomial.eraseLead_ne_zero, lt_of_le_of_ne
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.eraseLead ≠ 0
by_contra : ∀ (h₂ : ¬0 < f.natDegree), False
⊢ 0 < f.natDegree

Tactic:
by_contra h₂
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.eraseLead ≠ 0
h₂ : ¬0 < f.natDegree
⊢ Ne.{u_1 + 1} (α := R[X]) (eraseLead ((C : (a : R) → R[X]) (f.coeff 0))) 0

Tactic:
rw [eq_C_of_natDegree_eq_zero (Nat.eq_zero_of_not_pos h₂)] at h

Premises used: Polynomial.eq_C_of_natDegree_eq_zero, Nat.eq_zero_of_not_pos
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.eraseLead ≠ 0
h₂ : ¬0 < f.natDegree
h₁ : Ne.{u_1 + 1} (α := R[X]) (eraseLead ((C : (a : R) → R[X]) (f.coeff 0))) 0
⊢ ¬0 < f.natDegree

Tactic:
rw [eq_C_of_natDegree_eq_zero (Nat.eq_zero_of_not_pos h₂)] at h

Premises used: Polynomial.eq_C_of_natDegree_eq_zero, Nat.eq_zero_of_not_pos
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : Ne.{u_1 + 1} (α := R[X]) (eraseLead ((C : (a : R) → R[X]) (f.coeff 0))) 0
h₂ : ¬0 < f.natDegree
⊢ False

Tactic:
simp at h
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
pos : ∀ (h : #f.support ≤ 1), f.eraseLead.natDegree < f.natDegree ∨ f.eraseLead = 0
neg : ∀ (h : 1 < #f.support), f.eraseLead.natDegree < f.natDegree ∨ f.eraseLead = 0
⊢ f.eraseLead.natDegree < f.natDegree ∨ f.eraseLead = 0

Tactic:
by_cases! h : #f.support ≤ 1

Premises used: Polynomial.support
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : #f.support ≤ 1
pos : f.eraseLead = 0
⊢ f.eraseLead.natDegree < f.natDegree ∨ f.eraseLead = 0

Tactic:
right
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : #f.support ≤ 1
pos :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).eraseLead =
    0
⊢ f.eraseLead = 0

Tactic:
rw [← C_mul_X_pow_eq_self h]

Premises used: Polynomial.C_mul_X_pow_eq_self
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : #f.support ≤ 1
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).eraseLead =
    0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : 1 < #f.support
neg : f.eraseLead.natDegree < f.natDegree
⊢ f.eraseLead.natDegree < f.natDegree ∨ f.eraseLead = 0

Tactic:
left
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : 1 < #f.support
⊢ f.eraseLead.natDegree < f.natDegree

Tactic:
apply eraseLead_natDegree_lt h

Premises used: Polynomial.eraseLead_natDegree_lt
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
inl : ∀ (h : f.eraseLead.natDegree < f.natDegree), f.eraseLead.natDegree ≤ f.natDegree - 1
inr : ∀ (h : f.eraseLead = 0), f.eraseLead.natDegree ≤ f.natDegree - 1
⊢ f.eraseLead.natDegree ≤ f.natDegree - 1

Tactic:
rcases f.eraseLead_natDegree_lt_or_eraseLead_eq_zero with (h | h)

Premises used: Polynomial.eraseLead_natDegree_lt_or_eraseLead_eq_zero
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.eraseLead.natDegree < f.natDegree
⊢ f.eraseLead.natDegree ≤ f.natDegree - 1

Tactic:
Nat.le_sub_one_of_lt h

Premises used: Nat.le_sub_one_of_lt
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.eraseLead.natDegree < f.natDegree
⊢ f.eraseLead.natDegree ≤ f.natDegree - 1

Tactic:
exact Nat.le_sub_one_of_lt h

Premises used: Nat.le_sub_one_of_lt
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.eraseLead = 0
⊢ f.eraseLead.natDegree ≤ f.natDegree - 1

Tactic:
simp only [h, natDegree_zero, zero_le]

Premises used: zero_le, Polynomial.natDegree_zero
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
⊢ 0 < f.natDegree

Tactic:
have := natDegree_pos_of_nextCoeff_ne_zero h
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ f.eraseLead.natDegree = f.natDegree - 1

Tactic:
f.eraseLead_natDegree_le.antisymm <| le_natDegree_of_ne_zero ?_

Premises used: Polynomial.eraseLead_natDegree_le, LE.le.antisymm, Polynomial.le_natDegree_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
refine : f.eraseLead.coeff (f.natDegree - 1) ≠ 0
⊢ f.eraseLead.natDegree = f.natDegree - 1

Tactic:
refine f.eraseLead_natDegree_le.antisymm <| le_natDegree_of_ne_zero ?_

Premises used: Polynomial.eraseLead_natDegree_le, LE.le.antisymm, Polynomial.le_natDegree_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this rwa : 0 < f.natDegree
rwa₁ : 0 < f.natDegree
rwa₂ : LT.lt (α := ℕ) 0 1
⊢ f.eraseLead.coeff (f.natDegree - 1) ≠ 0

Tactic:
rwa [eraseLead_coeff_of_ne _ (tsub_lt_self _ _).ne, ← nextCoeff_of_natDegree_pos]

Premises used: Polynomial.nextCoeff_of_natDegree_pos, Polynomial.eraseLead_coeff_of_ne, tsub_lt_self, LT.lt.ne
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ 0 < f.natDegree

Tactic:
positivity
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ LT.lt (α := ℕ) 0 1

Tactic:
positivity
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
rw : 1 ≤ f.natDegree
⊢ f.eraseLead.natDegree + 1 = f.natDegree

Tactic:
rw [natDegree_eraseLead h, tsub_add_cancel_of_le]

Premises used: tsub_add_cancel_of_le, Polynomial.natDegree_eraseLead
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
⊢ 1 ≤ f.natDegree

Tactic:
natDegree_pos_of_nextCoeff_ne_zero h

Premises used: Polynomial.natDegree_pos_of_nextCoeff_ne_zero, Nat.lt
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
⊢ 1 ≤ f.natDegree

Tactic:
exact natDegree_pos_of_nextCoeff_ne_zero h

Premises used: Polynomial.natDegree_pos_of_nextCoeff_ne_zero
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.nextCoeff = 0
⊢ f.eraseLead.natDegree ≤ f.natDegree - 2

Tactic:
natDegree_le_pred (n := f.natDegree - 1) (eraseLead_natDegree_le f) ?_

Premises used: Polynomial.eraseLead_natDegree_le, WithBot.recBotCoe, Polynomial.natDegree_le_pred, Polynomial.natDegree, Nat.pred, WithBot.unbotD
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.nextCoeff = 0
refine : f.eraseLead.coeff (f.natDegree - 1) = 0
⊢ f.eraseLead.natDegree ≤ f.natDegree - 2

Tactic:
refine natDegree_le_pred (n := f.natDegree - 1) (eraseLead_natDegree_le f) ?_

Premises used: Polynomial.eraseLead_natDegree_le, Polynomial.natDegree_le_pred
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.nextCoeff = 0
⊢ (∃ (x : R), (C : (a : R) → R[X]) x = f) ∨ 0 < f.natDegree ∧ f.coeff (f.natDegree - 1) = 0

Tactic:
rw [nextCoeff_eq_zero, natDegree_eq_zero] at h

Premises used: Polynomial.nextCoeff_eq_zero, Polynomial.natDegree_eq_zero
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : (∃ (x : R), (C : (a : R) → R[X]) x = f) ∨ 0 < f.natDegree ∧ f.coeff (f.natDegree - 1) = 0
inl :
  ∀ (a : R),
    Eq.{u_1 + 1} (α := R)
      (coeff (eraseLead ((C : (a : R) → R[X]) a)) (natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) a) - 1)) 0
inr : ∀ (hf : 0 < f.natDegree) (h : f.coeff (f.natDegree - 1) = 0), f.eraseLead.coeff (f.natDegree - 1) = 0
⊢ f.eraseLead.coeff (f.natDegree - 1) = 0

Tactic:
obtain ⟨a, rfl⟩ | ⟨hf, h⟩ := h

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
a : R
⊢ Eq.{u_1 + 1} (α := R)
    (coeff (eraseLead ((C : (a : R) → R[X]) a)) (natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) a) - 1)) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : 0 < f.natDegree
h : f.coeff (f.natDegree - 1) = 0
inr : f.nextCoeff = 0
⊢ f.eraseLead.coeff (f.natDegree - 1) = 0

Tactic:
rw [eraseLead_coeff_of_ne _ (tsub_lt_self hf zero_lt_one).ne, ← nextCoeff_of_natDegree_pos hf]

Premises used: Polynomial.nextCoeff_of_natDegree_pos, zero_lt_one, Polynomial.eraseLead_coeff_of_ne, tsub_lt_self, LT.lt.ne
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : 0 < f.natDegree
h : f.coeff (f.natDegree - 1) = 0
⊢ f.nextCoeff = 0

Tactic:
simp [nextCoeff_eq_zero, h, eq_zero_or_pos]

Premises used: Polynomial.nextCoeff_eq_zero, eq_zero_or_pos
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hlead : f.eraseLead ≠ 0
hnext : f.nextCoeff = 0
contrapose! : ∀ (hlead : f.natDegree < 2), f.eraseLead = 0
⊢ 2 ≤ f.natDegree

Tactic:
contrapose! hlead
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hnext : f.nextCoeff = 0
hlead : f.natDegree < 2
⊢ (∃ (x : R), (C : (a : R) → R[X]) x = f) ∨
    ∃ (a : R),
      a ≠ 0 ∧
        ∃ (b : R),
          HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
              ((C : (a : R) → R[X]) b : R[X]) =
            f

Tactic:
rw [Nat.lt_succ_iff, Nat.le_one_iff_eq_zero_or_eq_one, natDegree_eq_zero, natDegree_eq_one]
    at hlead

Premises used: Nat.le_one_iff_eq_zero_or_eq_one, Polynomial.natDegree_eq_one, Nat.lt_succ_iff, Polynomial.natDegree_eq_zero
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hnext : f.nextCoeff = 0
hlead :
  (∃ (x : R), (C : (a : R) → R[X]) x = f) ∨
    ∃ (a : R),
      a ≠ 0 ∧
        ∃ (b : R),
          HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
              ((C : (a : R) → R[X]) b : R[X]) =
            f
inl :
  ∀ (a : R) (hnext : Eq.{u_1 + 1} (α := R) (nextCoeff ((C : (a : R) → R[X]) a)) 0),
    Eq.{u_1 + 1} (α := R[X]) (eraseLead ((C : (a : R) → R[X]) a)) 0
inr :
  ∀ (a : R) (ha : a ≠ 0) (b : R)
    (hnext :
      (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
            ((C : (a : R) → R[X]) b : R[X])).nextCoeff =
        0),
    (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
          ((C : (a : R) → R[X]) b : R[X])).eraseLead =
      0
⊢ f.eraseLead = 0

Tactic:
obtain ⟨a, rfl⟩ | ⟨a, ha, b, rfl⟩ := hlead

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
a : R
hnext : Eq.{u_1 + 1} (α := R) (nextCoeff ((C : (a : R) → R[X]) a)) 0
⊢ Eq.{u_1 + 1} (α := R[X]) (eraseLead ((C : (a : R) → R[X]) a)) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
a : R
ha : a ≠ 0
b : R
hnext :
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).nextCoeff =
    0
⊢ b = 0

Tactic:
rw [nextCoeff_C_mul_X_add_C ha] at hnext

Premises used: Polynomial.nextCoeff_C_mul_X_add_C
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
a : R
ha : a ≠ 0
b : R
hnext : b = 0
inr : (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X + (C : (a : R) → R[X]) 0).eraseLead = 0
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).eraseLead =
    0

Tactic:
subst b
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
a : R
ha : a ≠ 0
⊢ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X + (C : (a : R) → R[X]) 0).eraseLead = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
rw : 0 < f.natDegree
rw₁ : LT.lt (α := ℕ) 0 1
hnc : ¬f.natDegree = 0
⊢ f.eraseLead.leadingCoeff = f.nextCoeff

Tactic:
rw [leadingCoeff, nextCoeff, natDegree_eraseLead h, if_neg,
    eraseLead_coeff_of_ne _ (tsub_lt_self _ _).ne]

Premises used: Polynomial.leadingCoeff, Polynomial.nextCoeff, Polynomial.natDegree_eraseLead, Polynomial.eraseLead_coeff_of_ne, if_neg, tsub_lt_self, LT.lt.ne
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ ¬f.natDegree = 0

Tactic:
positivity
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.eraseLead = 0
by_contra : ∀ (h₂ : ¬f.nextCoeff = 0), False
⊢ f.nextCoeff = 0

Tactic:
by_contra h₂
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.eraseLead = 0
h₂ : ¬f.nextCoeff = 0
⊢ False

Tactic:
leadingCoeff_ne_zero.mp (leadingCoeff_eraseLead_eq_nextCoeff h₂ ▸ h₂) h

Premises used: Polynomial.leadingCoeff_ne_zero, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.eraseLead = 0
h₂ : ¬f.nextCoeff = 0
⊢ False

Tactic:
exact leadingCoeff_ne_zero.mp (leadingCoeff_eraseLead_eq_nextCoeff h₂ ▸ h₂) h

Premises used: Polynomial.leadingCoeff_ne_zero, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_2
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
pos :
  ∀ (hp : P = 0),
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead =
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead
neg :
  ∀ (hp : ¬P = 0),
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead =
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead

Tactic:
by_cases hp : P = 0
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_2
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : P = 0
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead

Tactic:
simp [hp]
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_2
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
pos :
  ∀ (he : P.eraseLead = 0),
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead =
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead
neg :
  ∀ (he : ¬P.eraseLead = 0),
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead =
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead

Tactic:
by_cases he : P.eraseLead = 0

Premises used: Polynomial.eraseLead