awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
inst_2 : Nontrivial R
inl :
  ∀ (hd : p.degree < 0),
    (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).leadingCoeff = p.leadingCoeff
inr :
  ∀ (hd : 0 < p.degree),
    (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).leadingCoeff = p.leadingCoeff
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).leadingCoeff = p.leadingCoeff

Tactic:
rcases hp.lt_or_gt with hd | hd

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
inst_2 : Nontrivial R
hd : p.degree < 0
inl : (0 /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).leadingCoeff = leadingCoeff 0
inl₁ inl₂ : Eq.{u + 1} (α := R) (leadingCoeff 0) (leadingCoeff 0)
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).leadingCoeff = p.leadingCoeff

Tactic:
rw [degree_eq_bot.mp <| Nat.WithBot.lt_zero_iff.mp hd, zero_divByMonic]

Premises used: Polynomial.zero_divByMonic, Nat.WithBot.lt_zero_iff, Iff.mp, Polynomial.degree_eq_bot
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
inst_2 : Nontrivial R
hd : 0 < p.degree
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).leadingCoeff = p.leadingCoeff

Tactic:
leadingCoeff_divByMonic_of_monic (monic_X_sub_C a) ?_

Premises used: Polynomial.monic_X_sub_C, Polynomial.leadingCoeff_divByMonic_of_monic
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
inst_2 : Nontrivial R
hd : 0 < p.degree
inr : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree ≤ p.degree
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).leadingCoeff = p.leadingCoeff

Tactic:
refine leadingCoeff_divByMonic_of_monic (monic_X_sub_C a) ?_

Premises used: Polynomial.monic_X_sub_C, Polynomial.leadingCoeff_divByMonic_of_monic
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
inst_2 : Nontrivial R
hd : 0 < p.degree
inr : 1 ≤ p.degree
inr₁ inr₂ inr₃ inr₄ : 0 < p.degree
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree ≤ p.degree

Tactic:
rwa [degree_X_sub_C, Nat.WithBot.one_le_iff_zero_lt]

Premises used: Polynomial.degree_X_sub_C, Nat.WithBot.one_le_iff_zero_lt
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
hpq : p ∣ q
h₁ : q.natDegree ≤ p.natDegree
h₂ : p.leadingCoeff = q.leadingCoeff
inl : ∀ (hpq : p ∣ 0) (h₁ : natDegree.{u} (R := R) 0 ≤ p.natDegree) (h₂ : p.leadingCoeff = leadingCoeff 0), p = 0
inr : ∀ (hq : q ≠ 0), p = q
⊢ p = q

Tactic:
rcases eq_or_ne q 0 with rfl | hq

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hpq : p ∣ 0
h₁ : natDegree.{u} (R := R) 0 ≤ p.natDegree
h₂ : p.leadingCoeff = leadingCoeff 0
⊢ p = 0

Tactic:
simpa using h₂
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
hpq : p ∣ q
h₁ : q.natDegree ≤ p.natDegree
h₂ : p.leadingCoeff = q.leadingCoeff
hq : q ≠ 0
⊢ p.natDegree = q.natDegree

Tactic:
replace h₁ := (natDegree_le_of_dvd hpq hq).antisymm h₁
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
hpq : p ∣ q
h₂ : p.leadingCoeff = q.leadingCoeff
hq : q ≠ 0
h₁ : p.natDegree = q.natDegree
inr :
  ∀ (u : R[X]) (h₂ : p.leadingCoeff = (p * u).leadingCoeff) (hq : p * u ≠ 0) (h₁ : p.natDegree = (p * u).natDegree),
    p = p * u
⊢ p = q

Tactic:
obtain ⟨u, rfl⟩ := hpq

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p u : R[X]
h₂ : p.leadingCoeff = (p * u).leadingCoeff
hq : p * u ≠ 0
h₁ : p.natDegree = (p * u).natDegree
⊢ p ≠ 0 ∧ u ≠ 0

Tactic:
rw [mul_ne_zero_iff] at hq

Premises used: mul_ne_zero_iff
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p u : R[X]
h₂ : p.leadingCoeff = (p * u).leadingCoeff
hq : p * u ≠ 0
h₁ : p.natDegree = (p * u).natDegree
hq₁ : p ≠ 0 ∧ u ≠ 0
⊢ p.natDegree = (p * u).natDegree

Tactic:
rw [mul_ne_zero_iff] at hq

