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 g : MvPolynomial σ R
a b : σ →₀ ℕ
ha :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) a : m.syn)
hb :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
c d : σ →₀ ℕ
h : (c, d) ≠ (a, b)
hcd : c + d = a + b
hf :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
hf' :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
neg :
  HAdd.hAdd (α := m.syn) (β := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) a : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn) ≤
    HAdd.hAdd (α := m.syn) (β := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) a : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)

Tactic:
apply le_of_add_le_add_right (a := m.toSyn b)

Premises used: le_of_add_le_add_right
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
a b : σ →₀ ℕ
ha :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) a : m.syn)
hb :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
c d : σ →₀ ℕ
h : (c, d) ≠ (a, b)
hcd : c + d = a + b
hf :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
hf' :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
neg :
  HAdd.hAdd (α := m.syn) (β := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn) ≤
    HAdd.hAdd (α := m.syn) (β := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
⊢ HAdd.hAdd (α := m.syn) (β := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) a : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn) ≤
    HAdd.hAdd (α := m.syn) (β := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)

Tactic:
rw [← map_add, ← hcd, map_add]

Premises used: map_add
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
a b : σ →₀ ℕ
ha :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) a : m.syn)
hb :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
c d : σ →₀ ℕ
h : (c, d) ≠ (a, b)
hcd : c + d = a + b
hf :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
hf' :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
neg : LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
⊢ HAdd.hAdd (α := m.syn) (β := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn) ≤
    HAdd.hAdd (α := m.syn) (β := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)

Tactic:
simp only [add_le_add_iff_left]

Premises used: add_le_add_iff_left
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
a b : σ →₀ ℕ
ha :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) a : m.syn)
hb :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
c d : σ →₀ ℕ
h : (c, d) ≠ (a, b)
hcd : c + d = a + b
hf :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
hf' :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)

Tactic:
le_trans hf' hb

Premises used: le_trans
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
a b : σ →₀ ℕ
ha :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) a : m.syn)
hb :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
c d : σ →₀ ℕ
h : (c, d) ≠ (a, b)
hcd : c + d = a + b
hf :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
hf' :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)

Tactic:
exact le_trans hf' hb

Premises used: le_trans
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
a b : σ →₀ ℕ
ha :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) a : m.syn)
hb :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
⊢ (a, b) ∉ @Finset.antidiagonal _ Finsupp.instAddMonoid _ (a + b) → coeff (a, b).1 f * coeff (a, b).2 g = 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
f g : MvPolynomial σ R
a b : σ →₀ ℕ
ha :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) a : m.syn)
hb :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
rw : ∑ x ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ (a + b), coeff x.1 f * coeff x.2 g = coeff a f * coeff b g
rw₁ : coeff (a, b).1 f * coeff (a, b).2 g = coeff a f * coeff b g
h₀ : ∀ b_1 ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ (a + b), b_1 ≠ (a, b) → coeff b_1.1 f * coeff b_1.2 g = 0
h₁ : (a, b) ∉ @Finset.antidiagonal _ Finsupp.instAddMonoid _ (a + b) → coeff (a, b).1 f * coeff (a, b).2 g = 0
rw₂ : coeff (a, b).1 f * coeff (a, b).2 g = coeff a f * coeff b g
h₂ : ∀ b_1 ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ (a + b), b_1 ≠ (a, b) → coeff b_1.1 f * coeff b_1.2 g = 0
h₃ : (a, b) ∉ @Finset.antidiagonal _ Finsupp.instAddMonoid _ (a + b) → coeff (a, b).1 f * coeff (a, b).2 g = 0
h₄ : ∀ b_1 ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ (a + b), b_1 ≠ (a, b) → coeff b_1.1 f * coeff b_1.2 g = 0
h₅ h₆ : (a, b) ∉ @Finset.antidiagonal _ Finsupp.instAddMonoid _ (a + b) → coeff (a, b).1 f * coeff (a, b).2 g = 0
⊢ coeff (a + b) (f * g) = coeff a f * coeff b g

