awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Localization (goal)
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
g : 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}) :=
  RingHom.comp
    (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}))
    C
⊢ IsUnit (M :=
    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}))
    ((g : (a : R) → MvPolynomial Unit R ⧸ Ideal.span {(C : (a : R) → MvPolynomial Unit R) r * X () - 1}) 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}))
have simp : IsUnit (M :=
  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}))
  ((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})
      ((C : (a : R) → MvPolynomial Unit R) 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}))
Tactic: simp only [RingHom.coe_comp, Function.comp_apply, g]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Localization (goal)
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
g : 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}) :=
  RingHom.comp
    (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}))
    C
⊢ IsUnit (M :=
    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}))
    ((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})
        ((C : (a : R) → MvPolynomial Unit R) 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}))
have rw : ∃ (b :
  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})),
  HMul.hMul (α :=
      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}))
      ((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})
          ((C : (a : R) → MvPolynomial Unit R) 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}))
      b =
    1
Tactic: rw [isUnit_iff_exists_inv]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Localization (goal)
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
⊢ Eq (α := S →+* S)
    (RingHom.comp (β :=
      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}))
      (AlgHom.toRingHom (auxHom S r)) (auxInv S r))
    (RingHom.id S)
have h : Eq (α := R →+* S)
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
    (RingHom.comp (β :=
      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}))
      (AlgHom.toRingHom (auxHom S r)) (auxInv S r))
    (algebraMap R S))
  (RingHom.comp (RingHom.id S) (algebraMap R S))
Tactic: apply IsLocalization.ringHom_ext (Submonoid.powers r)
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Localization (goal)
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
⊢ Eq (α := R →+* S)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (RingHom.comp (β :=
        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}))
        (AlgHom.toRingHom (auxHom S r)) (auxInv S r))
      (algebraMap R S))
    (RingHom.comp (RingHom.id S) (algebraMap R S))
have h : ∀ (x : R),
  Eq.{u_3 + 1} (α := S)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (RingHom.comp (β :=
              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}))
              (AlgHom.toRingHom (auxHom S r)) (auxInv S r))
            (algebraMap R S) :
          (a : R) → S)
        x :
      S)
    ((RingHom.comp (RingHom.id S) (algebraMap R S) : (a : R) → S) x : S)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Localization (goal)
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
⊢ Eq (α :=
    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}) →+*
      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}))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (auxInv S r) (AlgHom.toRingHom (auxHom S r)))
    (RingHom.id
      (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})))
have rw : Eq (α :=
  MvPolynomial Unit 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}))
  (RingHom.comp (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (auxInv S r) (AlgHom.toRingHom (auxHom S r)))
    (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})))
  (RingHom.comp
    (RingHom.id
      (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})))
    (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})))
Tactic: rw [← RingHom.cancel_right (Ideal.Quotient.mk_surjective)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Localization (goal)
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
x : Unit
⊢ 1 =
    HMul.hMul (α :=
      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}))
      (β :=
      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}))
      ((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})
          ((C : (a : R) → MvPolynomial Unit R) 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}))
      ((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})
          (X x) :
        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}))
have hX : Membership.mem (γ := 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})
  (HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
      ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X x) -
    1)
Tactic: rw [← map_one (Ideal.Quotient.mk _), ← map_mul, Ideal.Quotient.mk_eq_mk_iff_sub_mem,
      ← Ideal.neg_mem_iff, neg_sub]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
