awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.FreeCommRing
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst : DecidableEq κ
inst_1 : CommRing R
inst_2 : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × ↥(monoms i) ⊕ κ → R
i : ι
⊢ Eq.{u_3 + 1} (α := R)
    (∑ x ∈ (monoms i).attach,
      HMul.hMul (β := R) (f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i x)))
        ((((lift : (a : (i : ι) × ↥(monoms i) ⊕ κ → R) → FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ) →+* R) f :
                FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ) →+* R) :
              (a : FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ)) → R)
            ((↑x : κ →₀ ℕ).prod fun (j : κ) (n : ℕ) ↦
              HPow.hPow (α := FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ)) (of (Sum.inr j)) n) :
          R))
    (∑ x ∈ (monoms i).attach,
      if
          ∃ (h : (↑x : κ →₀ ℕ) ∈ monoms i),
            ¬f
                  (Sum.inl
                    (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                      (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) (↑x : κ →₀ ℕ) ⋯))) =
                0 then
        HMul.hMul (α := R)
          (if h : (↑x : κ →₀ ℕ) ∈ monoms i then
            f
              (Sum.inl
                (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                  (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) (↑x : κ →₀ ℕ) ⋯)))
          else 0)
          (∏ x_1 ∈ (↑x : κ →₀ ℕ).support, HPow.hPow (β := ℕ) (f (Sum.inr x_1)) (((↑x : κ →₀ ℕ) : (a : κ) → ℕ) x_1 : ℕ))
      else 0)

Tactic:
Finset.sum_congr rfl ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.MvPolynomial.FreeCommRing
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst : DecidableEq κ
inst_1 : CommRing R
inst_2 : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × ↥(monoms i) ⊕ κ → R
i : ι
refine :
  ∀ x ∈ (monoms i).attach,
    HMul.hMul (β := R) (f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i x)))
        ((((lift : (a : (i : ι) × ↥(monoms i) ⊕ κ → R) → FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ) →+* R) f :
                FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ) →+* R) :
              (a : FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ)) → R)
            ((↑x : κ →₀ ℕ).prod fun (j : κ) (n : ℕ) ↦
              HPow.hPow (α := FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ)) (of (Sum.inr j)) n) :
          R) =
      if
          ∃ (h : (↑x : κ →₀ ℕ) ∈ monoms i),
            ¬f
                  (Sum.inl
                    (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                      (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) (↑x : κ →₀ ℕ) ⋯))) =
                0 then
        HMul.hMul (α := R)
          (if h : (↑x : κ →₀ ℕ) ∈ monoms i then
            f
              (Sum.inl
                (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                  (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) (↑x : κ →₀ ℕ) ⋯)))
          else 0)
          (∏ x_1 ∈ (↑x : κ →₀ ℕ).support, HPow.hPow (β := ℕ) (f (Sum.inr x_1)) (((↑x : κ →₀ ℕ) : (a : κ) → ℕ) x_1 : ℕ))
      else 0
⊢ Eq.{u_3 + 1} (α := R)
    (∑ x ∈ (monoms i).attach,
      HMul.hMul (β := R) (f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i x)))
        ((((lift : (a : (i : ι) × ↥(monoms i) ⊕ κ → R) → FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ) →+* R) f :
                FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ) →+* R) :
              (a : FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ)) → R)
            ((↑x : κ →₀ ℕ).prod fun (j : κ) (n : ℕ) ↦
              HPow.hPow (α := FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ)) (of (Sum.inr j)) n) :
          R))
    (∑ x ∈ (monoms i).attach,
      if
          ∃ (h : (↑x : κ →₀ ℕ) ∈ monoms i),
            ¬f
                  (Sum.inl
                    (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                      (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) (↑x : κ →₀ ℕ) ⋯))) =
                0 then
        HMul.hMul (α := R)
          (if h : (↑x : κ →₀ ℕ) ∈ monoms i then
            f
              (Sum.inl
                (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                  (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) (↑x : κ →₀ ℕ) ⋯)))
          else 0)
          (∏ x_1 ∈ (↑x : κ →₀ ℕ).support, HPow.hPow (β := ℕ) (f (Sum.inr x_1)) (((↑x : κ →₀ ℕ) : (a : κ) → ℕ) x_1 : ℕ))
      else 0)

