awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd : LT.lt.{u_3} (α := m.syn) (0 : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
unfold :
  LT.lt.{u_3} (α := m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
          ((m.toSyn.symm : (a : m.syn) → σ →₀ ℕ) (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn))) :
        m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn) ↔
    ∀ c ∈ f.support,
      LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
⊢ LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn) ↔
    ∀ c ∈ f.support,
      LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)

Tactic:
unfold degree

Premises used: MonomialOrder.degree
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd : LT.lt.{u_3} (α := m.syn) (0 : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
simp :
  LT.lt.{u_3} (α := m.syn) (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn) ↔
    ∀ c ∈ f.support,
      LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
⊢ LT.lt.{u_3} (α := m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
          ((m.toSyn.symm : (a : m.syn) → σ →₀ ℕ) (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn))) :
        m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn) ↔
    ∀ c ∈ f.support,
      LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)

Tactic:
simp only [AddEquiv.apply_symm_apply]

Premises used: AddEquiv.apply_symm_apply
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd : LT.lt.{u_3} (α := m.syn) (0 : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
⊢ LT.lt.{u_3} (α := m.syn) (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn) ↔
    ∀ c ∈ f.support,
      LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)

Tactic:
Finset.sup_lt_iff hd

Premises used: Finset.sup_lt_iff
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd : LT.lt.{u_3} (α := m.syn) (0 : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
⊢ LT.lt.{u_3} (α := m.syn) (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn) ↔
    ∀ c ∈ f.support,
      LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)

Tactic:
exact Finset.sup_lt_iff hd

Premises used: Finset.sup_lt_iff
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd : d ∈ f.support
unfold :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
        ((m.toSyn.symm : (a : m.syn) → σ →₀ ℕ) (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn))) :
      m.syn)
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)

Tactic:
unfold degree

Premises used: MonomialOrder.degree
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd : d ∈ f.support
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
        ((m.toSyn.symm : (a : m.syn) → σ →₀ ℕ) (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn))) :
      m.syn)

Tactic:
simp only [AddEquiv.apply_symm_apply, Finset.le_sup hd]

Premises used: AddEquiv.apply_symm_apply, Finset.le_sup
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
⊢ ¬LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)

Tactic:
rw [← not_le] at hd

Premises used: not_le
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd :
  ¬LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
by_contra : ∀ (hf : ¬coeff d f = 0), False
⊢ coeff d f = 0

Tactic:
by_contra hf
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd :
  ¬LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
hf : ¬coeff d f = 0
⊢ False

Tactic:
apply hd (m.le_degree (mem_support_iff.mpr hf))

Premises used: Iff.mpr, MvPolynomial.mem_support_iff, MonomialOrder.le_degree
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
mp : m.leadingCoeff f ≠ 0 → f ≠ 0
mpr : f ≠ 0 → m.leadingCoeff f ≠ 0
⊢ m.leadingCoeff f ≠ 0 ↔ f ≠ 0

Tactic:
constructor
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
mp : f = 0 → m.leadingCoeff f = 0
⊢ m.leadingCoeff f ≠ 0 → f ≠ 0

Tactic:
rw [not_imp_not]

Premises used: not_imp_not
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
hf : f = 0
mp : Eq.{u_2 + 1} (α := R) (m.leadingCoeff 0) 0
mp₁ mp₂ : Eq.{u_2 + 1} (α := R) 0 0
⊢ m.leadingCoeff f = 0

Tactic:
rw [hf, leadingCoeff_zero]

Premises used: MonomialOrder.leadingCoeff_zero
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
hf : f ≠ 0
⊢ f.support.Nonempty

Tactic:
rw [← support_nonempty] at hf

Premises used: MvPolynomial.support_nonempty
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
hf : f.support.Nonempty
mpr : (m.toSyn.symm : (a : m.syn) → σ →₀ ℕ) (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn)) ∈ f.support
⊢ m.leadingCoeff f ≠ 0

Tactic:
rw [leadingCoeff, ← mem_support_iff, degree]

Premises used: MvPolynomial.mem_support_iff, MonomialOrder.leadingCoeff, MonomialOrder.degree
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
hf : f.support.Nonempty
this :
  Membership.mem (γ := Set m.syn) ((⇑m.toSyn : (a : σ →₀ ℕ) → m.syn) '' (↑f.support : Set (σ →₀ ℕ)))
    (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn))
