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_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
⊢ ∀ c ∈ (f + g).support,
    LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
          ((m.toSyn.symm : (a : m.syn) → σ →₀ ℕ)
            (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f)) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g)))) :
        m.syn)
have simp : ∀ c ∈ (f + g).support,
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn) ∨
    LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
Tactic: simp only [AddEquiv.apply_symm_apply, le_sup_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 g : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ (f + g).support
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn) ∨
    LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
have pos : ∀ (hf : b ∈ f.support),
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn) ∨
    LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
Tactic: by_cases hf : b ∈ f.support
-- 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 g : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ (f + g).support
pos :
  ∀ (hf : b ∈ f.support),
    LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn) ∨
      LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn) ∨
    LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
have neg : ∀ (hf : b ∉ f.support),
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn) ∨
    LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
Tactic: by_cases hf : b ∈ f.support
-- 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 g : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ (f + g).support
hf : b ∈ f.support
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn) ∨
    LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
have pos : LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
Tactic: left
-- 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 g : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ (f + g).support
hf : b ∉ f.support
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn) ∨
    LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
have neg : LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
Tactic: right
-- 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 g : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ (f + g).support
hf : b ∉ f.support
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
have neg : b ∈ g.support
Tactic: apply m.le_degree
-- 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
f g : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ (f + g).support
hf : b ∉ f.support
⊢ b ∈ g.support
have hf₁ : coeff b f = 0
Tactic: simp only [notMem_support_iff] 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
f : α → MvPolynomial σ R
a : α
s : Finset α
haA : a ∉ s
h :
  LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ x ∈ s, f x)) : m.syn)
    (s.sup fun (x : α) ↦ (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f x)) : m.syn)
⊢ LE.le.{u_4} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ x ∈ Finset.cons a s haA, f x)) : m.syn)
    ((Finset.cons a s haA).sup fun (x : α) ↦ (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f x)) : m.syn)
have cons : LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f a + ∑ x ∈ s, f x)) : m.syn)
  (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f a)))
      (s.sup fun (x : α) ↦ (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f x))) :
    m.syn)
Tactic: rw [Finset.sum_cons, Finset.sup_cons]
-- 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
s : Finset α
f : α → MvPolynomial σ R
⊢ LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ x ∈ s, f x)) : m.syn)
    (s.sup fun (x : α) ↦ (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f x)) : m.syn)
have empty : LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ x ∈ ∅, f x)) : m.syn)
  (Finset.sup ∅ fun (x : α) ↦ (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f x)) : m.syn)
Tactic: induction s using Finset.cons_induction_on with
  | empty => simp
  | cons a s haA h =>
    rw [Finset.sum_cons, Finset.sup_cons]
    exact le_trans m.degree_add_le (max_le_max le_rfl h)
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
s : Finset α
f : α → MvPolynomial σ R
empty :
  LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ x ∈ ∅, f x)) : m.syn)
    (Finset.sup ∅ fun (x : α) ↦ (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f x)) : m.syn)
⊢ LE.le.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ x ∈ s, f x)) : m.syn)
    (s.sup fun (x : α) ↦ (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f x)) : m.syn)
have cons : ∀ (a : α) (s : Finset α) (haA : a ∉ s)
  (h :
    LE.le.{u_4} (α := m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ x ∈ s, f x)) : m.syn)
      (s.sup fun (x : α) ↦ (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f x)) : m.syn)),
  LE.le.{u_4} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ x ∈ Finset.cons a s haA, f x)) : m.syn)
    ((Finset.cons a s haA).sup fun (x : α) ↦ (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f x)) : m.syn)
Tactic: induction s using Finset.cons_induction_on with
  | empty => simp
  | cons a s haA h =>
    rw [Finset.sum_cons, Finset.sup_cons]
    exact le_trans m.degree_add_le (max_le_max le_rfl h)
Cleared hypotheses: s
-- 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 g : MvPolynomial σ R
h :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
⊢ m.degree (f + g) = m.degree f
have 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.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_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
h :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : 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.syn)
have a : LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f + g)) : m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
Tactic: apply le_antisymm
-- 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 g : MvPolynomial σ R
h :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
a :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f + g)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : 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.syn)
have a₁ : LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f + g)) : m.syn)
Tactic: apply le_antisymm
-- 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 g : MvPolynomial σ R
h :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : 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 (f + g)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
have a : LE.le.{u_3} (α := m.syn)
  (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f)) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g)) : m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
Tactic: apply le_trans degree_add_le
-- 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 g : MvPolynomial σ R
h :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : 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 f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f + g)) : m.syn)
have a : m.degree f ∈ (f + g).support
Tactic: apply le_degree
-- 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 g : MvPolynomial σ R
h :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
⊢ m.degree f ∈ (f + g).support
have a : f ≠ 0
Tactic: rw [mem_support_iff, coeff_add, m.coeff_eq_zero_of_lt h, add_zero,
      ← leadingCoeff, leadingCoeff_ne_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
f g : MvPolynomial σ R
h :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
hf : f = 0
⊢ False
have h₁ : ¬LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_3} m (R := R) 0) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
Tactic: rw [← not_le, hf] at h
Cleared hypotheses: h, hf
-- 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 g : MvPolynomial σ R
h :
  ¬LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_3} m (R := R) 0) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
hf : f = 0
⊢ False
have a : LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_3} m (R := R) 0) : m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
Tactic: apply 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 g : MvPolynomial σ R
h :
  ¬LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_3} m (R := R) 0) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