Tactic:
refine Finset.sum_congr rfl ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.MvPolynomial.FreeCommRing
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst : DecidableEq κ
inst_1 : CommRing R
inst_2 : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × ↥(monoms i) ⊕ κ → R
i : ι
m : ↥(monoms i)
_ :
  m ∈ (monoms i).attach →
    HMul.hMul (β := R) (f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i m)))
        ((((lift : (a : (i : ι) × ↥(monoms i) ⊕ κ → R) → FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ) →+* R) f :
                FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ) →+* R) :
              (a : FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ)) → R)
            ((↑m : κ →₀ ℕ).prod fun (j : κ) (n : ℕ) ↦
              HPow.hPow (α := FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ)) (of (Sum.inr j)) n) :
          R) =
      if
          ∃ (h : (↑m : κ →₀ ℕ) ∈ monoms i),
            ¬f
                  (Sum.inl
                    (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                      (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) (↑m : κ →₀ ℕ) ⋯))) =
                0 then
        HMul.hMul (α := R)
          (if h : (↑m : κ →₀ ℕ) ∈ monoms i then
            f
              (Sum.inl
                (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                  (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) (↑m : κ →₀ ℕ) ⋯)))
          else 0)
          (∏ x ∈ (↑m : κ →₀ ℕ).support, HPow.hPow (β := ℕ) (f (Sum.inr x)) (((↑m : κ →₀ ℕ) : (a : κ) → ℕ) x : ℕ))
      else 0
⊢ m ∈ (monoms i).attach →
    HMul.hMul (β := R) (f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i m)))
        ((((lift : (a : (i : ι) × ↥(monoms i) ⊕ κ → R) → FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ) →+* R) f :
                FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ) →+* R) :
              (a : FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ)) → R)
            ((↑m : κ →₀ ℕ).prod fun (j : κ) (n : ℕ) ↦
              HPow.hPow (α := FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ)) (of (Sum.inr j)) n) :
          R) =
      if
          ∃ (h : (↑m : κ →₀ ℕ) ∈ monoms i),
            ¬f
                  (Sum.inl
                    (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                      (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) (↑m : κ →₀ ℕ) ⋯))) =
                0 then
        HMul.hMul (α := R)
          (if h : (↑m : κ →₀ ℕ) ∈ monoms i then
            f
              (Sum.inl
                (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                  (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) (↑m : κ →₀ ℕ) ⋯)))
          else 0)
          (∏ x ∈ (↑m : κ →₀ ℕ).support, HPow.hPow (β := ℕ) (f (Sum.inr x)) (((↑m : κ →₀ ℕ) : (a : κ) → ℕ) x : ℕ))
      else 0

Tactic:
_
-- Module: Mathlib.RingTheory.MvPolynomial.FreeCommRing
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst : DecidableEq κ
inst_1 : CommRing R
inst_2 : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × ↥(monoms i) ⊕ κ → R
i : ι
m : ↥(monoms i)
h : m ∈ (monoms i).attach
simp :
  f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i m)) *
      ∏ x ∈ (↑m : κ →₀ ℕ).support, HPow.hPow (β := ℕ) (f (Sum.inr x)) (((↑m : κ →₀ ℕ) : (a : κ) → ℕ) x : ℕ) =
    if f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i m)) = 0 then 0
    else
      f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i m)) *
        ∏ x ∈ (↑m : κ →₀ ℕ).support, HPow.hPow (β := ℕ) (f (Sum.inr x)) (((↑m : κ →₀ ℕ) : (a : κ) → ℕ) x : ℕ)
⊢ HMul.hMul (β := R) (f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i m)))
      ((((lift : (a : (i : ι) × ↥(monoms i) ⊕ κ → R) → FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ) →+* R) f :
              FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ) →+* R) :
            (a : FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ)) → R)
          ((↑m : κ →₀ ℕ).prod fun (j : κ) (n : ℕ) ↦
            HPow.hPow (α := FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ)) (of (Sum.inr j)) n) :
        R) =
    if
        ∃ (h : (↑m : κ →₀ ℕ) ∈ monoms i),
          ¬f
                (Sum.inl
                  (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                    (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) (↑m : κ →₀ ℕ) ⋯))) =
              0 then
      HMul.hMul (α := R)
        (if h : (↑m : κ →₀ ℕ) ∈ monoms i then
          f
            (Sum.inl
              (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) (↑m : κ →₀ ℕ) ⋯)))
        else 0)
        (∏ x ∈ (↑m : κ →₀ ℕ).support, HPow.hPow (β := ℕ) (f (Sum.inr x)) (((↑m : κ →₀ ℕ) : (a : κ) → ℕ) x : ℕ))
    else 0