Premises used: mul_ne_zero_iff
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p u : R[X]
h₂ : p.leadingCoeff = (p * u).leadingCoeff
hq : p ≠ 0 ∧ u ≠ 0
h₁ : p.natDegree = (p * u).natDegree
⊢ u.natDegree = 0

Tactic:
rw [natDegree_mul hq.1 hq.2, left_eq_add] at h₁

Premises used: left_eq_add, Polynomial.natDegree_mul, And.right, And.left
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p u : R[X]
h₂ : p.leadingCoeff = (p * u).leadingCoeff
hq : p ≠ 0 ∧ u ≠ 0
h₁ : u.natDegree = 0
⊢ u.coeff 0 = 1

Tactic:
rw [eq_C_of_natDegree_eq_zero h₁, leadingCoeff_mul, leadingCoeff_C,
    eq_comm, mul_eq_left₀ (leadingCoeff_ne_zero.mpr hq.1)] at h₂

Premises used: Iff.mpr, Polynomial.leadingCoeff_mul, mul_eq_left₀, Polynomial.eq_C_of_natDegree_eq_zero, eq_comm, And.left, Polynomial.leadingCoeff_ne_zero, Polynomial.leadingCoeff_C
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p u : R[X]
h₂ : p.leadingCoeff = (p * u).leadingCoeff
hq : p ≠ 0 ∧ u ≠ 0
h₁ : u.natDegree = 0
h₃ : u.coeff 0 = 1
⊢ p ≠ 0 ∧ u ≠ 0

Tactic:
rw [eq_C_of_natDegree_eq_zero h₁, leadingCoeff_mul, leadingCoeff_C,
    eq_comm, mul_eq_left₀ (leadingCoeff_ne_zero.mpr hq.1)] at h₂

Premises used: Iff.mpr, Polynomial.leadingCoeff_mul, mul_eq_left₀, Polynomial.eq_C_of_natDegree_eq_zero, eq_comm, And.left, Polynomial.leadingCoeff_ne_zero, Polynomial.leadingCoeff_C
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p u : R[X]
h₂ : p.leadingCoeff = (p * u).leadingCoeff
hq : p ≠ 0 ∧ u ≠ 0
h₁ : u.natDegree = 0
h₃ : u.coeff 0 = 1
hq₁ : p ≠ 0 ∧ u ≠ 0
⊢ u.natDegree = 0

Tactic:
rw [eq_C_of_natDegree_eq_zero h₁, leadingCoeff_mul, leadingCoeff_C,
    eq_comm, mul_eq_left₀ (leadingCoeff_ne_zero.mpr hq.1)] at h₂

Premises used: Iff.mpr, Polynomial.leadingCoeff_mul, mul_eq_left₀, Polynomial.eq_C_of_natDegree_eq_zero, eq_comm, And.left, Polynomial.leadingCoeff_ne_zero, Polynomial.leadingCoeff_C
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p u : R[X]
h₂ : u.coeff 0 = 1
hq : p ≠ 0 ∧ u ≠ 0
h₁ : u.natDegree = 0
inr : p = HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) (u.coeff 0) : R[X])
inr₁ : p = p * (C : (a : R) → R[X]) 1
inr₂ : p = p * 1
inr₃ inr₄ : p = p
⊢ p = p * u

Tactic:
rw [eq_C_of_natDegree_eq_zero h₁, h₂, map_one, mul_one]

Premises used: Polynomial.eq_C_of_natDegree_eq_zero, map_one, mul_one
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
hpq : p ∣ q
h₁ : q.natDegree ≤ p.natDegree
h₂ : q.leadingCoeff ∣ p.leadingCoeff
r : R[X]
hr : q = p * r
u : Rˣ
hu : p.leadingCoeff * (↑u : R) = q.leadingCoeff
rwa rwa₁ rwa₂ rwa₃ : p ∣ q
⊢ p * (↑((Units.map (↑C : R →* R[X]) : (a : Rˣ) → R[X]ˣ) u) : R[X]) ∣ q

Tactic:
rwa [Units.mul_right_dvd]

Premises used: Units.mul_right_dvd
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
hpq : p ∣ q
h₁ : q.natDegree ≤ p.natDegree
h₂ : q.leadingCoeff ∣ p.leadingCoeff
r : R[X]
hr : q = p * r
u : Rˣ
hu : p.leadingCoeff * (↑u : R) = q.leadingCoeff
⊢ q.natDegree ≤ (p * (↑((Units.map (↑C : R →* R[X]) : (a : Rˣ) → R[X]ˣ) u) : R[X])).natDegree