Tactic:
classical
  rw [coeff_mul, Finset.sum_eq_single (a, b)]
  · rintro ⟨c, d⟩ hcd h
    simp only [Finset.mem_antidiagonal] at hcd
    by_cases hf : m.degree f ≺[m] c
    · rw [m.coeff_eq_zero_of_lt hf, zero_mul]
    · suffices m.degree g ≺[m] d by
        rw [coeff_eq_zero_of_lt this, mul_zero]
      rw [not_lt] at hf
      rw [← not_le]
      intro hf'
      apply h
      suffices c = a by
        simpa [Prod.mk.injEq, this] using hcd
      apply m.toSyn.injective
      apply le_antisymm (le_trans hf ha)
      apply le_of_add_le_add_right (a := m.toSyn b)
      rw [← map_add, ← hcd, map_add]
      simp only [add_le_add_iff_left]
      exact le_trans hf' hb
  · simp

Premises used: not_le, le_of_add_le_add_right, MulZeroClass.zero_mul, add_le_add_iff_left, map_add, Prod.mk, Finset.sum_eq_single, Finset.HasAntidiagonal.mem_antidiagonal, MonomialOrder.degree, not_lt, AddEquiv.injective, MvPolynomial.coeff_mul, 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 g : MvPolynomial σ R
⊢ coeff (m.degree f + m.degree g) (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
coeff_mul_of_add_of_degree_le (le_of_eq rfl) (le_of_eq rfl)

Premises used: MonomialOrder.leadingCoeff, le_of_eq, MonomialOrder.coeff_mul_of_add_of_degree_le, rfl
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hfg : m.leadingCoeff f * m.leadingCoeff g ≠ 0
a :
  Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f * g)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f + m.degree g) : m.syn)
⊢ m.degree (f * g) = m.degree f + m.degree g

Tactic:
apply m.toSyn.injective

Premises used: 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 g : MvPolynomial σ R
hfg : m.leadingCoeff f * m.leadingCoeff g ≠ 0
a :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f + m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f * g)) : m.syn)
⊢ Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f * g)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f + m.degree g) : m.syn)

Tactic:
apply le_antisymm degree_mul_le

Premises used: MonomialOrder.degree_mul_le, le_antisymm
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hfg : m.leadingCoeff f * m.leadingCoeff g ≠ 0
a : m.degree f + m.degree g ∈ (f * g).support
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f + m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f * g)) : m.syn)

Tactic:
apply le_degree

Premises used: 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 g : MvPolynomial σ R
hfg a : m.leadingCoeff f * m.leadingCoeff g ≠ 0
⊢ m.degree f + m.degree g ∈ (f * g).support

Tactic:
rw [mem_support_iff, coeff_mul_of_degree_add]

Premises used: MvPolynomial.mem_support_iff, MonomialOrder.coeff_mul_of_degree_add
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hfg : m.leadingCoeff f * m.leadingCoeff g ≠ 0
⊢ m.leadingCoeff f * m.leadingCoeff g ≠ 0

Tactic:
hfg
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hfg : m.leadingCoeff f * m.leadingCoeff g ≠ 0
⊢ m.leadingCoeff f * m.leadingCoeff g ≠ 0

Tactic:
exact hfg
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hfg : m.leadingCoeff f * m.leadingCoeff g ≠ 0
rw : coeff (m.degree (f * g)) (f * g) = m.leadingCoeff f * m.leadingCoeff g
rw₁ : coeff (m.degree (f * g)) (f * g) = coeff (m.degree f + m.degree g) (f * g)
rw₂ rw₃ : coeff (m.degree f + m.degree g) (f * g) = coeff (m.degree f + m.degree g) (f * g)
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
rw [leadingCoeff, ← coeff_mul_of_degree_add, degree_mul_of_mul_leadingCoeff_ne_zero hfg]

Premises used: MonomialOrder.leadingCoeff, MonomialOrder.degree_mul_of_mul_leadingCoeff_ne_zero, MonomialOrder.coeff_mul_of_degree_add
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hf : Membership.mem (γ := Submonoid R) R⁰ (m.leadingCoeff f)
hg : g ≠ 0
hfg : m.leadingCoeff f * m.leadingCoeff g ≠ 0
⊢ m.degree (f * g) = m.degree f + m.degree g

Tactic:
apply degree_mul_of_mul_leadingCoeff_ne_zero