Tactic:
simp only [Finsupp.prod, map_prod, map_pow, lift_of, Subtype.coe_eta, Finset.coe_mem,
    exists_prop, true_and, dite_eq_ite, ite_true, ite_not]

Premises used: FreeCommRing.lift_of, Finset.coe_mem, ite_true, map_pow, exists_prop, map_prod, Subtype.coe_eta, ite_not, dite_eq_ite, Finsupp.prod, true_and
-- Module: Mathlib.RingTheory.MvPolynomial.FreeCommRing
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst : DecidableEq κ
inst_1 : CommRing R
inst_2 : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × ↥(monoms i) ⊕ κ → R
i : ι
m : ↥(monoms i)
h : m ∈ (monoms i).attach
pos :
  ∀ (h0 : f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i m)) = 0),
    f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i m)) *
        ∏ x ∈ (↑m : κ →₀ ℕ).support, HPow.hPow (β := ℕ) (f (Sum.inr x)) (((↑m : κ →₀ ℕ) : (a : κ) → ℕ) x : ℕ) =
      0
neg :
  ∀ (h0 : ¬f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i m)) = 0),
    f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i m)) *
        ∏ x ∈ (↑m : κ →₀ ℕ).support, HPow.hPow (β := ℕ) (f (Sum.inr x)) (((↑m : κ →₀ ℕ) : (a : κ) → ℕ) x : ℕ) =
      f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i m)) *
        ∏ x ∈ (↑m : κ →₀ ℕ).support, HPow.hPow (β := ℕ) (f (Sum.inr x)) (((↑m : κ →₀ ℕ) : (a : κ) → ℕ) x : ℕ)
⊢ f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i m)) *
      ∏ x ∈ (↑m : κ →₀ ℕ).support, HPow.hPow (β := ℕ) (f (Sum.inr x)) (((↑m : κ →₀ ℕ) : (a : κ) → ℕ) x : ℕ) =
    if f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i m)) = 0 then 0
    else
      f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i m)) *
        ∏ x ∈ (↑m : κ →₀ ℕ).support, HPow.hPow (β := ℕ) (f (Sum.inr x)) (((↑m : κ →₀ ℕ) : (a : κ) → ℕ) x : ℕ)

Tactic:
split_ifs with h0
-- Module: Mathlib.RingTheory.MvPolynomial.FreeCommRing
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst : DecidableEq κ
inst_1 : CommRing R
inst_2 : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × ↥(monoms i) ⊕ κ → R
i : ι
m : ↥(monoms i)
h : m ∈ (monoms i).attach
h0 : f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i m)) = 0
⊢ f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i m)) *
      ∏ x ∈ (↑m : κ →₀ ℕ).support, HPow.hPow (β := ℕ) (f (Sum.inr x)) (((↑m : κ →₀ ℕ) : (a : κ) → ℕ) x : ℕ) =
    0

Tactic:
simp_all
-- Module: Mathlib.RingTheory.MvPolynomial.FreeCommRing
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst : DecidableEq κ
inst_1 : CommRing R
inst_2 : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × ↥(monoms i) ⊕ κ → R
i : ι
m : ↥(monoms i)
h : m ∈ (monoms i).attach
h0 : ¬f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i m)) = 0
⊢ f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i m)) *
      ∏ x ∈ (↑m : κ →₀ ℕ).support, HPow.hPow (β := ℕ) (f (Sum.inr x)) (((↑m : κ →₀ ℕ) : (a : κ) → ℕ) x : ℕ) =
    f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i m)) *
      ∏ x ∈ (↑m : κ →₀ ℕ).support, HPow.hPow (β := ℕ) (f (Sum.inr x)) (((↑m : κ →₀ ℕ) : (a : κ) → ℕ) x : ℕ)