Tactic:
simpa [natDegree_mul_C] using h₁

Premises used: Polynomial.natDegree_mul_C
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
hpq : p ∣ q
h₁ : q.natDegree ≤ p.natDegree
h₂ : q.leadingCoeff ∣ p.leadingCoeff
r : R[X]
hr : q = p * r
u : Rˣ
hu : p.leadingCoeff * (↑u : R) = q.leadingCoeff
⊢ (p * (↑((Units.map (↑C : R →* R[X]) : (a : Rˣ) → R[X]ˣ) u) : R[X])).leadingCoeff = q.leadingCoeff

Tactic:
simpa using hu
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
K : Type u_1
inst : Field K
p q : K[X]
hpq : p ∣ q
hq : q ≠ 0
h₁ : q.natDegree ≤ p.natDegree
rwa : ∀ (hq : q.leadingCoeff ≠ 0) (h₁ : q.natDegree ≤ p.natDegree), IsUnit q.leadingCoeff
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (hq : IsUnit q.leadingCoeff) (h₁ : q.natDegree ≤ p.natDegree), IsUnit q.leadingCoeff
⊢ IsUnit q.leadingCoeff

Tactic:
rwa [← leadingCoeff_ne_zero, ← isUnit_iff_ne_zero] at hq

Premises used: isUnit_iff_ne_zero, Polynomial.leadingCoeff_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
K : Type u_1
inst : Field K
p q : K[X]
hpq : p ∣ q
h₁ : p.degree = q.degree
hq : q = 0
⊢ p = q

Tactic:
simpa [hq] using h₁
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
hp : p.Monic
hdvd : p ∣ q
hdeg : q.natDegree ≤ p.natDegree
rw : q = HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
rw₁ rw₂ : q = q
⊢ q = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X]) p

Tactic:
rw [mul_comm, ← eq_mul_leadingCoeff_of_monic_of_dvd_of_natDegree_le hp hdvd hdeg]

Premises used: Polynomial.eq_mul_leadingCoeff_of_monic_of_dvd_of_natDegree_le, mul_comm
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
⊢ f.eraseLead.support = f.support.erase f.natDegree

Tactic:
simp only [eraseLead, support_erase]

Premises used: Polynomial.eraseLead, Polynomial.support_erase
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
i : ℕ
⊢ f.eraseLead.coeff i = if i = f.natDegree then 0 else f.coeff i

Tactic:
simp only [eraseLead, coeff_erase]

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

Tactic:
simp [eraseLead_coeff]

Premises used: Polynomial.eraseLead_coeff
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
i : ℕ
hi : i ≠ f.natDegree
⊢ f.eraseLead.coeff i = f.coeff i

Tactic:
simp [eraseLead_coeff, hi]

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

Tactic:
simp only [eraseLead, erase_zero]

Premises used: Polynomial.eraseLead, Polynomial.erase_zero
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
⊢ HAdd.hAdd (β := R[X]) f.eraseLead ((monomial f.natDegree : (a : R) → R[X]) f.leadingCoeff : R[X]) = f

Tactic:
(add_comm _ _).trans (f.monomial_add_erase _)

Premises used: add_comm, Eq.trans, Polynomial.monomial_add_erase
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
rw : HAdd.hAdd (β := R[X]) f.eraseLead ((monomial f.natDegree : (a : R) → R[X]) f.leadingCoeff : R[X]) = f
rw₁ rw₂ : f = f
⊢ f.eraseLead +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree) =
    f

Tactic:
rw [C_mul_X_pow_eq_monomial, eraseLead_add_monomial_natDegree_leadingCoeff]

Premises used: Polynomial.C_mul_X_pow_eq_monomial, Polynomial.eraseLead_add_monomial_natDegree_leadingCoeff
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_2
inst : Ring R
f : R[X]
⊢ HSub.hSub (β := R[X]) f ((monomial f.natDegree : (a : R) → R[X]) f.leadingCoeff : R[X]) = f.eraseLead

Tactic:
(eq_sub_iff_add_eq.mpr (eraseLead_add_monomial_natDegree_leadingCoeff f)).symm