obtain :
  ∀ (d : σ →₀ ℕ) (hd : d ∈ (↑f.support : Set (σ →₀ ℕ)))
    (hd' :
      Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
        (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn) : m.syn)),
    (m.toSyn.symm : (a : m.syn) → σ →₀ ℕ) (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn)) ∈ f.support
⊢ (m.toSyn.symm : (a : m.syn) → σ →₀ ℕ) (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn)) ∈ f.support

Tactic:
obtain ⟨d, hd, hd'⟩ := this
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
hf : f.support.Nonempty
d : σ →₀ ℕ
hd : d ∈ (↑f.support : Set (σ →₀ ℕ))
hd' :
  Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
    (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn) : m.syn)
rw : d ∈ f.support
⊢ (m.toSyn.symm : (a : m.syn) → σ →₀ ℕ) (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn)) ∈ f.support

Tactic:
rw [← hd', AddEquiv.symm_apply_apply]

Premises used: AddEquiv.symm_apply_apply
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
hf : f.support.Nonempty
d : σ →₀ ℕ
hd : d ∈ (↑f.support : Set (σ →₀ ℕ))
hd' :
  Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
    (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn) : m.syn)
⊢ d ∈ f.support

Tactic:
hd
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
hf : f.support.Nonempty
d : σ →₀ ℕ
hd : d ∈ (↑f.support : Set (σ →₀ ℕ))
hd' :
  Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
    (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn) : m.syn)
⊢ d ∈ f.support

Tactic:
exact hd
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
hf : f.support.Nonempty
mpr :
  Membership.mem (γ := Set m.syn) ((⇑m.toSyn : (a : σ →₀ ℕ) → m.syn) '' (↑f.support : Set (σ →₀ ℕ)))
    (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn))
⊢ (m.toSyn.symm : (a : m.syn) → σ →₀ ℕ) (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn)) ∈ f.support

Tactic:
suffices f.support.sup m.toSyn ∈ m.toSyn '' f.support by
      obtain ⟨d, hd, hd'⟩ := this
      rw [← hd', AddEquiv.symm_apply_apply]
      exact hd
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
hf : f.support.Nonempty
⊢ Membership.mem (γ := Set m.syn) ((⇑m.toSyn : (a : σ →₀ ℕ) → m.syn) '' (↑f.support : Set (σ →₀ ℕ)))
    (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn))

Tactic:
Finset.sup_mem_of_nonempty hf

Premises used: Finset.sup_mem_of_nonempty
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
hf : f.support.Nonempty
⊢ Membership.mem (γ := Set m.syn) ((⇑m.toSyn : (a : σ →₀ ℕ) → m.syn) '' (↑f.support : Set (σ →₀ ℕ)))
    (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn))

Tactic:
exact Finset.sup_mem_of_nonempty hf

Premises used: Finset.sup_mem_of_nonempty
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
⊢ m.leadingCoeff f = 0 ↔ f = 0

Tactic:
simp only [← not_iff_not, leadingCoeff_ne_zero_iff]

Premises used: not_iff_not, MonomialOrder.leadingCoeff_ne_zero_iff
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
⊢ coeff (m.degree f) f ≠ 0 ↔ f ≠ 0

Tactic:
m.leadingCoeff_ne_zero_iff

Premises used: MonomialOrder.leadingCoeff, MonomialOrder.leadingCoeff_ne_zero_iff
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
⊢ m.degree f ∈ f.support ↔ f ≠ 0

Tactic:
mem_support_iff.trans coeff_degree_ne_zero_iff

Premises used: MvPolynomial.mem_support_iff, Iff.trans, MonomialOrder.coeff_degree_ne_zero_iff
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
⊢ coeff (m.degree f) f = 0 ↔ f = 0

Tactic:
m.leadingCoeff_eq_zero_iff

Premises used: MonomialOrder.leadingCoeff_eq_zero_iff, MonomialOrder.leadingCoeff
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
hp : p ≠ 0
rwa : coeff (m.degree p) p ≠ 0
rwa₁ rwa₂ rwa₃ rwa₄ : p ≠ 0
⊢ m.degree p ∈ p.support

Tactic:
rwa [MvPolynomial.mem_support_iff, coeff_degree_ne_zero_iff]

Premises used: MvPolynomial.mem_support_iff, MonomialOrder.coeff_degree_ne_zero_iff
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
rw :
  Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn) ↔
    f.totalDegree = 0
