awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
⊢ Eq.{u_2 + 1} (α := R) (coeff.{u_2, u_1} (σ := σ) (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i))
    (∏ i ∈ s, m.leadingCoeff (P i))
have empty : Eq.{u_2 + 1} (α := R) (coeff.{u_2, u_1} (σ := σ) (∑ i ∈ ∅, m.degree (P i)) (∏ i ∈ ∅, P i))
  (∏ i ∈ ∅, m.leadingCoeff (P i))
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert a s has hrec =>
    simp only [Finset.prod_insert has, Finset.sum_insert has]
    rw [coeff_mul_of_add_of_degree_le (le_of_eq rfl) degree_prod_le]
    exact congr_arg₂ _ rfl hrec
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
empty :
  Eq.{u_2 + 1} (α := R) (coeff.{u_2, u_1} (σ := σ) (∑ i ∈ ∅, m.degree (P i)) (∏ i ∈ ∅, P i))
    (∏ i ∈ ∅, m.leadingCoeff (P i))
⊢ Eq.{u_2 + 1} (α := R) (coeff.{u_2, u_1} (σ := σ) (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i))
    (∏ i ∈ s, m.leadingCoeff (P i))
have insert : ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
  (hrec :
    Eq.{u_2 + 1} (α := R) (coeff.{u_2, u_1} (σ := σ) (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i))
      (∏ i ∈ s, m.leadingCoeff (P i))),
  Eq.{u_2 + 1} (α := R) (coeff.{u_2, u_1} (σ := σ) (∑ i ∈ insert a s, m.degree (P i)) (∏ i ∈ insert a s, P i))
    (∏ i ∈ insert a s, m.leadingCoeff (P i))
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert a s has hrec =>
    simp only [Finset.prod_insert has, Finset.sum_insert has]
    rw [coeff_mul_of_add_of_degree_le (le_of_eq rfl) degree_prod_le]
    exact congr_arg₂ _ rfl hrec
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, Membership.mem (γ := Submonoid R) R⁰ (m.leadingCoeff (P i))
h : Nontrivial R
⊢ degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ s, P i) = ∑ i ∈ s, m.degree (P i)
have inr : Eq.{u_4 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ s, P i)) : m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (∑ i ∈ s, m.degree (P i)) : m.syn)
Tactic: apply m.toSyn.injective
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, Membership.mem (γ := Submonoid R) R⁰ (m.leadingCoeff (P i))
h : Nontrivial R
⊢ Eq.{u_4 + 1} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ s, P i)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (∑ i ∈ s, m.degree (P i)) : m.syn)
have inr : Membership.mem (γ := Finset (σ →₀ ℕ)) (support.{u_2, u_1} (R := R) (∏ i ∈ s, P i)) (∑ i ∈ s, m.degree (P i))
Tactic: refine le_antisymm degree_prod_le (m.le_degree ?_)
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, Membership.mem (γ := Submonoid R) R⁰ (m.leadingCoeff (P i))
h : Nontrivial R
⊢ Membership.mem (γ := Finset (σ →₀ ℕ)) (support.{u_2, u_1} (R := R) (∏ i ∈ s, P i)) (∑ i ∈ s, m.degree (P i))
have inr : Ne.{u_2 + 1} (α := R) (∏ i ∈ s, m.leadingCoeff (P i)) 0
Tactic: rw [mem_support_iff, m.coeff_prod_sum_degree]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (hypothesis)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, Membership.mem (γ := Submonoid R) R⁰ (m.leadingCoeff (P i))
⊢ degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ s, P i) = ∑ i ∈ s, m.degree (P i)
have x : Subsingleton R ∨ Nontrivial R
Tactic: cases subsingleton_or_nontrivial R with
  | inl _ => simp [Subsingleton.elim _ (0 : MvPolynomial σ R)]
  | inr _ =>
    apply m.toSyn.injective
    refine le_antisymm degree_prod_le (m.le_degree ?_)
    rw [mem_support_iff, m.coeff_prod_sum_degree]
    exact nonZeroDivisors.ne_zero (prod_mem_nonZeroDivisors_of_mem_nonZeroDivisors H)
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))
h : Nontrivial R
⊢ degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ s, P i) = ∑ i ∈ s, m.degree (P i)
have inr : Eq.{u_4 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ s, P i)) : m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (∑ i ∈ s, m.degree (P i)) : m.syn)
Tactic: apply m.toSyn.injective
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))
h : Nontrivial R
⊢ Eq.{u_4 + 1} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ s, P i)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (∑ i ∈ s, m.degree (P i)) : m.syn)
have inr : Membership.mem (γ := Finset (σ →₀ ℕ)) (support.{u_2, u_1} (R := R) (∏ i ∈ s, P i)) (∑ i ∈ s, m.degree (P i))
Tactic: refine le_antisymm degree_prod_le (m.le_degree ?_)
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))
h : Nontrivial R
⊢ Membership.mem (γ := Finset (σ →₀ ℕ)) (support.{u_2, u_1} (R := R) (∏ i ∈ s, P i)) (∑ i ∈ s, m.degree (P i))
have inr : Ne.{u_2 + 1} (α := R) (∏ i ∈ s, m.leadingCoeff (P i)) 0
Tactic: rw [mem_support_iff, m.coeff_prod_sum_degree]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (hypothesis)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))
⊢ degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ s, P i) = ∑ i ∈ s, m.degree (P i)
have x : Subsingleton R ∨ Nontrivial R
Tactic: cases subsingleton_or_nontrivial R with
  | inl _ => simp [Subsingleton.elim _ (0 : MvPolynomial σ R)]
  | inr _ =>
    apply m.toSyn.injective
    refine le_antisymm degree_prod_le (m.le_degree ?_)
    rw [mem_support_iff, m.coeff_prod_sum_degree]
    exact (IsRegular.prod H).ne_zero
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, P i ≠ 0
h : Nontrivial R
⊢ degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ s, P i) = ∑ i ∈ s, m.degree (P i)
have inr : Eq.{u_4 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ s, P i)) : m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (∑ i ∈ s, m.degree (P i)) : m.syn)
Tactic: apply m.toSyn.injective
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, P i ≠ 0
h : Nontrivial R
⊢ Eq.{u_4 + 1} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ s, P i)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (∑ i ∈ s, m.degree (P i)) : m.syn)
have inr : Membership.mem (γ := Finset (σ →₀ ℕ)) (support.{u_2, u_1} (R := R) (∏ i ∈ s, P i)) (∑ i ∈ s, m.degree (P i))
Tactic: refine le_antisymm degree_prod_le (m.le_degree ?_)
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (hypothesis)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, P i ≠ 0
⊢ degree.{u_1, u_2, u_4} m (R := R) (∏ i ∈ s, P i) = ∑ i ∈ s, m.degree (P i)
have x : Subsingleton R ∨ Nontrivial R
Tactic: cases subsingleton_or_nontrivial R with
  | inl _ => simp [Subsingleton.elim _ (0 : MvPolynomial σ R)]
  | inr _ =>
    apply m.toSyn.injective
    refine le_antisymm degree_prod_le (m.le_degree ?_)
    simpa [m.coeff_prod_sum_degree, Finset.prod_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (hypothesis)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f g : MvPolynomial σ R
hf : f * g ≠ 0
⊢ m.degree (f * g) = m.degree f + m.degree g
have hf₁ : f ≠ 0 ∧ g ≠ 0
Tactic: apply ne_zero_and_ne_zero_of_mul at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, m.Monic (P i)
⊢ Monic.{u_1, u_2, u_4} m (R := R) (∏ i ∈ s, P i)
have rw : Eq.{u_2 + 1} (α := R) (∏ i ∈ s, m.leadingCoeff (P i)) 1
Tactic: rw [Monic, leadingCoeff_prod_of_regular]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, m.Monic (P i)
rw : Eq.{u_2 + 1} (α := R) (∏ i ∈ s, m.leadingCoeff (P i)) 1
⊢ Monic.{u_1, u_2, u_4} m (R := R) (∏ i ∈ s, P i)
have rw₁ : ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))
Tactic: rw [Monic, leadingCoeff_prod_of_regular]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, m.Monic (P i)
i : ι
hi : i ∈ s
⊢ IsRegular (m.leadingCoeff (P i))
have rw : IsRegular.{u_2} (R := R) 1
Tactic: rw [(H i hi).leadingCoeff_eq_one]
-- 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
⊢ Eq (α := MvPolynomial σ R) (m.leadingTerm 0) 0
have rw : Eq (α := MvPolynomial σ R) 0 0
Tactic: rw [leadingTerm_eq_zero_iff]
-- 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
f : MvPolynomial σ R
⊢ m.degree (m.leadingTerm f) = m.degree f
have simp : f = 0 → 0 = m.degree f
Tactic: simp only [leadingTerm, degree_monomial, leadingCoeff_eq_zero_iff, ite_eq_right_iff]
-- 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
f : MvPolynomial σ R
⊢ m.degree (m.leadingTerm f) = m.degree f
have simp : f = 0 → 0 = m.degree f
Tactic: classical
  simp only [leadingTerm, degree_monomial, leadingCoeff_eq_zero_iff, ite_eq_right_iff]
  simp_intro h
