awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.Localization
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
M : Submonoid R
S : Type u_3
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
inst_3 : Away r S
⊢ ∀
    (x y :
      HasQuotient.Quotient (MvPolynomial Unit R) (B := Ideal (MvPolynomial Unit R))
        (Ideal.span
          {HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
                ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
              1})),
    (auxHom S r : (a : MvPolynomial Unit R ⧸ Ideal.span {(C : (a : R) → MvPolynomial Unit R) r * X () - 1}) → S)
        (x + y) =
      HAdd.hAdd (α := S) (β := S)
        ((auxHom S r : (a : MvPolynomial Unit R ⧸ Ideal.span {(C : (a : R) → MvPolynomial Unit R) r * X () - 1}) → S)
            x :
          S)
        ((auxHom S r : (a : MvPolynomial Unit R ⧸ Ideal.span {(C : (a : R) → MvPolynomial Unit R) r * X () - 1}) → S)
            y :
          S)

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.Localization
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
M : Submonoid R
S : Type u_3
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
inst_3 : Away r S
⊢ ∀ (r_1 : R),
    Eq.{u_3 + 1} (α := S)
      ((auxHom S r : (a : MvPolynomial Unit R ⧸ Ideal.span {(C : (a : R) → MvPolynomial Unit R) r * X () - 1}) → S)
          ((algebraMap R
                  (HasQuotient.Quotient (MvPolynomial Unit R) (B := Ideal (MvPolynomial Unit R))
                    (Ideal.span
                      {HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
                            ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
                          1})) :
                (a : R) → MvPolynomial Unit R ⧸ Ideal.span {(C : (a : R) → MvPolynomial Unit R) r * X () - 1})
              r_1 :
            HasQuotient.Quotient (MvPolynomial Unit R) (B := Ideal (MvPolynomial Unit R))
              (Ideal.span
                {HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
                      ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
                    1})) :
        S)
      ((algebraMap R S : (a : R) → S) r_1 : S)

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.Localization
Goal:
R : Type u_2
inst : CommRing R
S : Type u_3
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
inst_3 : Away r S
p : MvPolynomial Unit R
⊢ Eq.{u_3 + 1} (α := S)
    ((mvPolynomialQuotientEquiv S r :
          (a : MvPolynomial Unit R ⧸ Ideal.span {(C : (a : R) → MvPolynomial Unit R) r * X () - 1}) → S)
        ((Ideal.Quotient.mk
                (Ideal.span
                  {HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
                        ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
                      1}) :
              (a : MvPolynomial Unit R) →
                MvPolynomial Unit R ⧸ Ideal.span {(C : (a : R) → MvPolynomial Unit R) r * X () - 1})
            p :
          HasQuotient.Quotient (MvPolynomial Unit R) (B := Ideal (MvPolynomial Unit R))
            (Ideal.span
              {HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
                    ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
                  1})) :
      S)
    ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) p : S)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Quotient.liftOn', AddCon.liftOn, Finsupp.sum, MvPolynomial.eval₂, Finset.sum, rfl
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
pos : ∀ (hf : f = 0), (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (MonomialOrder.degree degLex f) = f.totalDegree
neg : ∀ (hf : ¬f = 0), (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (MonomialOrder.degree degLex f) = f.totalDegree
⊢ (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (MonomialOrder.degree degLex f) = f.totalDegree

Tactic:
by_cases hf : f = 0
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
hf : f = 0
⊢ (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (MonomialOrder.degree degLex f) = f.totalDegree

Tactic:
simp [hf]
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
hf : ¬f = 0
neg : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (MonomialOrder.degree degLex f) ≤ f.totalDegree
neg₁ : f.totalDegree ≤ (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (MonomialOrder.degree degLex f)
⊢ (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (MonomialOrder.degree degLex f) = f.totalDegree

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
hf : ¬f = 0
⊢ (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (MonomialOrder.degree degLex f) ≤ f.totalDegree

Tactic:
le_totalDegree (degLex.degree_mem_support hf)

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MonomialOrder.degree_mem_support, MvPolynomial.le_totalDegree, Finset.sum
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
hf : ¬f = 0
⊢ (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (MonomialOrder.degree degLex f) ≤ f.totalDegree

Tactic:
exact le_totalDegree (degLex.degree_mem_support hf)

Premises used: MonomialOrder.degree_mem_support, MvPolynomial.le_totalDegree
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
hf : ¬f = 0
neg :
  ∀ b ∈ f.support,
    LE.le (α := ℕ) (b.sum fun (x : σ) (e : ℕ) ↦ e : ℕ)
      ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (MonomialOrder.degree degLex f) : ℕ)
⊢ LE.le (α := ℕ) (f.support.sup fun (s : σ →₀ ℕ) ↦ s.sum fun (x : σ) (e : ℕ) ↦ e : ℕ)
    ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (MonomialOrder.degree degLex f) : ℕ)

Tactic:
apply Finset.sup_le

Premises used: Finset.sup_le
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
hf : ¬f = 0
b : σ →₀ ℕ
hb : b ∈ f.support
⊢ LE.le (α := ℕ) (b.sum fun (x : σ) (e : ℕ) ↦ e : ℕ)
    ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (MonomialOrder.degree degLex f) : ℕ)

Tactic:
DegLex.monotone_degree (degLex.le_degree hb)

Premises used: Multiset.sum, Multiset.foldr, MonomialOrder.le_degree, Finsupp.sum, Finsupp.DegLex.monotone_degree, Finset.sum
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
hf : ¬f = 0
b : σ →₀ ℕ
hb : b ∈ f.support
⊢ LE.le (α := ℕ) (b.sum fun (x : σ) (e : ℕ) ↦ e : ℕ)
    ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (MonomialOrder.degree degLex f) : ℕ)

Tactic:
exact DegLex.monotone_degree (degLex.le_degree hb)

Premises used: MonomialOrder.le_degree, Finsupp.DegLex.monotone_degree
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
h :
  LE.le (α := syn (σ := σ) degLex)
    ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn) (MonomialOrder.degree degLex f) : syn (σ := σ) degLex)
    ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn) (MonomialOrder.degree degLex g) : syn (σ := σ) degLex)