⊢ m.degree f = 0 ↔ f.totalDegree = 0

Tactic:
rw [← m.toSyn.injective.eq_iff]

Premises used: Function.Injective.eq_iff, AddEquiv.injective, MonomialOrder.toSyn
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
rw :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn) ↔
    f.totalDegree = 0
⊢ Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn) ↔
    f.totalDegree = 0

Tactic:
rw [map_zero, ← m.bot_eq_zero, eq_bot_iff, m.bot_eq_zero, ← m.toSyn.map_zero]

Premises used: AddEquiv.map_zero, MonomialOrder.bot_eq_zero, map_zero, eq_bot_iff, MonomialOrder.toSyn
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
rw :
  (∀ c ∈ f.support,
      LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn)) ↔
    f.totalDegree = 0
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn) ↔
    f.totalDegree = 0

Tactic:
rw [degree_le_iff]

Premises used: MonomialOrder.degree_le_iff
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
rw :
  (∀ c ∈ f.support,
      LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn)) ↔
    ∀ m ∈ f.support, ∀ (x : σ), Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
⊢ (∀ c ∈ f.support,
      LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn)) ↔
    f.totalDegree = 0

Tactic:
rw [totalDegree_eq_zero_iff]

Premises used: MvPolynomial.totalDegree_eq_zero_iff
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
h :
  ∀ (a : σ →₀ ℕ),
    a ∈ f.support →
        LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) a : m.syn)
          ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn) ↔
      a ∈ f.support → ∀ (x : σ), Eq (α := ℕ) ((a : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
⊢ (∀ c ∈ f.support,
      LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn)) ↔
    ∀ m ∈ f.support, ∀ (x : σ), Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)

Tactic:
apply forall_congr'

Premises used: forall_congr'
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn) ↔
    ∀ (x : σ), Eq (α := ℕ) ((d : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
⊢ d ∈ f.support →
      LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn) ↔
    d ∈ f.support → ∀ (x : σ), Eq (α := ℕ) ((d : (a : σ) → ℕ) x : ℕ) (0 : ℕ)

Tactic:
apply imp_congr (rfl.to_iff)

Premises used: Eq.to_iff, imp_congr, rfl
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h :
  Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn) (0 : m.syn) ↔
    ∀ (x : σ), Eq (α := ℕ) ((d : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn) ↔
    ∀ (x : σ), Eq (α := ℕ) ((d : (a : σ) → ℕ) x : ℕ) (0 : ℕ)

Tactic:
rw [map_zero, ← m.bot_eq_zero, ← eq_bot_iff, m.bot_eq_zero]

Premises used: MonomialOrder.bot_eq_zero, map_zero, eq_bot_iff
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : d = 0 ↔ ∀ (x : σ), Eq (α := ℕ) ((d : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
⊢ Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn) (0 : m.syn) ↔
    ∀ (x : σ), Eq (α := ℕ) ((d : (a : σ) → ℕ) x : ℕ) (0 : ℕ)

Tactic:
simp only [EmbeddingLike.map_eq_zero_iff]

Premises used: EmbeddingLike.map_eq_zero_iff
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
⊢ d = 0 ↔ ∀ (x : σ), Eq (α := ℕ) ((d : (a : σ) → ℕ) x : ℕ) (0 : ℕ)

Tactic:
Finsupp.ext_iff

Premises used: Finsupp.ext_iff
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
⊢ d = 0 ↔ ∀ (x : σ), Eq (α := ℕ) ((d : (a : σ) → ℕ) x : ℕ) (0 : ℕ)

Tactic:
exact Finsupp.ext_iff

Premises used: Finsupp.ext_iff
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
r : R
rw : totalDegree.{u_2, u_1} (R := R) (σ := σ) ((C : (a : R) → MvPolynomial σ R) r) = 0
rw₁ rw₂ : Eq (α := ℕ) 0 0
⊢ degree.{u_1, u_2, u_3} m (R := R) ((C : (a : R) → MvPolynomial σ R) r) = 0

Tactic:
rw [degree_eq_zero_iff_totalDegree_eq_zero, totalDegree_C]

Premises used: MvPolynomial.totalDegree_C, MonomialOrder.degree_eq_zero_iff_totalDegree_eq_zero
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
c : R
⊢ m.leadingCoeff ((C : (a : R) → MvPolynomial σ R) c) = c

Tactic:
simp [leadingCoeff]

Premises used: MonomialOrder.leadingCoeff
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
hf : m.degree f = 0
a : ∀ (d : σ →₀ ℕ), coeff d f = coeff d ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f))
⊢ f = (C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f)

