-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f g : MvPolynomial σ R
inr :
  ∀
    (this :
      ∀ {σ : Type u_1} {m : MonomialOrder.{u_1, u_3} σ} {R : Type u_2} [inst : CommRing R] (f g : MvPolynomial σ R)
        (h0 : f ≠ 0 ∧ g ≠ 0),
        LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.sPolynomial f g)) : m.syn)
          ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f ⊔ m.degree g) : m.syn))
    (h0 : f = 0 ∨ g = 0),
    LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.sPolynomial f g)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f ⊔ m.degree g) : m.syn)
wlog! wlog!₁ :
  ∀ {σ : Type u_1} {m : MonomialOrder.{u_1, u_3} σ} {R : Type u_2} [inst : CommRing R] (f g : MvPolynomial σ R)
    (h0 : f ≠ 0 ∧ g ≠ 0),
    LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.sPolynomial f g)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f ⊔ m.degree g) : m.syn)
wlog!₂ :
  ∀ {σ : Type u_1} {m : MonomialOrder.{u_1, u_3} σ} {R : Type u_2} [inst : CommRing R] (f g : MvPolynomial σ R)
    (h0 : f ≠ 0 ∧ g ≠ 0),
    LE.le.{u_3} (α := m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
          (m.degree
            (HMul.hMul (α := MvPolynomial σ R)
                ((monomial (m.degree f ⊔ m.degree g - m.degree f) : (a : R) → MvPolynomial σ R) (m.leadingCoeff g) :
                  MvPolynomial σ R)
                f -
              HMul.hMul (α := MvPolynomial σ R)
                ((monomial (m.degree f ⊔ m.degree g - m.degree g) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) :
                  MvPolynomial σ R)
                g)) :
        m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f ⊔ m.degree g) : m.syn)
wlog!₃ :
  ∀ {σ : Type u_1} {m : MonomialOrder.{u_1, u_3} σ} {R : Type u_2} [inst : CommRing R] (f g : MvPolynomial σ R)
    (h0 : f ≠ 0 ∧ g ≠ 0),
    LE.le.{u_3} (α := m.syn)
      (max
          ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
            (m.degree
              (HMul.hMul (α := MvPolynomial σ R)
                ((monomial (m.degree f ⊔ m.degree g - m.degree f) : (a : R) → MvPolynomial σ R) (m.leadingCoeff g) :
                  MvPolynomial σ R)
                f)))
          ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
            (m.degree
              (HMul.hMul (α := MvPolynomial σ R)
                ((monomial (m.degree f ⊔ m.degree g - m.degree g) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) :
                  MvPolynomial σ R)
                g))) :
        m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f ⊔ m.degree g) : m.syn)
wlog!₄ :
  ∀ {σ : Type u_1} {m : MonomialOrder.{u_1, u_3} σ} {R : Type u_2} [inst : CommRing R] (f g : MvPolynomial σ R)
    (h0 : f ≠ 0 ∧ g ≠ 0),
    LE.le.{u_3} (α := m.syn)
      (max
          ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
            (degree.{u_1, u_2, u_3} m (R := R)
                ((monomial (m.degree f ⊔ m.degree g - m.degree f) : (a : R) → MvPolynomial σ R) (m.leadingCoeff g)) +
              m.degree f))
          ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
            (degree.{u_1, u_2, u_3} m (R := R)
                ((monomial (m.degree f ⊔ m.degree g - m.degree g) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f)) +
              m.degree g)) :
        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 (m.sPolynomial f g)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f ⊔ m.degree g) : m.syn)

Tactic:
classical
  wlog! +distrib h0 : f ≠ 0 ∧ g ≠ 0
  · (obtain rfl | rfl := h0) <;> simp
  simp only [sPolynomial_def]
  apply degree_sub_le.trans
  apply (sup_le_sup degree_mul_le degree_mul_le).trans
  simp [degree_monomial, h0.1, h0.2, tsub_add_cancel_of_le, le_sup_left, le_sup_right]

Premises used: MonomialOrder.degree_monomial, sup_le_sup, MonomialOrder.degree_sub_le, le_sup_left, tsub_add_cancel_of_le, le_sup_right, MonomialOrder.degree_mul_le, MonomialOrder.sPolynomial_def, LE.le.trans, rfl