-- 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 : 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)
⊢ 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)
have 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)
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]
Cleared hypotheses: f, g