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 : σ →₀ ℕ
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)
this :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) e : m.syn)
⊢ coeff d f * coeff e g = 0
have rw : coeff d f * 0 = 0
Tactic: rw [m.coeff_eq_zero_of_lt this, mul_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
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)
this :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) e : m.syn)
rw : coeff d f * 0 = 0
⊢ coeff d f * coeff e g = 0
have rw₁ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [m.coeff_eq_zero_of_lt this, mul_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
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 neg : LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) e : m.syn)
Tactic: suffices m.degree g ≺[m] e by
      rw [m.coeff_eq_zero_of_lt this, mul_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 = 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)
⊢ LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) e : m.syn)
have hd₁ : LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
Tactic: simp only [not_lt] at hd
Cleared hypotheses: hd
-- 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 :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : 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 g) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) e : m.syn)
have neg : HAdd.hAdd (α := m.syn) (β := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g) : m.syn) <
  HAdd.hAdd (α := m.syn) (β := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) e : m.syn)
Tactic: apply lt_of_add_lt_add_left (a := m.toSyn 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
⊢ 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: classical
  rw [degree_le_iff]
  intro c
  rw [← not_lt, mem_support_iff, not_imp_not]
  intro hc
  rw [coeff_mul]
  apply Finset.sum_eq_zero
  rintro ⟨d, e⟩ hde
  simp only [Finset.mem_antidiagonal] at hde
  dsimp only
  by_cases hd : m.degree f ≺[m] d
  · rw [m.coeff_eq_zero_of_lt hd, zero_mul]
  · suffices m.degree g ≺[m] e by
      rw [m.coeff_eq_zero_of_lt this, mul_zero]
    simp only [not_lt] at hd
    apply lt_of_add_lt_add_left (a := m.toSyn d)
    grw [← map_add _ _ e, hd, ← map_add, hde]
    exact hc
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
rw rw₁ rw₂ 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)
⊢ 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 : σ →₀ ℕ),
  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: classical
  rw [degree_le_iff]
  intro c
  rw [← not_lt, mem_support_iff, not_imp_not]
  intro hc
  rw [coeff_mul]
  apply Finset.sum_eq_zero
  rintro ⟨d, e⟩ hde
  simp only [Finset.mem_antidiagonal] at hde
  dsimp only
  by_cases hd : m.degree f ≺[m] d
  · rw [m.coeff_eq_zero_of_lt hd, zero_mul]
  · suffices m.degree g ≺[m] e by
      rw [m.coeff_eq_zero_of_lt this, mul_zero]
    simp only [not_lt] at hd
    apply lt_of_add_lt_add_left (a := m.toSyn d)
    grw [← map_add _ _ e, hd, ← map_add, hde]
    exact hc
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
rw rw₁ rw₂ 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)
rw₄ rw₅ :
  ∀ (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
⊢ 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 : σ →₀ ℕ)
  (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
Tactic: classical
  rw [degree_le_iff]
  intro c
  rw [← not_lt, mem_support_iff, not_imp_not]
  intro hc
  rw [coeff_mul]
  apply Finset.sum_eq_zero
  rintro ⟨d, e⟩ hde
  simp only [Finset.mem_antidiagonal] at hde
  dsimp only
  by_cases hd : m.degree f ≺[m] d
  · rw [m.coeff_eq_zero_of_lt hd, zero_mul]
  · suffices m.degree g ≺[m] e by
      rw [m.coeff_eq_zero_of_lt this, mul_zero]
    simp only [not_lt] at hd
    apply lt_of_add_lt_add_left (a := m.toSyn d)
    grw [← map_add _ _ e, hd, ← map_add, hde]
    exact hc
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
rw rw₁ rw₂ 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)
rw₄ rw₅ :
  ∀ (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
rw₆ :
  ∀ (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
⊢ 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 h : ∀ (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)),
  ∀ x ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ c, coeff x.1 f * coeff x.2 g = 0
Tactic: classical
  rw [degree_le_iff]
  intro c
  rw [← not_lt, mem_support_iff, not_imp_not]
  intro hc
  rw [coeff_mul]
  apply Finset.sum_eq_zero
  rintro ⟨d, e⟩ hde
  simp only [Finset.mem_antidiagonal] at hde
  dsimp only
  by_cases hd : m.degree f ≺[m] d
  · rw [m.coeff_eq_zero_of_lt hd, zero_mul]
  · suffices m.degree g ≺[m] e by
      rw [m.coeff_eq_zero_of_lt this, mul_zero]
    simp only [not_lt] at hd
    apply lt_of_add_lt_add_left (a := m.toSyn d)
    grw [← map_add _ _ e, hd, ← map_add, hde]
    exact hc
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
rw rw₁ rw₂ 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)
rw₄ rw₅ :
  ∀ (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
rw₆ :
  ∀ (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
h :
  ∀ (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)),
    ∀ x ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ c, coeff x.1 f * coeff x.2 g = 0
⊢ 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 h₁ : ∀ (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
Tactic: classical
  rw [degree_le_iff]
  intro c
  rw [← not_lt, mem_support_iff, not_imp_not]
  intro hc
  rw [coeff_mul]
  apply Finset.sum_eq_zero
  rintro ⟨d, e⟩ hde
  simp only [Finset.mem_antidiagonal] at hde
  dsimp only
  by_cases hd : m.degree f ≺[m] d
  · rw [m.coeff_eq_zero_of_lt hd, zero_mul]
  · suffices m.degree g ≺[m] e by
      rw [m.coeff_eq_zero_of_lt this, mul_zero]
    simp only [not_lt] at hd
    apply lt_of_add_lt_add_left (a := m.toSyn d)
    grw [← map_add _ _ e, hd, ← map_add, hde]
    exact hc
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
rw rw₁ rw₂ 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)
rw₄ rw₅ :
  ∀ (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
rw₆ :
  ∀ (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
h :
  ∀ (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)),
    ∀ x ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ c, coeff x.1 f * coeff x.2 g = 0
h₁ :
  ∀ (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
⊢ 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 h₂ : ∀ (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
Tactic: classical
  rw [degree_le_iff]
  intro c
  rw [← not_lt, mem_support_iff, not_imp_not]
  intro hc
  rw [coeff_mul]
  apply Finset.sum_eq_zero
  rintro ⟨d, e⟩ hde
  simp only [Finset.mem_antidiagonal] at hde
  dsimp only
  by_cases hd : m.degree f ≺[m] d
  · rw [m.coeff_eq_zero_of_lt hd, zero_mul]
  · suffices m.degree g ≺[m] e by
      rw [m.coeff_eq_zero_of_lt this, mul_zero]
    simp only [not_lt] at hd
    apply lt_of_add_lt_add_left (a := m.toSyn d)
    grw [← map_add _ _ e, hd, ← map_add, hde]
    exact hc
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
rw rw₁ rw₂ 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)
rw₄ rw₅ :
  ∀ (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
rw₆ :
  ∀ (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
h :
  ∀ (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)),
    ∀ x ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ c, coeff x.1 f * coeff x.2 g = 0
h₁ :
  ∀ (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
h₂ :
  ∀ (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
⊢ 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 h₃ : ∀ (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
Tactic: classical
  rw [degree_le_iff]
  intro c
  rw [← not_lt, mem_support_iff, not_imp_not]
  intro hc
  rw [coeff_mul]
  apply Finset.sum_eq_zero
  rintro ⟨d, e⟩ hde
  simp only [Finset.mem_antidiagonal] at hde
  dsimp only
  by_cases hd : m.degree f ≺[m] d
  · rw [m.coeff_eq_zero_of_lt hd, zero_mul]
  · suffices m.degree g ≺[m] e by
      rw [m.coeff_eq_zero_of_lt this, mul_zero]
    simp only [not_lt] at hd
    apply lt_of_add_lt_add_left (a := m.toSyn d)
    grw [← map_add _ _ e, hd, ← map_add, hde]
    exact hc
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
rw rw₁ rw₂ 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)
rw₄ rw₅ :
  ∀ (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
rw₆ :
  ∀ (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
h :
  ∀ (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)),
    ∀ x ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ c, coeff x.1 f * coeff x.2 g = 0
h₁ :
  ∀ (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
h₂ :
  ∀ (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
h₃ :
  ∀ (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
⊢ 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 pos : ∀ (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
Tactic: classical
  rw [degree_le_iff]
  intro c
  rw [← not_lt, mem_support_iff, not_imp_not]
  intro hc
  rw [coeff_mul]
  apply Finset.sum_eq_zero
  rintro ⟨d, e⟩ hde
  simp only [Finset.mem_antidiagonal] at hde
  dsimp only
  by_cases hd : m.degree f ≺[m] d
  · rw [m.coeff_eq_zero_of_lt hd, zero_mul]
  · suffices m.degree g ≺[m] e by
      rw [m.coeff_eq_zero_of_lt this, mul_zero]
    simp only [not_lt] at hd
    apply lt_of_add_lt_add_left (a := m.toSyn d)
    grw [← map_add _ _ e, hd, ← map_add, hde]
    exact hc
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
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)
⊢ coeff (a + b) (f * g) = coeff a f * coeff b g
have h₀ : ∀ b_1 ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ (a + b), b_1 ≠ (a, b) → coeff b_1.1 f * coeff b_1.2 g = 0
Tactic: rw [coeff_mul, Finset.sum_eq_single (a, b)]
-- 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
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)
h₀ : ∀ b_1 ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ (a + b), b_1 ≠ (a, b) → coeff b_1.1 f * coeff b_1.2 g = 0
⊢ coeff (a + b) (f * g) = coeff a f * coeff b g
have h₁ : (a, b) ∉ @Finset.antidiagonal _ Finsupp.instAddMonoid _ (a + b) → coeff (a, b).1 f * coeff (a, b).2 g = 0
Tactic: rw [coeff_mul, Finset.sum_eq_single (a, b)]
-- 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
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 : σ →₀ ℕ
hcd : (c, d) ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ (a + b)
h : (c, d) ≠ (a, b)
⊢ coeff (c, d).1 f * coeff (c, d).2 g = 0
have hcd₁ : c + d = a + b
Tactic: simp only [Finset.mem_antidiagonal] at hcd
Cleared hypotheses: hcd
-- 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
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
⊢ coeff (c, d).1 f * coeff (c, d).2 g = 0
have pos : ∀
  (hf :
    LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)),
  coeff (c, d).1 f * coeff (c, d).2 g = 0
Tactic: by_cases hf : m.degree f ≺[m] c
-- 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
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
pos :
  ∀
    (hf :
      LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)),
    coeff (c, d).1 f * coeff (c, d).2 g = 0
⊢ coeff (c, d).1 f * coeff (c, d).2 g = 0
have neg : ∀
  (hf :
    ¬LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)),
  coeff (c, d).1 f * coeff (c, d).2 g = 0
Tactic: by_cases hf : m.degree f ≺[m] c