-- 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
f : MvPolynomial σ R
⊢ m.leadingTerm (m.leadingTerm f) = m.leadingTerm f
have pos : ∀ (h : f = 0), m.leadingTerm (m.leadingTerm f) = m.leadingTerm f
Tactic: by_cases h : f = 0
-- 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
f : MvPolynomial σ R
pos : ∀ (h : f = 0), m.leadingTerm (m.leadingTerm f) = m.leadingTerm f
⊢ m.leadingTerm (m.leadingTerm f) = m.leadingTerm f
have neg : ∀ (h : ¬f = 0), m.leadingTerm (m.leadingTerm f) = m.leadingTerm f
Tactic: by_cases h : f = 0
-- 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
f : MvPolynomial σ R
⊢ m.leadingTerm (m.leadingTerm f) = m.leadingTerm f
have pos : ∀ (h : f = 0), m.leadingTerm (m.leadingTerm f) = m.leadingTerm f
Tactic: classical
  by_cases h : f = 0 <;> simp [leadingTerm, h, 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
f : MvPolynomial σ R
pos : ∀ (h : f = 0), m.leadingTerm (m.leadingTerm f) = m.leadingTerm f
⊢ m.leadingTerm (m.leadingTerm f) = m.leadingTerm f
have neg : ∀ (h : ¬f = 0), m.leadingTerm (m.leadingTerm f) = m.leadingTerm f
Tactic: classical
  by_cases h : f = 0 <;> simp [leadingTerm, h, 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
s : σ →₀ ℕ
c : R
⊢ Eq (α := MvPolynomial σ R) (m.leadingTerm ((monomial s : (a : R) → MvPolynomial σ R) c))
    ((monomial s : (a : R) → MvPolynomial σ R) c)
have pos : ∀ (h : c = 0),
  Eq (α := MvPolynomial σ R) (m.leadingTerm ((monomial s : (a : R) → MvPolynomial σ R) c))
    ((monomial s : (a : R) → MvPolynomial σ R) c)
Tactic: by_cases h : c = 0
-- 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
s : σ →₀ ℕ
c : R
pos :
  ∀ (h : c = 0),
    Eq (α := MvPolynomial σ R) (m.leadingTerm ((monomial s : (a : R) → MvPolynomial σ R) c))
      ((monomial s : (a : R) → MvPolynomial σ R) c)
⊢ Eq (α := MvPolynomial σ R) (m.leadingTerm ((monomial s : (a : R) → MvPolynomial σ R) c))
    ((monomial s : (a : R) → MvPolynomial σ R) c)
have neg : ∀ (h : ¬c = 0),
  Eq (α := MvPolynomial σ R) (m.leadingTerm ((monomial s : (a : R) → MvPolynomial σ R) c))
    ((monomial s : (a : R) → MvPolynomial σ R) c)
Tactic: by_cases h : c = 0
-- 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
s : σ →₀ ℕ
c : R
⊢ Eq (α := MvPolynomial σ R) (m.leadingTerm ((monomial s : (a : R) → MvPolynomial σ R) c))
    ((monomial s : (a : R) → MvPolynomial σ R) c)
have pos : ∀ (h : c = 0),
  Eq (α := MvPolynomial σ R) (m.leadingTerm ((monomial s : (a : R) → MvPolynomial σ R) c))
    ((monomial s : (a : R) → MvPolynomial σ R) c)
Tactic: classical
  by_cases h : c = 0 <;> simp [leadingTerm, degree_monomial, h]
-- 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
s : σ →₀ ℕ
c : R
pos :
  ∀ (h : c = 0),
    Eq (α := MvPolynomial σ R) (m.leadingTerm ((monomial s : (a : R) → MvPolynomial σ R) c))
      ((monomial s : (a : R) → MvPolynomial σ R) c)
⊢ Eq (α := MvPolynomial σ R) (m.leadingTerm ((monomial s : (a : R) → MvPolynomial σ R) c))
    ((monomial s : (a : R) → MvPolynomial σ R) c)
have neg : ∀ (h : ¬c = 0),
  Eq (α := MvPolynomial σ R) (m.leadingTerm ((monomial s : (a : R) → MvPolynomial σ R) c))
    ((monomial s : (a : R) → MvPolynomial σ R) c)
Tactic: classical
  by_cases h : c = 0 <;> simp [leadingTerm, degree_monomial, h]
-- 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 : NoZeroDivisors R
p q : MvPolynomial σ R
⊢ m.degree (m.leadingTerm p * q) = m.degree (p * q)
have inr : ∀
  (this :
    ∀ {σ : Type u_1} {m : MonomialOrder.{u_1, u_3} σ} {R : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R]
      (p q : MvPolynomial σ R) (h : p ≠ 0 ∧ q ≠ 0), m.degree (m.leadingTerm p * q) = m.degree (p * q))
  (h : p = 0 ∨ q = 0), m.degree (m.leadingTerm p * q) = m.degree (p * q)
Tactic: wlog! +distrib h : p ≠ 0 ∧ q ≠ 0
-- 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 : NoZeroDivisors R
p q : MvPolynomial σ R
inr :
  ∀
    (this :
      ∀ {σ : Type u_1} {m : MonomialOrder.{u_1, u_3} σ} {R : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R]
        (p q : MvPolynomial σ R) (h : p ≠ 0 ∧ q ≠ 0), m.degree (m.leadingTerm p * q) = m.degree (p * q))
    (h : p = 0 ∨ q = 0), m.degree (m.leadingTerm p * q) = m.degree (p * q)
⊢ m.degree (m.leadingTerm p * q) = m.degree (p * q)
have wlog! : ∀ {σ : Type u_1} {m : MonomialOrder.{u_1, u_3} σ} {R : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R]
  (p q : MvPolynomial σ R) (h : p ≠ 0 ∧ q ≠ 0), m.degree (m.leadingTerm p * q) = m.degree (p * q)
Tactic: wlog! +distrib h : p ≠ 0 ∧ q ≠ 0
Cleared hypotheses: inst_1, p, q
-- 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 : NoZeroDivisors R
p q : MvPolynomial σ R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder.{u_1, u_3} σ} {R : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R]
    (p q : MvPolynomial σ R) (h : p ≠ 0 ∧ q ≠ 0), m.degree (m.leadingTerm p * q) = m.degree (p * q)
h : p = 0 ∨ q = 0
⊢ m.degree (m.leadingTerm p * q) = m.degree (p * q)
have inr : m.degree (m.leadingTerm 0 * q) = m.degree (0 * q)
Tactic: obtain rfl | rfl := h
Cleared hypotheses: p, h
-- 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 : NoZeroDivisors R
p q : MvPolynomial σ R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder.{u_1, u_3} σ} {R : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R]
    (p q : MvPolynomial σ R) (h : p ≠ 0 ∧ q ≠ 0), m.degree (m.leadingTerm p * q) = m.degree (p * q)
