-- 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
this : ∀ (f g : MvPolynomial σ R), m.degree g - m.degree f = m.degree f ⊔ m.degree g - m.degree f
rw :
  HMul.hMul (α := MvPolynomial σ R)
        ((monomial (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) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) : MvPolynomial σ R) g =
    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
rw₁ :
  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) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) : MvPolynomial σ R) g =
    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
rw₂ :
  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 g ⊔ m.degree f - m.degree g) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) :
          MvPolynomial σ R)
        g =
    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.sPolynomial f g =
    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
have rw₃ : HMul.hMul (α := MvPolynomial σ R)
      ((monomial (m.degree g ⊔ m.degree f - m.degree f) : (a : R) → MvPolynomial σ R) (m.leadingCoeff g) :
        MvPolynomial σ R)
      f -
    HMul.hMul (α := MvPolynomial σ R)
      ((monomial (m.degree g ⊔ m.degree f - m.degree g) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) :
        MvPolynomial σ R)
      g =
  HMul.hMul (α := MvPolynomial σ R)
      ((monomial (m.degree g ⊔ m.degree f - m.degree f) : (a : R) → MvPolynomial σ R) (m.leadingCoeff g) :
        MvPolynomial σ R)
      f -
    HMul.hMul (α := MvPolynomial σ R)
      ((monomial (m.degree g ⊔ m.degree f - m.degree g) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) :
        MvPolynomial σ R)
      g
Tactic: rw [sPolynomial, this, this, sup_comm]