Premises used: Iff.mpr, eq_sub_iff_add_eq, Polynomial.eraseLead_add_monomial_natDegree_leadingCoeff, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_2
inst : Ring R
f : R[X]
rw : HSub.hSub (β := R[X]) f ((monomial f.natDegree : (a : R) → R[X]) f.leadingCoeff : R[X]) = f.eraseLead
rw₁ rw₂ : f.eraseLead = f.eraseLead
⊢ f - HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree) =
    f.eraseLead

Tactic:
rw [C_mul_X_pow_eq_monomial, self_sub_monomial_natDegree_leadingCoeff]

Premises used: Polynomial.self_sub_monomial_natDegree_leadingCoeff, Polynomial.C_mul_X_pow_eq_monomial
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
f0 : 2 ≤ #f.support
rw : ¬#(f.support.erase f.natDegree) = 0
⊢ f.eraseLead ≠ 0

Tactic:
rw [Ne, ← card_support_eq_zero, eraseLead_support]

Premises used: Polynomial.eraseLead_support, Ne, Polynomial.card_support_eq_zero
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
f0 : 2 ≤ #f.support
⊢ ¬#(f.support.erase f.natDegree) = 0

Tactic:
(zero_lt_one.trans_le <| (tsub_le_tsub_right f0 1).trans Finset.pred_card_le_card_erase).ne.symm

Premises used: Ne.symm, zero_lt_one, Finset.pred_card_le_card_erase, LT.lt.trans_le, tsub_le_tsub_right, LE.le.trans, OfNat.ofNat, LT.lt.ne
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
f0 : 2 ≤ #f.support
⊢ ¬#(f.support.erase f.natDegree) = 0

Tactic:
exact
    (zero_lt_one.trans_le <| (tsub_le_tsub_right f0 1).trans Finset.pred_card_le_card_erase).ne.symm

Premises used: Ne.symm, zero_lt_one, Finset.pred_card_le_card_erase, LT.lt.trans_le, tsub_le_tsub_right, LE.le.trans, OfNat.ofNat, LT.lt.ne
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
a : ℕ
h : a ∈ f.eraseLead.support
⊢ a ≠ f.natDegree ∧ a ∈ f.support

Tactic:
rw [eraseLead_support, mem_erase] at h

Premises used: Polynomial.eraseLead_support, Finset.mem_erase
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
a : ℕ
h : a ≠ f.natDegree ∧ a ∈ f.support
⊢ a < f.natDegree

Tactic:
(le_natDegree_of_mem_supp a h.2).lt_of_ne h.1

Premises used: Polynomial.le_natDegree_of_mem_supp, LE.le.lt_of_ne, And.right, And.left
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
a : ℕ
h : a ≠ f.natDegree ∧ a ∈ f.support
⊢ a < f.natDegree

Tactic:
exact (le_natDegree_of_mem_supp a h.2).lt_of_ne h.1

Premises used: Polynomial.le_natDegree_of_mem_supp, LE.le.lt_of_ne, And.right, And.left
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
a : ℕ
h : a ∈ f.eraseLead.support
⊢ a ≠ f.natDegree

Tactic:
(lt_natDegree_of_mem_eraseLead_support h).ne

Premises used: Polynomial.lt_natDegree_of_mem_eraseLead_support, LT.lt.ne
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
⊢ f.natDegree ∉ f.eraseLead.support

Tactic:
fun h =>
  ne_natDegree_of_mem_eraseLead_support h rfl

Premises used: Polynomial.ne_natDegree_of_mem_eraseLead_support, Not, rfl
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f ≠ 0
rw : #(f.support.erase f.natDegree) < #f.support
⊢ #f.eraseLead.support < #f.support

Tactic:
rw [eraseLead_support]

Premises used: Polynomial.eraseLead_support
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f ≠ 0
⊢ #(f.support.erase f.natDegree) < #f.support

Tactic:
card_lt_card (erase_ssubset <| natDegree_mem_support_of_nonzero h)

Premises used: Finset.card_lt_card, Polynomial.natDegree_mem_support_of_nonzero, Finset.erase_ssubset
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f ≠ 0
⊢ #(f.support.erase f.natDegree) < #f.support

Tactic:
exact card_lt_card (erase_ssubset <| natDegree_mem_support_of_nonzero h)