Tactic:
simp_all
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
apply :
  LE.le.{u_3} (α := m.syn)
    (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f))
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
          (degree.{u_1, u_2, u_3} m (R := R)
            ((monomial (m.degree f) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f)))) :
      m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.subLTerm f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)

Tactic:
apply le_trans degree_sub_le

Premises used: MonomialOrder.degree_sub_le, le_trans
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
simp :
  LE.le.{u_3} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
        (degree.{u_1, u_2, u_3} m (R := R) ((monomial (m.degree f) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f))) :
      m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
⊢ LE.le.{u_3} (α := m.syn)
    (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f))
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
          (degree.{u_1, u_2, u_3} m (R := R)
            ((monomial (m.degree f) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f)))) :
      m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)

Tactic:
simp only [sup_le_iff, le_refl, true_and]

Premises used: le_refl, sup_le_iff, true_and
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
⊢ LE.le.{u_3} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
        (degree.{u_1, u_2, u_3} m (R := R) ((monomial (m.degree f) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f))) :
      m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)

Tactic:
apply degree_monomial_le

Premises used: MonomialOrder.degree_monomial_le
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
rw :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.subLTerm f)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn) ∧
    Ne.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.subLTerm f)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
⊢ LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.subLTerm f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)

Tactic:
rw [lt_iff_le_and_ne]

Premises used: lt_iff_le_and_ne
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.subLTerm f)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn) ∧
    Ne.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.subLTerm f)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)

Tactic:
⟨degree_sub_LTerm_le f, ?_⟩

Premises used: And.intro, MonomialOrder.degree_sub_LTerm_le
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
refine :
  Ne.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.subLTerm f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.subLTerm f)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn) ∧
    Ne.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.subLTerm f)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)

Tactic:
refine ⟨degree_sub_LTerm_le f, ?_⟩
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
hf' :
  Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.subLTerm f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
⊢ m.degree (m.subLTerm f) = m.degree f

Tactic:
simp only [EmbeddingLike.apply_eq_iff_eq] at hf'

Premises used: EmbeddingLike.apply_eq_iff_eq
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
hf' : m.degree (m.subLTerm f) = m.degree f
h : m.subLTerm f = 0
⊢ 0 = m.degree f

Tactic:
simp only [h, degree_zero] at hf'

Premises used: MonomialOrder.degree_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
h : m.subLTerm f = 0
hf' : 0 = m.degree f
⊢ False

Tactic:
hf hf'.symm

Premises used: Eq.symm
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
h : m.subLTerm f = 0
hf' : 0 = m.degree f
⊢ False

Tactic:
exact hf hf'.symm

Premises used: Eq.symm
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
hf' : m.degree (m.subLTerm f) = m.degree f
⊢ m.subLTerm f ≠ 0

Tactic:
have : m.subLTerm f ≠ 0 := by
    intro h
    simp only [h, degree_zero] at hf'
    exact hf hf'.symm
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
hf' : m.degree (m.subLTerm f) = m.degree f
this : m.subLTerm f ≠ 0
⊢ coeff (m.degree f) (m.subLTerm f) ≠ 0

Tactic:
rw [← coeff_degree_ne_zero_iff (m := m), hf'] at this

Premises used: MonomialOrder.coeff_degree_ne_zero_iff
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
hf' : m.degree (m.subLTerm f) = m.degree f
this : coeff (m.degree f) (m.subLTerm f) ≠ 0
apply : coeff (m.degree f) (m.subLTerm f) = 0
⊢ False

Tactic:
apply this
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
hf' : m.degree (m.subLTerm f) = m.degree f
this : coeff (m.degree f) (m.subLTerm f) ≠ 0
⊢ coeff (m.degree f) (m.subLTerm f) = 0

Tactic:
simp [subLTerm, coeff_monomial, leadingCoeff]

Premises used: MonomialOrder.leadingCoeff, MvPolynomial.coeff_monomial, MonomialOrder.subLTerm
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
intro :
  ∀
    (hf' :
      Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.subLTerm f)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)),
    False