Tactic:
ext d
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
hf : m.degree f = 0
d : σ →₀ ℕ
a : coeff d f = coeff d ((C : (a : R) → MvPolynomial σ R) (coeff 0 f))
⊢ coeff d f = coeff d ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f))

Tactic:
simp only [leadingCoeff, hf]

Premises used: MonomialOrder.leadingCoeff
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
hf : m.degree f = 0
d : σ →₀ ℕ
pos : ∀ (hd : d = 0), coeff d f = coeff d ((C : (a : R) → MvPolynomial σ R) (coeff 0 f))
neg : ∀ (hd : ¬d = 0), coeff d f = coeff d ((C : (a : R) → MvPolynomial σ R) (coeff 0 f))
⊢ coeff d f = coeff d ((C : (a : R) → MvPolynomial σ R) (coeff 0 f))

Tactic:
by_cases hd : d = 0
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
hf : m.degree f = 0
d : σ →₀ ℕ
hd : d = 0
⊢ coeff d f = coeff d ((C : (a : R) → MvPolynomial σ R) (coeff 0 f))

Tactic:
simp [hd]
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
hf : m.degree f = 0
d : σ →₀ ℕ
hd : ¬d = 0
neg : coeff d f = 0
⊢ coeff d f = coeff d ((C : (a : R) → MvPolynomial σ R) (coeff 0 f))

Tactic:
rw [coeff_C, if_neg (Ne.symm hd)]

Premises used: MvPolynomial.coeff_C, Ne.symm, if_neg
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
hf : m.degree f = 0
d : σ →₀ ℕ
hd : ¬d = 0
neg :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
⊢ coeff d f = 0

Tactic:
apply coeff_eq_zero_of_lt (m := m)

Premises used: MonomialOrder.coeff_eq_zero_of_lt
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
hf : m.degree f = 0
d : σ →₀ ℕ
hd : ¬d = 0
neg : LE.le.{u_3} (α := m.syn) (0 : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn) ∧ ¬d = 0
⊢ LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)

Tactic:
rw [hf, map_zero, lt_iff_le_and_ne, ne_eq, eq_comm, EmbeddingLike.map_eq_zero_iff]

Premises used: lt_iff_le_and_ne, map_zero, eq_comm, ne_eq, EmbeddingLike.map_eq_zero_iff
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
hf : m.degree f = 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ LE.le.{u_3} (α := m.syn) (0 : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn) ∧ ¬d = 0

Tactic:
⟨bot_le, hd⟩

Premises used: And.intro, bot_le
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
hf : m.degree f = 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ LE.le.{u_3} (α := m.syn) (0 : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn) ∧ ¬d = 0

Tactic:
exact ⟨bot_le, hd⟩
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
hf : m.degree f = 0
d : σ →₀ ℕ
pos : ∀ (hd : d = 0), coeff d f = coeff d ((C : (a : R) → MvPolynomial σ R) (coeff 0 f))
neg neg₁ : ∀ (hd : ¬d = 0), coeff d f = coeff d ((C : (a : R) → MvPolynomial σ R) (coeff 0 f))
⊢ coeff d f = coeff d ((C : (a : R) → MvPolynomial σ R) (coeff 0 f))

Tactic:
classical
  by_cases hd : d = 0
  · simp [hd]
  · rw [coeff_C, if_neg (Ne.symm hd)]
    apply coeff_eq_zero_of_lt (m := m)
    rw [hf, map_zero, lt_iff_le_and_ne, ne_eq, eq_comm, EmbeddingLike.map_eq_zero_iff]
    exact ⟨bot_le, hd⟩

Premises used: lt_iff_le_and_ne, MonomialOrder.coeff_eq_zero_of_lt, MvPolynomial.coeff_C, map_zero, eq_comm, ne_eq, EmbeddingLike.map_eq_zero_iff
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
h : f = (C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f)
rw : degree.{u_1, u_2, u_3} m (R := R) ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f)) = 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := σ →₀ ℕ) 0 0
⊢ m.degree f = 0

Tactic:
rw [h, MonomialOrder.degree_C]

Premises used: MonomialOrder.degree_C