simp :
  LE.le (α := ℕ) ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (MonomialOrder.degree degLex f) : ℕ)
    ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (MonomialOrder.degree degLex g) : ℕ)
⊢ f.totalDegree ≤ g.totalDegree

Tactic:
simp only [← MvPolynomial.degree_degLexDegree]

Premises used: MvPolynomial.degree_degLexDegree
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
h :
  LE.le (α := syn (σ := σ) degLex)
    ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn) (MonomialOrder.degree degLex f) : syn (σ := σ) degLex)
    ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn) (MonomialOrder.degree degLex g) : syn (σ := σ) degLex)
⊢ LE.le (α := ℕ) ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (MonomialOrder.degree degLex f) : ℕ)
    ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (MonomialOrder.degree degLex g) : ℕ)

Tactic:
DegLex.monotone_degree h

Premises used: Finsupp.DegLex.monotone_degree
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
h :
  LE.le (α := syn (σ := σ) degLex)
    ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn) (MonomialOrder.degree degLex f) : syn (σ := σ) degLex)
    ((toSyn degLex : (a : σ →₀ ℕ) → degLex.syn) (MonomialOrder.degree degLex g) : syn (σ := σ) degLex)
⊢ LE.le (α := ℕ) ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (MonomialOrder.degree degLex f) : ℕ)
    ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (MonomialOrder.degree degLex g) : ℕ)

Tactic:
exact DegLex.monotone_degree h