intro₁ : ∀ (hf' : m.degree (m.subLTerm f) = m.degree f), False
intro₂ : ∀ (hf' : m.degree (m.subLTerm f) = m.degree f) (this : m.subLTerm f ≠ 0), False
intro₃ : ∀ (hf' : m.degree (m.subLTerm f) = m.degree f) (this : coeff (m.degree f) (m.subLTerm f) ≠ 0), False
intro₄ :
  ∀ (hf' : m.degree (m.subLTerm f) = m.degree f) (this : coeff (m.degree f) (m.subLTerm f) ≠ 0),
    coeff (m.degree f) (m.subLTerm f) = 0
⊢ Ne.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.subLTerm f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)

Tactic:
classical
  intro hf'
  simp only [EmbeddingLike.apply_eq_iff_eq] at hf'
  have : m.subLTerm f ≠ 0 := by
    intro h
    simp only [h, degree_zero] at hf'
    exact hf hf'.symm
  rw [← coeff_degree_ne_zero_iff (m := m), hf'] at this
  apply this
  simp [subLTerm, coeff_monomial, leadingCoeff]

Premises used: MonomialOrder.leadingCoeff, EmbeddingLike.apply_eq_iff_eq, MvPolynomial.coeff_monomial, MonomialOrder.subLTerm, MonomialOrder.coeff_degree_ne_zero_iff
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
rw : m.degree f = m.degree f - m.degree b + m.degree b
hnc : ¬(↑hb.unit⁻¹ : R) * m.leadingCoeff f = 0
⊢ m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b

Tactic:
rw [degree_monomial, if_neg]

Premises used: MonomialOrder.degree_monomial, if_neg
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
h :
  ∀ (d : σ), Eq (α := ℕ) ((m.degree f : (a : σ) → ℕ) d : ℕ) ((m.degree f - m.degree b + m.degree b : (a : σ) → ℕ) d : ℕ)
⊢ m.degree f = m.degree f - m.degree b + m.degree b

Tactic:
ext d
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
d : σ
h h₁ : Eq (α := ℕ) ((m.degree f : (a : σ) → ℕ) d : ℕ) ((m.degree f : (a : σ) → ℕ) d : ℕ)
⊢ Eq (α := ℕ) ((m.degree f : (a : σ) → ℕ) d : ℕ) ((m.degree f - m.degree b + m.degree b : (a : σ) → ℕ) d : ℕ)

Tactic:
rw [tsub_add_cancel_of_le hbf]

Premises used: tsub_add_cancel_of_le
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
hnc : ¬f = 0
⊢ ¬(↑hb.unit⁻¹ : R) * m.leadingCoeff f = 0

Tactic:
simp only [Units.mul_right_eq_zero, leadingCoeff_eq_zero_iff]

Premises used: MonomialOrder.leadingCoeff_eq_zero_iff, Units.mul_right_eq_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
hf0 : f = 0
hnc : m.degree f = 0
⊢ False

Tactic:
apply hf
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
hf0 : f = 0
⊢ m.degree f = 0

Tactic:
simp [hf0]
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
rw : m.degree f = (if (↑hb.unit⁻¹ : R) * m.leadingCoeff f = 0 then 0 else m.degree f - m.degree b) + m.degree b
rw₁ : m.degree f = m.degree f - m.degree b + m.degree b
hnc : ¬(↑hb.unit⁻¹ : R) * m.leadingCoeff f = 0
rw₂ : m.degree f = m.degree f - m.degree b + m.degree b
hnc₁ : ¬(↑hb.unit⁻¹ : R) * m.leadingCoeff f = 0
rw₃ : m.degree f = m.degree f - m.degree b + m.degree b
hnc₂ hnc₃ : ¬(↑hb.unit⁻¹ : R) * m.leadingCoeff f = 0
⊢ m.degree f =
    degree.{u_1, u_2, u_3} m (R := R)
        ((monomial (m.degree f - m.degree b) : (a : R) → MvPolynomial σ R) ((↑hb.unit⁻¹ : R) * m.leadingCoeff f)) +
      m.degree b

Tactic:
classical
    rw [degree_monomial, if_neg]
    · ext d
      rw [tsub_add_cancel_of_le hbf]
    · simp only [Units.mul_right_eq_zero, leadingCoeff_eq_zero_iff]
      intro hf0
      apply hf
      simp [hf0]

Premises used: MonomialOrder.degree_monomial, MonomialOrder.leadingCoeff_eq_zero_iff, tsub_add_cancel_of_le, Units.mul_right_eq_zero, if_neg