h : p = 0 ∨ q = 0
inr : m.degree (m.leadingTerm 0 * q) = m.degree (0 * q)
⊢ m.degree (m.leadingTerm p * q) = m.degree (p * q)
have inr₁ : m.degree (m.leadingTerm p * 0) = m.degree (p * 0)
Tactic: obtain rfl | rfl := h
Cleared hypotheses: q, h
-- 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 : NoZeroDivisors R
p p' q : MvPolynomial σ R
hp : p ≠ 0
h :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (p * q)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (p' * q)) : m.syn)
⊢ LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p') : m.syn)
have inr : ∀
  (this :
    ∀ {σ : Type u_1} {m : MonomialOrder.{u_1, u_3} σ} {R : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R]
      {p p' q : MvPolynomial σ R} (hp : p ≠ 0)
      (h :
        LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (p * q)) : m.syn)
          ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (p' * q)) : m.syn))
      (hq : q ≠ 0),
      LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p') : m.syn))
  (hq : q = 0),
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p') : m.syn)
Tactic: wlog! hq : q ≠ 0
-- 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 : NoZeroDivisors R
p p' q : MvPolynomial σ R
hp : p ≠ 0
h :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (p * q)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (p' * q)) : m.syn)
inr :
  ∀
    (this :
      ∀ {σ : Type u_1} {m : MonomialOrder.{u_1, u_3} σ} {R : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R]
        {p p' q : MvPolynomial σ R} (hp : p ≠ 0)
        (h :
          LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (p * q)) : m.syn)
            ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (p' * q)) : m.syn))
        (hq : q ≠ 0),
        LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p) : m.syn)
          ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p') : m.syn))
    (hq : q = 0),
    LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p') : m.syn)
⊢ LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p') : m.syn)
have wlog! : ∀ {σ : Type u_1} {m : MonomialOrder.{u_1, u_3} σ} {R : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R]
  {p p' q : MvPolynomial σ R} (hp : p ≠ 0)
  (h :
    LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (p * q)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (p' * q)) : m.syn))
  (hq : q ≠ 0),
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p') : m.syn)
Tactic: wlog! hq : q ≠ 0
Cleared hypotheses: inst_1, p, p', q, hp, h
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (hypothesis)
Goal:
σ_1 : Type u_1
m_1 : MonomialOrder.{u_1, u_3} σ_1
R_1 : Type u_2
inst : CommSemiring R_1
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst_1 : CommSemiring R
inst_2 : NoZeroDivisors R
p p' q : MvPolynomial σ R
hp : p ≠ 0
h :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (p * q)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (p' * q)) : m.syn)
hq : q ≠ 0
⊢ LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p') : m.syn)
have h₁ : LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (p * q)) : m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p' + m.degree q) : m.syn)
Tactic: apply lt_of_le_of_lt' m.degree_mul_le at h
Cleared hypotheses: h
-- 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 : NoZeroDivisors R
p p' q : MvPolynomial σ R
hp : p ≠ 0
hq : q ≠ 0
⊢ LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (p * q)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (p' * q)) : m.syn) ↔
    LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p') : m.syn)
have refine : LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p') : m.syn) →
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (p * q)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (p' * q)) : m.syn)
Tactic: refine ⟨m.degree_lt_of_left_ne_zero_of_degree_mul_lt hp, ?_⟩
-- 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 : NoZeroDivisors R
p p' q : MvPolynomial σ R
hp : p ≠ 0
hq : q ≠ 0
h :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p') : m.syn)
⊢ p' ≠ 0
have contrapose! : ∀ (h : p' = 0),
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p') : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree p) : m.syn)
Tactic: contrapose! h
Cleared hypotheses: h
-- 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 q : MvPolynomial σ R
⊢ m.leadingTerm p = m.leadingTerm q ↔ m.leadingCoeff p = m.leadingCoeff q ∧ m.degree p = m.degree q
have rw : m.degree p = m.degree q ∧ m.leadingCoeff p = m.leadingCoeff q ∨ m.leadingCoeff p = 0 ∧ m.leadingCoeff q = 0 ↔
  m.leadingCoeff p = m.leadingCoeff q ∧ m.degree p = m.degree q
Tactic: rw [leadingTerm, leadingTerm, monomial_eq_monomial_iff]