-- 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
inst_1 : NoZeroDivisors R
p₁ p₂ : MvPolynomial σ R
d₁ d₂ : σ →₀ ℕ
c₁ c₂ : R
⊢ m.sPolynomial
      (HMul.hMul (α := MvPolynomial σ R) ((monomial d₁ : (a : R) → MvPolynomial σ R) c₁ : MvPolynomial σ R) p₁)
      (HMul.hMul (α := MvPolynomial σ R) ((monomial d₂ : (a : R) → MvPolynomial σ R) c₂ : MvPolynomial σ R) p₂) =
    HMul.hMul (α := MvPolynomial σ R)
      ((monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂) : (a : R) → MvPolynomial σ R)
          (c₁ * c₂) :
        MvPolynomial σ R)
      (m.sPolynomial p₁ p₂)
have simp : HMul.hMul (α := MvPolynomial σ R)
      ((monomial
              (m.degree
                    (HMul.hMul (α := MvPolynomial σ R)
                      ((monomial d₁ : (a : R) → MvPolynomial σ R) c₁ : MvPolynomial σ R) p₁) ⊔
                  m.degree
                    (HMul.hMul (α := MvPolynomial σ R)
                      ((monomial d₂ : (a : R) → MvPolynomial σ R) c₂ : MvPolynomial σ R) p₂) -
                m.degree
                  (HMul.hMul (α := MvPolynomial σ R) ((monomial d₁ : (a : R) → MvPolynomial σ R) c₁ : MvPolynomial σ R)
                    p₁)) :
            (a : R) → MvPolynomial σ R)
          (m.leadingCoeff
            (HMul.hMul (α := MvPolynomial σ R) ((monomial d₂ : (a : R) → MvPolynomial σ R) c₂ : MvPolynomial σ R) p₂)) :
        MvPolynomial σ R)
      (HMul.hMul (α := MvPolynomial σ R) ((monomial d₁ : (a : R) → MvPolynomial σ R) c₁ : MvPolynomial σ R) p₁) -
    HMul.hMul (α := MvPolynomial σ R)
      ((monomial
              (m.degree
                    (HMul.hMul (α := MvPolynomial σ R)
                      ((monomial d₁ : (a : R) → MvPolynomial σ R) c₁ : MvPolynomial σ R) p₁) ⊔
                  m.degree
                    (HMul.hMul (α := MvPolynomial σ R)
                      ((monomial d₂ : (a : R) → MvPolynomial σ R) c₂ : MvPolynomial σ R) p₂) -
                m.degree
                  (HMul.hMul (α := MvPolynomial σ R) ((monomial d₂ : (a : R) → MvPolynomial σ R) c₂ : MvPolynomial σ R)
                    p₂)) :
            (a : R) → MvPolynomial σ R)
          (m.leadingCoeff
            (HMul.hMul (α := MvPolynomial σ R) ((monomial d₁ : (a : R) → MvPolynomial σ R) c₁ : MvPolynomial σ R) p₁)) :
        MvPolynomial σ R)
      (HMul.hMul (α := MvPolynomial σ R) ((monomial d₂ : (a : R) → MvPolynomial σ R) c₂ : MvPolynomial σ R) p₂) =
  HMul.hMul (α := MvPolynomial σ R)
    ((monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂) : (a : R) → MvPolynomial σ R)
        (c₁ * c₂) :
      MvPolynomial σ R)
    (HMul.hMul (α := MvPolynomial σ R)
        ((monomial (m.degree p₁ ⊔ m.degree p₂ - m.degree p₁) : (a : R) → MvPolynomial σ R) (m.leadingCoeff p₂) :
          MvPolynomial σ R)
        p₁ -
      HMul.hMul (α := MvPolynomial σ R)
        ((monomial (m.degree p₁ ⊔ m.degree p₂ - m.degree p₂) : (a : R) → MvPolynomial σ R) (m.leadingCoeff p₁) :
          MvPolynomial σ R)
        p₂)
Tactic: classical
  simp only [sPolynomial_def]
  wlog! +distrib H : c₁ ≠ 0 ∧ c₂ ≠ 0 ∧ p₁ ≠ 0 ∧ p₂ ≠ 0
  · (obtain rfl | rfl | rfl | rfl := H) <;> simp
  rcases H with ⟨hc1, hc2, hp1, hp2⟩
  have hm1 := (monomial_eq_zero (s := d₁)).not.mpr hc1
  have hm2 := (monomial_eq_zero (s := d₂)).not.mpr hc2
  simp_rw [m.degree_mul hm1 hp1, m.degree_mul hm2 hp2,
    mul_sub, ← mul_assoc _ _ p₁, ← mul_assoc _ _ p₂, monomial_mul,
    m.leadingCoeff_mul, m.leadingCoeff_monomial,
    degree_monomial, hc1, hc2, reduceIte, mul_right_comm, mul_comm c₂ c₁]
  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]