-- 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
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
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
neg neg₁ :
  ∀ (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
⊢ 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)

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

Premises used: MvPolynomial.mem_support_iff, MulZeroClass.zero_mul, Finset.sum_eq_zero, MonomialOrder.degree_le_iff, map_add, Finset.HasAntidiagonal.mem_antidiagonal, MonomialOrder.degree, not_lt, MvPolynomial.coeff_mul, not_imp_not