⊢ (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (MonomialOrder.degree degLex f) = f.totalDegree
have pos : ∀ (hf : f = 0), (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (MonomialOrder.degree degLex f) = f.totalDegree
Tactic: by_cases hf : f = 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex (goal)
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
⊢ (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (MonomialOrder.degree degLex f) = f.totalDegree
have neg : ∀ (hf : ¬f = 0), (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (MonomialOrder.degree degLex f) = f.totalDegree
Tactic: by_cases hf : f = 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex (goal)
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
have neg : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (MonomialOrder.degree degLex f) ≤ f.totalDegree
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex (goal)
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
⊢ (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (MonomialOrder.degree degLex f) = f.totalDegree
have neg₁ : f.totalDegree ≤ (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (MonomialOrder.degree degLex f)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
hf : ¬f = 0
⊢ LE.le (α := ℕ) (f.support.sup fun (s : σ →₀ ℕ) ↦ s.sum fun (x : σ) (e : ℕ) ↦ e : ℕ)
    ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (MonomialOrder.degree degLex f) : ℕ)
have neg : ∀ b ∈ f.support,
  LE.le (α := ℕ) (b.sum fun (x : σ) (e : ℕ) ↦ e : ℕ)
    ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (MonomialOrder.degree degLex f) : ℕ)
Tactic: apply Finset.sup_le
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex (goal)
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)
⊢ f.totalDegree ≤ g.totalDegree
have simp : LE.le (α := ℕ) ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (MonomialOrder.degree degLex f) : ℕ)
  ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (MonomialOrder.degree degLex g) : ℕ)
Tactic: simp only [← MvPolynomial.degree_degLexDegree]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
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
have rw : (monomial (m.degree p) : (a : R) → MvPolynomial σ R) (m.leadingCoeff p * 1) = m.leadingTerm p
Tactic: rw [MvPolynomial.C_mul_monomial, mul_one, leadingTerm]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
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
⊢ 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
have rw₁ : (monomial (m.degree p) : (a : R) → MvPolynomial σ R) (m.leadingCoeff p) = m.leadingTerm p
Tactic: rw [MvPolynomial.C_mul_monomial, mul_one, leadingTerm]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
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
⊢ 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
have 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)
Tactic: rw [MvPolynomial.C_mul_monomial, mul_one, leadingTerm]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
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.degree f = 0
have rw : degree.{u_1, u_2, u_3} m (R := R) 0 = 0
Tactic: rw [Subsingleton.eq_zero f, degree_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
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
⊢ m.degree f = 0
have rw₁ : Eq.{u_1 + 1} (α := σ →₀ ℕ) 0 0
Tactic: rw [Subsingleton.eq_zero f, degree_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
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)
    ((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)
have 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)
Tactic: simp only [degree, AddEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
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.{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)
have 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)
Tactic: apply le_trans (Finset.sup_mono support_monomial_subset)
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
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)
⊢ degree.{u_1, u_2, u_3} m (R := R) ((monomial d : (a : R) → MvPolynomial σ R) c) = if c = 0 then 0 else d
have 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
Tactic: simp only [degree, support_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
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)
⊢ (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
have 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
Tactic: split_ifs with hc
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
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
⊢ (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
have neg : ∀ (hc : ¬c = 0),
  (m.toSyn.symm : (a : m.syn) → σ →₀ ℕ) (Finset.sup (β := σ →₀ ℕ) {d} (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn)) = d
Tactic: split_ifs with hc
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
inst_1 : Nontrivial R
s : σ
⊢ degree.{u_1, u_2, u_3} m (R := R) ((monomial (Finsupp.single s 1) : (a : R) → MvPolynomial σ R) 1) =
    Finsupp.single s 1
have rw : Eq (α := σ →₀ ℕ) (if Eq.{u_2 + 1} (α := R) 1 0 then 0 else Finsupp.single s 1) (Finsupp.single s 1)
Tactic: rw [degree_monomial, if_neg one_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
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)
⊢ degree.{u_1, u_2, u_3} m (R := R) ((monomial (Finsupp.single s 1) : (a : R) → MvPolynomial σ R) 1) =
    Finsupp.single s 1
have rw₁ : Eq (α := σ →₀ ℕ) (Finsupp.single s 1) (Finsupp.single s 1)
Tactic: rw [degree_monomial, if_neg one_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
d : σ →₀ ℕ
c : R
⊢ m.leadingCoeff ((monomial d : (a : R) → MvPolynomial σ R) c) = c
have simp : coeff (if c = 0 then 0 else d) ((monomial d : (a : R) → MvPolynomial σ R) c) = c
Tactic: simp only [leadingCoeff, degree_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
d : σ →₀ ℕ
c : R
⊢ coeff (if c = 0 then 0 else d) ((monomial d : (a : R) → MvPolynomial σ R) c) = c
have pos : ∀ (hc : c = 0), coeff.{u_2, u_1} (σ := σ) 0 ((monomial d : (a : R) → MvPolynomial σ R) c) = c
Tactic: split_ifs with hc