Premises used: Finsupp.DegLex.monotone_degree
-- 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
rw : (monomial (m.degree p) : (a : R) → MvPolynomial σ R) (m.leadingCoeff p * 1) = m.leadingTerm p
rw₁ : (monomial (m.degree p) : (a : R) → MvPolynomial σ R) (m.leadingCoeff p) = m.leadingTerm p
rw₂ rw₃ :
  Eq (α := MvPolynomial σ R)
    ((monomial (m.degree p) : (a : R) → MvPolynomial σ R) (m.leadingCoeff p) : MvPolynomial σ R)
    ((monomial (m.degree p) : (a : R) → MvPolynomial σ R) (m.leadingCoeff p) : MvPolynomial σ R)
⊢ HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff p) : MvPolynomial σ R)
      ((monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R) =
    m.leadingTerm p

Tactic:
rw [MvPolynomial.C_mul_monomial, mul_one, leadingTerm]

Premises used: MvPolynomial.C_mul_monomial, MonomialOrder.leadingTerm, mul_one
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
inst_1 : Subsingleton R
f : MvPolynomial σ R
⊢ m.Monic f

Tactic:
Subsingleton.eq_one (m.leadingCoeff f)

Premises used: MonomialOrder.Monic, MonomialOrder.leadingCoeff, Subsingleton.eq_one
-- 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.Monic f
⊢ m.leadingCoeff f = 1

Tactic:
hf

Premises used: MonomialOrder.Monic
-- 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.Monic f
⊢ coeff (m.degree f) f = 1

Tactic:
hf

Premises used: MonomialOrder.Monic, MonomialOrder.leadingCoeff
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
⊢ degree.{u_1, u_2, u_3} m (R := R) 0 = 0

Tactic:
simp [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
h : degree.{u_1, u_2, u_3} m (R := R) 0 ≠ 0
⊢ False

Tactic:
h m.degree_zero

Premises used: MonomialOrder.degree_zero
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
h : degree.{u_1, u_2, u_3} m (R := R) 0 ≠ 0
⊢ False

Tactic:
exact h m.degree_zero

Premises used: MonomialOrder.degree_zero
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
inst_1 : Subsingleton R
f : MvPolynomial σ R
rw : degree.{u_1, u_2, u_3} m (R := R) 0 = 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := σ →₀ ℕ) 0 0
⊢ m.degree f = 0

Tactic:
rw [Subsingleton.eq_zero f, degree_zero]

Premises used: MonomialOrder.degree_zero, Subsingleton.eq_zero
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
⊢ Eq.{u_2 + 1} (α := R) (m.leadingCoeff 0) 0

Tactic:
simp [degree, leadingCoeff]

Premises used: 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
inst_1 : Nontrivial R
hf : Monic.{u_1, u_2, u_3} m (R := R) 0
⊢ False

Tactic:
simp [Monic, leadingCoeff_zero] at hf

Premises used: MonomialOrder.Monic, 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
d : σ →₀ ℕ
c : R
simp :
  LE.le.{u_3} (α := m.syn)
    (Finset.sup.{u_3, u_1} (β := σ →₀ ℕ) (support.{u_2, u_1} (R := R) ((monomial d : (a : R) → MvPolynomial σ R) c))
        (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn) :
      m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
⊢ LE.le.{u_3} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
        (degree.{u_1, u_2, u_3} m (R := R) ((monomial d : (a : R) → MvPolynomial σ R) c)) :
      m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)

Tactic:
simp only [degree, AddEquiv.apply_symm_apply]

Premises used: AddEquiv.apply_symm_apply, MonomialOrder.degree
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
d : σ →₀ ℕ
c : R
apply :
  LE.le.{u_3} (α := m.syn) (Finset.sup (β := σ →₀ ℕ) {d} (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
⊢ LE.le.{u_3} (α := m.syn)
    (Finset.sup.{u_3, u_1} (β := σ →₀ ℕ) (support.{u_2, u_1} (R := R) ((monomial d : (a : R) → MvPolynomial σ R) c))
        (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn) :
      m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)

Tactic:
apply le_trans (Finset.sup_mono support_monomial_subset)

Premises used: MvPolynomial.support_monomial_subset, Finset.sup_mono, le_trans
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
d : σ →₀ ℕ
c : R
⊢ LE.le.{u_3} (α := m.syn) (Finset.sup (β := σ →₀ ℕ) {d} (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)

Tactic:
simp only [Finset.sup_singleton, le_refl]

Premises used: le_refl, Finset.sup_singleton
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
d : σ →₀ ℕ
c : R
inst_1 : Decidable (c = 0)
simp :
  (m.toSyn.symm : (a : m.syn) → σ →₀ ℕ)
      (Finset.sup (β := σ →₀ ℕ) (if c = 0 then ∅ else {d}) (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn)) =
    if c = 0 then 0 else d
⊢ degree.{u_1, u_2, u_3} m (R := R) ((monomial d : (a : R) → MvPolynomial σ R) c) = if c = 0 then 0 else d

Tactic:
simp only [degree, support_monomial]

Premises used: MvPolynomial.support_monomial, MonomialOrder.degree
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
d : σ →₀ ℕ
c : R
inst_1 : Decidable (c = 0)
pos :
  ∀ (hc : c = 0),
    Eq.{u_1 + 1} (α := σ →₀ ℕ)
      ((m.toSyn.symm : (a : m.syn) → σ →₀ ℕ) (Finset.sup.{u_3, u_1} (β := σ →₀ ℕ) ∅ (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn)))
      0
neg :
  ∀ (hc : ¬c = 0),
    (m.toSyn.symm : (a : m.syn) → σ →₀ ℕ) (Finset.sup (β := σ →₀ ℕ) {d} (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn)) = d
⊢ (m.toSyn.symm : (a : m.syn) → σ →₀ ℕ)
      (Finset.sup (β := σ →₀ ℕ) (if c = 0 then ∅ else {d}) (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn)) =
    if c = 0 then 0 else d

Tactic:
split_ifs with hc
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
d : σ →₀ ℕ
c : R
inst_1 : Decidable (c = 0)
hc : c = 0
⊢ Eq.{u_1 + 1} (α := σ →₀ ℕ)
    ((m.toSyn.symm : (a : m.syn) → σ →₀ ℕ) (Finset.sup.{u_3, u_1} (β := σ →₀ ℕ) ∅ (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn))) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
d : σ →₀ ℕ
c : R
inst_1 : Decidable (c = 0)
hc : ¬c = 0
⊢ (m.toSyn.symm : (a : m.syn) → σ →₀ ℕ) (Finset.sup (β := σ →₀ ℕ) {d} (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn)) = d

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
s : σ
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_3} m (R := R) (X s)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (Finsupp.single s 1) : m.syn)

Tactic:
degree_monomial_le 1

Premises used: MvPolynomial.X, MonomialOrder.degree_monomial_le, OfNat.ofNat
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
inst_1 : Nontrivial R
s : σ
rw : Eq (α := σ →₀ ℕ) (if Eq.{u_2 + 1} (α := R) 1 0 then 0 else Finsupp.single s 1) (Finsupp.single s 1)
rw₁ rw₂ : Eq (α := σ →₀ ℕ) (Finsupp.single s 1) (Finsupp.single s 1)
⊢ degree.{u_1, u_2, u_3} m (R := R) ((monomial (Finsupp.single s 1) : (a : R) → MvPolynomial σ R) 1) =
    Finsupp.single s 1

Tactic:
rw [degree_monomial, if_neg one_ne_zero]

Premises used: MonomialOrder.degree_monomial, one_ne_zero, if_neg
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
d : σ →₀ ℕ
c : R
simp : coeff (if c = 0 then 0 else d) ((monomial d : (a : R) → MvPolynomial σ R) c) = c
⊢ m.leadingCoeff ((monomial d : (a : R) → MvPolynomial σ R) c) = c

Tactic:
simp only [leadingCoeff, degree_monomial]

Premises used: MonomialOrder.degree_monomial, MonomialOrder.leadingCoeff
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
d : σ →₀ ℕ
c : R
pos : ∀ (hc : c = 0), coeff.{u_2, u_1} (σ := σ) 0 ((monomial d : (a : R) → MvPolynomial σ R) c) = c
neg : ∀ (hc : ¬c = 0), coeff d ((monomial d : (a : R) → MvPolynomial σ R) c) = c
⊢ coeff (if c = 0 then 0 else d) ((monomial d : (a : R) → MvPolynomial σ R) c) = c

Tactic:
split_ifs with hc
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
d : σ →₀ ℕ
c : R
hc : c = 0
⊢ coeff.{u_2, u_1} (σ := σ) 0 ((monomial d : (a : R) → MvPolynomial σ R) c) = c

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

Tactic:
simp [hc]
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
d : σ →₀ ℕ
c : R
simp : coeff (if c = 0 then 0 else d) ((monomial d : (a : R) → MvPolynomial σ R) c) = c
⊢ m.leadingCoeff ((monomial d : (a : R) → MvPolynomial σ R) c) = c

Tactic:
classical
  simp only [leadingCoeff, degree_monomial]
  split_ifs with hc <;> simp [hc]

Premises used: MonomialOrder.degree_monomial, MonomialOrder.leadingCoeff
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
d : σ →₀ ℕ
⊢ Monic.{u_1, u_2, u_3} m (R := R) ((monomial d : (a : R) → MvPolynomial σ R) 1)

Tactic:
m.leadingCoeff_monomial 1

Premises used: MonomialOrder.Monic, MonomialOrder.leadingCoeff_monomial, OfNat.ofNat
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
d : σ →₀ ℕ
c : R
rw : Eq.{u_2 + 1} (α := R) (m.leadingCoeff ((monomial d : (a : R) → MvPolynomial σ R) c)) 1 ↔ c = 1
rw₁ rw₂ : c = 1 ↔ c = 1
⊢ Monic.{u_1, u_2, u_3} m (R := R) ((monomial d : (a : R) → MvPolynomial σ R) c) ↔ c = 1

Tactic:
rw [Monic, m.leadingCoeff_monomial]

Premises used: MonomialOrder.Monic, MonomialOrder.leadingCoeff_monomial
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
s : σ
⊢ Eq.{u_2 + 1} (α := R) (m.leadingCoeff (X s)) 1

Tactic:
m.leadingCoeff_monomial 1

Premises used: MvPolynomial.X, MonomialOrder.leadingCoeff_monomial, OfNat.ofNat
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
s : σ
⊢ Monic.{u_1, u_2, u_3} m (R := R) (X s)

Tactic:
monic_monomial_one

Premises used: MvPolynomial.X, MonomialOrder.monic_monomial_one
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
⊢ Eq.{u_2 + 1} (α := R) (m.leadingCoeff 1) 1

Tactic:
m.leadingCoeff_monomial 1

Premises used: MonomialOrder.leadingCoeff_monomial, OfNat.ofNat, Finsupp.single
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
⊢ Monic.{u_1, u_2, u_3} m (R := R) ((C : (a : R) → MvPolynomial σ R) 1)

Tactic:
monic_monomial_one

Premises used: MonomialOrder.monic_monomial_one, Finsupp.single
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
⊢ Monic.{u_1, u_2, u_3} m (R := R) 1

Tactic:
monic_monomial_one

Premises used: MonomialOrder.monic_monomial_one, Finsupp.single
-- 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 : σ →₀ ℕ
unfold :
  LE.le.{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,
      LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
⊢ LE.le.{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,
      LE.le.{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 : σ →₀ ℕ
⊢ LE.le.{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,
      LE.le.{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, Finset.sup_le_iff, mem_support_iff, ne_eq]

Premises used: MvPolynomial.mem_support_iff, ne_eq, AddEquiv.apply_symm_apply, Finset.sup_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
d : σ →₀ ℕ
hd : LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
⊢ LT.lt.{u_3} (α := m.syn) (0 : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)

Tactic:
simp only [map_zero] at hd

Premises used: map_zero