-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ_1 : Type u_1
m_1 : MonomialOrder.{u_1, u_3} σ_1
R_1 : Type u_2
inst : CommRing R_1
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst_1 : CommRing R
inst_2 : NoZeroDivisors R
p₁ p₂ : MvPolynomial σ R
d₁ d₂ : σ →₀ ℕ
c₁ c₂ : R
hc1 : c₁ ≠ 0
hc2 : c₂ ≠ 0
hp1 : p₁ ≠ 0
hp2 : p₂ ≠ 0
hm1 :
  ¬Eq (α := MvPolynomial σ R) ((monomial d₁ : (a : R) → MvPolynomial σ R) c₁ : MvPolynomial σ R) (0 : MvPolynomial σ R)
hm2 :
  ¬Eq (α := MvPolynomial σ R) ((monomial d₂ : (a : R) → MvPolynomial σ R) c₂ : MvPolynomial σ R) (0 : MvPolynomial σ R)
rw :
  HMul.hMul (α := MvPolynomial σ R)
        ((monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - (d₁ + m.degree p₁) + d₁) : (a : R) → MvPolynomial σ R)
            (c₁ * c₂ * m.leadingCoeff p₂) :
          MvPolynomial σ R)
        p₁ -
      HMul.hMul (α := MvPolynomial σ R)
        ((monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - (d₂ + m.degree p₂) + d₂) : (a : R) → MvPolynomial σ R)
            (c₁ * c₂ * m.leadingCoeff p₁) :
          MvPolynomial σ R)
        p₂ =
    HMul.hMul (α := MvPolynomial σ R)
        ((monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁) : (a : R) → MvPolynomial σ R)
            (c₁ * c₂ * m.leadingCoeff p₂) :
          MvPolynomial σ R)
        p₁ -
      HMul.hMul (α := MvPolynomial σ R)
        ((monomial
                ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂ +
                  (m.degree p₁ ⊔ m.degree p₂ - m.degree p₂)) :
              (a : R) → MvPolynomial σ R)
            (c₁ * c₂ * m.leadingCoeff p₁) :
          MvPolynomial σ R)
        p₂
rw₁ :
  HMul.hMul (α := MvPolynomial σ R)
        ((monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - (d₁ + m.degree p₁) + d₁) : (a : R) → MvPolynomial σ R)
            (c₁ * c₂ * m.leadingCoeff p₂) :
          MvPolynomial σ R)
        p₁ -
      HMul.hMul (α := MvPolynomial σ R)
        ((monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - (d₂ + m.degree p₂) + d₂) : (a : R) → MvPolynomial σ R)
            (c₁ * c₂ * m.leadingCoeff p₁) :
          MvPolynomial σ R)
        p₂ =
    HMul.hMul (α := MvPolynomial σ R)
        ((monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁) : (a : R) → MvPolynomial σ R)
            (c₁ * c₂ * m.leadingCoeff p₂) :
          MvPolynomial σ R)
        p₁ -
      HMul.hMul (α := MvPolynomial σ R)
        ((monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₂) : (a : R) → MvPolynomial σ R)
            (c₁ * c₂ * m.leadingCoeff p₁) :
          MvPolynomial σ R)
        p₂
rw₂ :
  HMul.hMul (α := MvPolynomial σ R)
        ((monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) + d₁ - (d₁ + m.degree p₁)) : (a : R) → MvPolynomial σ R)
            (c₁ * c₂ * m.leadingCoeff p₂) :
          MvPolynomial σ R)
        p₁ -
      HMul.hMul (α := MvPolynomial σ R)
        ((monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - (d₂ + m.degree p₂) + d₂) : (a : R) → MvPolynomial σ R)
            (c₁ * c₂ * m.leadingCoeff p₁) :
          MvPolynomial σ R)
        p₂ =
    HMul.hMul (α := MvPolynomial σ R)
        ((monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁) : (a : R) → MvPolynomial σ R)
            (c₁ * c₂ * m.leadingCoeff p₂) :
          MvPolynomial σ R)
        p₁ -
      HMul.hMul (α := MvPolynomial σ R)
        ((monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₂) : (a : R) → MvPolynomial σ R)
            (c₁ * c₂ * m.leadingCoeff p₁) :
          MvPolynomial σ R)
        p₂
⊢ HMul.hMul (α := MvPolynomial σ R)
        ((monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - (d₁ + m.degree p₁) + d₁) : (a : R) → MvPolynomial σ R)
            (c₁ * c₂ * m.leadingCoeff p₂) :
          MvPolynomial σ R)
        p₁ -
      HMul.hMul (α := MvPolynomial σ R)
        ((monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - (d₂ + m.degree p₂) + d₂) : (a : R) → MvPolynomial σ R)
            (c₁ * c₂ * m.leadingCoeff p₁) :
          MvPolynomial σ R)
        p₂ =
    HMul.hMul (α := MvPolynomial σ R)
        ((monomial
                ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂ +
                  (m.degree p₁ ⊔ m.degree p₂ - m.degree p₁)) :
              (a : R) → MvPolynomial σ R)
            (c₁ * c₂ * m.leadingCoeff p₂) :
          MvPolynomial σ R)
        p₁ -
      HMul.hMul (α := MvPolynomial σ R)
        ((monomial
                ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂ +
                  (m.degree p₁ ⊔ m.degree p₂ - m.degree p₂)) :
              (a : R) → MvPolynomial σ R)
            (c₁ * c₂ * m.leadingCoeff p₁) :
          MvPolynomial σ R)
        p₂
have rw₃ : HMul.hMul (α := MvPolynomial σ R)
      ((monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) + d₁ - (d₁ + m.degree p₁)) : (a : R) → MvPolynomial σ R)
          (c₁ * c₂ * m.leadingCoeff p₂) :
        MvPolynomial σ R)
      p₁ -
    HMul.hMul (α := MvPolynomial σ R)
      ((monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) + d₂ - (d₂ + m.degree p₂)) : (a : R) → MvPolynomial σ R)
          (c₁ * c₂ * m.leadingCoeff p₁) :
        MvPolynomial σ R)
      p₂ =
  HMul.hMul (α := MvPolynomial σ R)
      ((monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁) : (a : R) → MvPolynomial σ R)
          (c₁ * c₂ * m.leadingCoeff p₂) :
        MvPolynomial σ R)
      p₁ -
    HMul.hMul (α := MvPolynomial σ R)
      ((monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₂) : (a : R) → MvPolynomial σ R)
          (c₁ * c₂ * m.leadingCoeff p₁) :
        MvPolynomial σ R)
      p₂
Tactic: rw [tsub_add_tsub_cancel (sup_le_sup (self_le_add_left _ _) (self_le_add_left _ _)) (by simp),
    tsub_add_tsub_cancel (sup_le_sup (self_le_add_left _ _) (self_le_add_left _ _)) (by simp),
    tsub_add_eq_add_tsub le_sup_left, tsub_add_eq_add_tsub le_sup_right,
    add_comm d₁, add_comm d₂, add_tsub_add_eq_tsub_right, add_tsub_add_eq_tsub_right]