Premises used: Finset.card_lt_card, Polynomial.natDegree_mem_support_of_nonzero, Finset.erase_ssubset
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f ≠ 0
set :
  let c := #f.support;
  ∀ (hc : c = #f.support), #f.eraseLead.support + 1 = c
⊢ #f.eraseLead.support + 1 = #f.support

Tactic:
set c := #f.support with hc

Premises used: Polynomial.support
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
cases : ∀ (h₁ : c = 0), #f.eraseLead.support + 1 = 0
cases₁ : ∀ (n : ℕ) (h₁ : c = n + 1), #f.eraseLead.support + 1 = n + 1
⊢ #f.eraseLead.support + 1 = c

Tactic:
cases h₁ : c
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
h₁ : c = 0
by_contra : ∀ (this : ¬#f.eraseLead.support + 1 = 0), False
⊢ #f.eraseLead.support + 1 = 0

Tactic:
by_contra
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
h₁ : c = 0
this : ¬#f.eraseLead.support + 1 = 0
⊢ False

Tactic:
h (card_support_eq_zero.mp h₁)

Premises used: Polynomial.card_support_eq_zero, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
h₁ : c = 0
this : ¬#f.eraseLead.support + 1 = 0
⊢ False

Tactic:
exact h (card_support_eq_zero.mp h₁)

Premises used: Polynomial.card_support_eq_zero, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
h₁ : c = 0
⊢ #f.eraseLead.support + 1 = 0

Tactic:
case zero =>
    by_contra
    exact h (card_support_eq_zero.mp h₁)

Premises used: Polynomial.card_support_eq_zero, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
n : ℕ
h₁ : c = n + 1
rw : n + 1 - 1 + 1 = n + 1
⊢ #f.eraseLead.support + 1 = n + 1

Tactic:
rw [eraseLead_support, card_erase_of_mem (natDegree_mem_support_of_nonzero h), ← hc, h₁]

Premises used: Polynomial.eraseLead_support, Finset.card_erase_of_mem, Polynomial.natDegree_mem_support_of_nonzero
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
n : ℕ
h₁ : c = n + 1
⊢ n + 1 - 1 + 1 = n + 1

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
n : ℕ
h₁ : c = n + 1
case : #(f.support.erase f.natDegree) + 1 = n + 1
case₁ : #f.support - 1 + 1 = n + 1
case₂ : c - 1 + 1 = n + 1
case₃ case₄ case₅ : n + 1 - 1 + 1 = n + 1
⊢ #f.eraseLead.support + 1 = n + 1

Tactic:
case succ =>
    rw [eraseLead_support, card_erase_of_mem (natDegree_mem_support_of_nonzero h), ← hc, h₁]
    rfl

Premises used: Polynomial.eraseLead_support, Finset.card_erase_of_mem, Polynomial.natDegree_mem_support_of_nonzero
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
pos : ∀ (hf : f = 0), #f.eraseLead.support = #f.support - 1
neg : ∀ (hf : ¬f = 0), #f.eraseLead.support = #f.support - 1
⊢ #f.eraseLead.support = #f.support - 1

Tactic:
by_cases hf : f = 0
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : f = 0
pos : #(support.{u_1} (R := R) (eraseLead 0)) = #(support.{u_1} (R := R) 0) - 1
pos₁ : #(support.{u_1} (R := R) 0) = #(support.{u_1} (R := R) 0) - 1
pos₂ : card (α := ℕ) ∅ = card (α := ℕ) ∅ - 1
pos₃ pos₄ : 0 = HSub.hSub (α := ℕ) 0 1
⊢ #f.eraseLead.support = #f.support - 1

Tactic:
rw [hf, eraseLead_zero, support_zero, card_empty]

Premises used: Polynomial.eraseLead_zero, Finset.card_empty, Polynomial.support_zero
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : ¬f = 0
neg : #f.eraseLead.support = #f.eraseLead.support + 1 - 1
neg₁ neg₂ : #f.eraseLead.support = #f.eraseLead.support
⊢ #f.eraseLead.support = #f.support - 1

Tactic:
rw [← card_support_eraseLead_add_one hf, add_tsub_cancel_right]

Premises used: Polynomial.card_support_eraseLead_add_one, add_tsub_cancel_right
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
c : ℕ
fc : #f.support = c + 1
rw : #f.support - 1 = c
rw₁ : c + 1 - 1 = c
rw₂ rw₃ : c = c
⊢ #f.eraseLead.support = c

Tactic:
rw [card_support_eraseLead, fc, add_tsub_cancel_right]

Premises used: Polynomial.card_support_eraseLead, add_tsub_cancel_right
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.eraseLead = 0
by_cases : ∀ (hpz : f = 0), #f.support ≤ 1
by_cases₁ : ∀ (hpz : ¬f = 0), #f.support ≤ 1
⊢ #f.support ≤ 1

Tactic:
by_cases hpz : f = 0
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.eraseLead = 0
hpz : f = 0
⊢ #f.support ≤ 1

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

Tactic:
case pos => simp [hpz]
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.eraseLead = 0
hpz : ¬f = 0
⊢ #f.support ≤ 1

Tactic:
le_of_eq (card_support_eq_one_of_eraseLead_eq_zero hpz h)

Premises used: Polynomial.card_support_eq_one_of_eraseLead_eq_zero, le_of_eq
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.eraseLead = 0
hpz : ¬f = 0
⊢ #f.support ≤ 1

Tactic:
exact le_of_eq (card_support_eq_one_of_eraseLead_eq_zero hpz h)

Premises used: Polynomial.card_support_eq_one_of_eraseLead_eq_zero, le_of_eq
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.eraseLead = 0
hpz : ¬f = 0
⊢ #f.support ≤ 1

Tactic:
case neg => exact le_of_eq (card_support_eq_one_of_eraseLead_eq_zero hpz h)

Premises used: Polynomial.card_support_eq_one_of_eraseLead_eq_zero, le_of_eq
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
i : ℕ
r : R
pos : ∀ (hr : r = 0), Eq.{u_1 + 1} (α := R[X]) (eraseLead ((monomial i : (a : R) → R[X]) r)) 0
neg : ∀ (hr : ¬r = 0), Eq.{u_1 + 1} (α := R[X]) (eraseLead ((monomial i : (a : R) → R[X]) r)) 0
⊢ Eq.{u_1 + 1} (α := R[X]) (eraseLead ((monomial i : (a : R) → R[X]) r)) 0

Tactic:
by_cases hr : r = 0
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
i : ℕ
r : R
hr : r = 0
pos : Eq.{u_1 + 1} (α := R[X]) (eraseLead ((monomial i : (a : R) → R[X]) 0)) 0
⊢ Eq.{u_1 + 1} (α := R[X]) (eraseLead ((monomial i : (a : R) → R[X]) r)) 0

Tactic:
subst r
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
i : ℕ
⊢ Eq.{u_1 + 1} (α := R[X]) (eraseLead ((monomial i : (a : R) → R[X]) 0)) 0

Tactic:
simp only [monomial_zero_right, eraseLead_zero]

Premises used: Polynomial.eraseLead_zero, Polynomial.monomial_zero_right
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
i : ℕ
r : R
hr : ¬r = 0
neg :
  Eq.{u_1 + 1} (α := R[X])
    (erase (natDegree.{u_1} (R := R) ((monomial i : (a : R) → R[X]) r)) ((monomial i : (a : R) → R[X]) r)) 0
neg₁ : Eq.{u_1 + 1} (α := R[X]) (erase (if r = 0 then 0 else i) ((monomial i : (a : R) → R[X]) r)) 0
neg₂ : Eq.{u_1 + 1} (α := R[X]) (erase i ((monomial i : (a : R) → R[X]) r)) 0
neg₃ neg₄ : Eq.{u_1 + 1} (α := R[X]) 0 0
⊢ Eq.{u_1 + 1} (α := R[X]) (eraseLead ((monomial i : (a : R) → R[X]) r)) 0

Tactic:
rw [eraseLead, natDegree_monomial, if_neg hr, erase_monomial]

Premises used: Polynomial.eraseLead, Polynomial.natDegree_monomial, if_neg, Polynomial.erase_monomial
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
i : ℕ
r : R
pos : ∀ (hr : r = 0), Eq.{u_1 + 1} (α := R[X]) (eraseLead ((monomial i : (a : R) → R[X]) r)) 0
neg neg₁ : ∀ (hr : ¬r = 0), Eq.{u_1 + 1} (α := R[X]) (eraseLead ((monomial i : (a : R) → R[X]) r)) 0
⊢ Eq.{u_1 + 1} (α := R[X]) (eraseLead ((monomial i : (a : R) → R[X]) r)) 0

Tactic:
classical
  by_cases hr : r = 0
  · subst r
    simp only [monomial_zero_right, eraseLead_zero]
  · rw [eraseLead, natDegree_monomial, if_neg hr, erase_monomial]

Premises used: Polynomial.eraseLead, Polynomial.eraseLead_zero, Polynomial.natDegree_monomial, Polynomial.monomial_zero_right, Polynomial.erase_monomial