Premises used: MonomialOrder.degree_mul_of_mul_leadingCoeff_ne_zero
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hf : Membership.mem (γ := Submonoid R) R⁰ (m.leadingCoeff f)
hg : g ≠ 0
hfg : ¬m.leadingCoeff g = 0
⊢ m.leadingCoeff f * m.leadingCoeff g ≠ 0

Tactic:
apply not_imp_not.mpr (mem_nonZeroDivisors_iff.mp hf |>.1 _)

Premises used: Iff.mpr, mem_nonZeroDivisors_iff, And.left, Iff.mp, 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 g : MvPolynomial σ R
hf : Membership.mem (γ := Submonoid R) R⁰ (m.leadingCoeff f)
hg : g ≠ 0
⊢ ¬m.leadingCoeff g = 0

Tactic:
simp [hg]
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hf : f ≠ 0
hg : Membership.mem (γ := Submonoid R) R⁰ (m.leadingCoeff g)
⊢ m.degree (f * g) = m.degree f + m.degree g

Tactic:
add_comm (m.degree f) (m.degree g) ▸ mul_comm f g ▸ degree_mul_of_left_mem_nonZeroDivisors hg hf

Premises used: Eq.rec, MonomialOrder.degree_mul_of_left_mem_nonZeroDivisors, add_comm, MonomialOrder.degree, mul_comm, Eq.symm
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hf : Membership.mem (γ := Submonoid R) R⁰ (m.leadingCoeff f)
pos : ∀ (hg : g = 0), m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
neg : ∀ (hg : ¬g = 0), m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
by_cases hg : g = 0
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hf : Membership.mem (γ := Submonoid R) R⁰ (m.leadingCoeff f)
hg : g = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
simp [hg]
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hf : Membership.mem (γ := Submonoid R) R⁰ (m.leadingCoeff f)
hg : ¬g = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
simp only [leadingCoeff, degree_mul_of_left_mem_nonZeroDivisors hf hg, coeff_mul_of_degree_add]

Premises used: MonomialOrder.leadingCoeff, MonomialOrder.degree_mul_of_left_mem_nonZeroDivisors, MonomialOrder.coeff_mul_of_degree_add
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hg : Membership.mem (γ := Submonoid R) R⁰ (m.leadingCoeff g)
pos : ∀ (hf : f = 0), m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
neg : ∀ (hf : ¬f = 0), m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
by_cases hf : f = 0
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hg : Membership.mem (γ := Submonoid R) R⁰ (m.leadingCoeff g)
hf : f = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
simp [hf]
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hg : Membership.mem (γ := Submonoid R) R⁰ (m.leadingCoeff g)
hf : ¬f = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
simp only [leadingCoeff, degree_mul_of_right_mem_nonZeroDivisors hf hg, coeff_mul_of_degree_add]

Premises used: MonomialOrder.leadingCoeff, MonomialOrder.coeff_mul_of_degree_add, MonomialOrder.degree_mul_of_right_mem_nonZeroDivisors
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hf : IsRegular (m.leadingCoeff f)
hg : g ≠ 0
hfg : m.leadingCoeff f * m.leadingCoeff g ≠ 0
⊢ m.degree (f * g) = m.degree f + m.degree g

Tactic:
apply degree_mul_of_mul_leadingCoeff_ne_zero

Premises used: MonomialOrder.degree_mul_of_mul_leadingCoeff_ne_zero
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hf : IsRegular (m.leadingCoeff f)
hg : g ≠ 0
hfg : ¬g = 0
⊢ m.leadingCoeff f * m.leadingCoeff g ≠ 0

Tactic:
simp only [ne_eq, hf, IsRegular.left, IsLeftRegular.mul_left_eq_zero_iff,
    leadingCoeff_eq_zero_iff]

Premises used: IsLeftRegular.mul_left_eq_zero_iff, MonomialOrder.leadingCoeff_eq_zero_iff, ne_eq, IsRegular.left
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hf : IsRegular (m.leadingCoeff f)
hg : g ≠ 0
⊢ ¬g = 0

Tactic:
hg
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hf : IsRegular (m.leadingCoeff f)
hg : g ≠ 0
⊢ ¬g = 0