hf : f = 0
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_3} m (R := R) 0) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
have a : LE.le.{u_3} (α := m.syn) (0 : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
Tactic: simp only [degree_zero, map_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
f g : MvPolynomial σ R
h :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
⊢ m.degree (f + g) = m.degree g
have rw : m.degree (g + f) = m.degree g
Tactic: rw [add_comm]
-- 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 g : MvPolynomial σ R
h : m.degree f ≠ m.degree g
⊢ Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f + g)) : m.syn)
    (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f)) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g)) : m.syn)
have pos : ∀
  (h' :
    LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)),
  Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f + g)) : m.syn)
    (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f)) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g)) : m.syn)
Tactic: by_cases h' : m.degree g ≺[m] m.degree f
-- 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 g : MvPolynomial σ R
h : m.degree f ≠ m.degree g
pos :
  ∀
    (h' :
      LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)),
    Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f + g)) : m.syn)
      (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f)) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g)) : m.syn)
⊢ Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f + g)) : m.syn)
    (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f)) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g)) : m.syn)
have neg : ∀
  (h' :
    ¬LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)),
  Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f + g)) : m.syn)
    (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f)) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g)) : m.syn)
Tactic: by_cases h' : m.degree g ≺[m] m.degree f
-- 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
f g : MvPolynomial σ R
h : m.degree f ≠ m.degree g
h' :
  ¬LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
⊢ Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f + g)) : m.syn)
    (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f)) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g)) : m.syn)
have h'₁ : ¬m.degree f = m.degree g →
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
Tactic: rw [not_lt, le_iff_eq_or_lt, Classical.or_iff_not_imp_left, EmbeddingLike.apply_eq_iff_eq] 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
f g : MvPolynomial σ R
h : m.degree f ≠ m.degree g
h' :
  ¬m.degree f = m.degree g →
    LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
⊢ Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f + g)) : m.syn)
    (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f)) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g)) : m.syn)
have neg : LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
Tactic: rw [add_comm, degree_add_of_lt (h' h), right_eq_sup]
-- 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 g : MvPolynomial σ R
⊢ LE.le.{u_3} (α := 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)
have rw : ∀ c ∈ (f * g).support,
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f + m.degree g) : m.syn)
Tactic: rw [degree_le_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 g : MvPolynomial σ R
c : σ →₀ ℕ
⊢ c ∈ (f * g).support →
    LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f + m.degree g) : m.syn)
have rw : LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f + m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn) →
  coeff c (f * g) = 0
Tactic: rw [← not_lt, mem_support_iff, not_imp_not]
-- 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 g : MvPolynomial σ R
c : σ →₀ ℕ
hc :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f + m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
⊢ coeff c (f * g) = 0
have rw : Eq.{u_2 + 1} (α := R) (∑ x ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ c, coeff x.1 f * coeff x.2 g) 0
Tactic: rw [coeff_mul]
-- 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 g : MvPolynomial σ R
c : σ →₀ ℕ
hc :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f + m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
⊢ Eq.{u_2 + 1} (α := R) (∑ x ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ c, coeff x.1 f * coeff x.2 g) 0
have h : ∀ x ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ c, coeff x.1 f * coeff x.2 g = 0
Tactic: apply Finset.sum_eq_zero
-- 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
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f + m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
d e : σ →₀ ℕ
hde : (d, e) ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ c
⊢ coeff (d, e).1 f * coeff (d, e).2 g = 0
have hde₁ : d + e = c
Tactic: simp only [Finset.mem_antidiagonal] at hde
Cleared hypotheses: hde
-- 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 g : MvPolynomial σ R
c : σ →₀ ℕ
hc :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f + m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
d e : σ →₀ ℕ
hde : d + e = c
⊢ coeff (d, e).1 f * coeff (d, e).2 g = 0
have h : coeff d f * coeff e g = 0
Tactic: dsimp only
-- 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 g : MvPolynomial σ R
c : σ →₀ ℕ
hc :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f + m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
d e : σ →₀ ℕ
hde : d + e = c
⊢ coeff d f * coeff e g = 0
have pos : ∀
  (hd :
    LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)),
  coeff d f * coeff e g = 0
Tactic: by_cases hd : m.degree f ≺[m] d
-- 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 g : MvPolynomial σ R
c : σ →₀ ℕ
hc :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f + m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
d e : σ →₀ ℕ
hde : d + e = c
pos :
  ∀
    (hd :
      LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)),
    coeff d f * coeff e g = 0
⊢ coeff d f * coeff e g = 0
have neg : ∀
  (hd :
    ¬LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)),
  coeff d f * coeff e g = 0
Tactic: by_cases hd : m.degree f ≺[m] d
-- 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 g : MvPolynomial σ R
c : σ →₀ ℕ
hc :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f + m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
d e : σ →₀ ℕ
hde : d + e = c
hd :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
⊢ coeff d f * coeff e g = 0
have pos : 0 * coeff e g = 0
Tactic: rw [m.coeff_eq_zero_of_lt hd, zero_mul]
-- 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 g : MvPolynomial σ R
c : σ →₀ ℕ
hc :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f + m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
d e : σ →₀ ℕ
hde : d + e = c
hd :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
pos : 0 * coeff e g = 0
⊢ coeff d f * coeff e g = 0
have pos₁ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [m.coeff_eq_zero_of_lt hd, zero_mul]