Tactic:
exact hg
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hf : IsRegular (m.leadingCoeff f)
pos : ∀ (hg : g = 0), m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
neg : ∀ (hg : ¬g = 0), m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
by_cases hg : g = 0
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hf : IsRegular (m.leadingCoeff f)
hg : g = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
simp [hg]
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hf : IsRegular (m.leadingCoeff f)
hg : ¬g = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
simp only [leadingCoeff, degree_mul_of_isRegular_left hf hg, coeff_mul_of_degree_add]

Premises used: MonomialOrder.leadingCoeff, MonomialOrder.degree_mul_of_isRegular_left, MonomialOrder.coeff_mul_of_degree_add
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hf : f ≠ 0
hg : IsRegular (m.leadingCoeff g)
rw : m.degree (g * f) = m.degree f + m.degree g
rw₁ : m.degree g + m.degree f = m.degree f + m.degree g
rw₂ rw₃ : m.degree f + m.degree g = m.degree f + m.degree g
⊢ m.degree (f * g) = m.degree f + m.degree g

Tactic:
rw [mul_comm, m.degree_mul_of_isRegular_left hg hf, add_comm]

Premises used: add_comm, mul_comm, MonomialOrder.degree_mul_of_isRegular_left
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hg : IsRegular (m.leadingCoeff g)
pos : ∀ (hf : f = 0), m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
neg : ∀ (hf : ¬f = 0), m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
by_cases hf : f = 0
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hg : IsRegular (m.leadingCoeff g)
hf : f = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
simp [hf]
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hg : IsRegular (m.leadingCoeff g)
hf : ¬f = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
simp only [leadingCoeff, degree_mul_of_isRegular_right hf hg, coeff_mul_of_degree_add]

Premises used: MonomialOrder.leadingCoeff, MonomialOrder.degree_mul_of_isRegular_right, MonomialOrder.coeff_mul_of_degree_add
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hf : m.Monic f
hg : m.Monic g
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hf : m.Monic f
hg : m.Monic g
h : Nontrivial R
this : m.leadingCoeff f * m.leadingCoeff g = 1
rw : m.leadingCoeff f * m.leadingCoeff g ≠ 0
⊢ m.Monic (f * g)

Tactic:
rw [Monic, MonomialOrder.leadingCoeff,
      degree_mul_of_mul_leadingCoeff_ne_zero, coeff_mul_of_degree_add, this]

Premises used: MonomialOrder.Monic, MonomialOrder.leadingCoeff, MonomialOrder.degree_mul_of_mul_leadingCoeff_ne_zero, MonomialOrder.coeff_mul_of_degree_add
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hf : m.Monic f
hg : m.Monic g
h : Nontrivial R
this : m.leadingCoeff f * m.leadingCoeff g = 1
rw : Ne.{u_2 + 1} (α := R) 1 0
⊢ m.leadingCoeff f * m.leadingCoeff g ≠ 0

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hf : m.Monic f
hg : m.Monic g
h : Nontrivial R
this : m.leadingCoeff f * m.leadingCoeff g = 1
⊢ Ne.{u_2 + 1} (α := R) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hf : m.Monic f
hg : m.Monic g
h : Nontrivial R
this : m.leadingCoeff f * m.leadingCoeff g = 1
⊢ Ne.{u_2 + 1} (α := R) 1 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hf : m.Monic f
hg : m.Monic g
h : Nontrivial R
suffices : m.leadingCoeff f * m.leadingCoeff g = 1
⊢ m.Monic (f * g)

Tactic:
suffices m.leadingCoeff f * m.leadingCoeff g = 1 by
    rw [Monic, MonomialOrder.leadingCoeff,
      degree_mul_of_mul_leadingCoeff_ne_zero, coeff_mul_of_degree_add, this]
    rw [this]
    exact one_ne_zero
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
hf : m.Monic f
hg : m.Monic g
h : Nontrivial R
rw : 1 * m.leadingCoeff g = 1
rw₁ : HMul.hMul (α := R) 1 1 = 1
rw₂ rw₃ : Eq.{u_2 + 1} (α := R) 1 1
⊢ m.leadingCoeff f * m.leadingCoeff g = 1

Tactic:
rw [hf.leadingCoeff_eq_one, hg.leadingCoeff_eq_one, one_mul]

Premises used: MonomialOrder.Monic.leadingCoeff_eq_one, one_mul