-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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
inr :
  ∀
    (this :
      ∀ {σ : Type u_1} {m : MonomialOrder.{u_1, u_3} σ} {R : Type u_2} [inst : CommRing R] [NoZeroDivisors R]
        (p₁ p₂ : MvPolynomial σ R) (d₁ d₂ : σ →₀ ℕ) (c₁ c₂ : R) (H : c₁ ≠ 0 ∧ c₂ ≠ 0 ∧ p₁ ≠ 0 ∧ p₂ ≠ 0),
        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
                    (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 p₁ ⊔ m.degree p₂) :
                  (a : R) → MvPolynomial σ R)
                (c₁ * c₂) :
              MvPolynomial σ R)
            (m.sPolynomial p₁ p₂))
    (H : c₁ = 0 ∨ c₂ = 0 ∨ p₁ = 0 ∨ p₂ = 0),
    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
                (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 p₁ ⊔ m.degree p₂) :
              (a : R) → MvPolynomial σ R)
            (c₁ * c₂) :
          MvPolynomial σ R)
        (m.sPolynomial p₁ p₂)
wlog! wlog!₁ :
  ∀ {σ : Type u_1} {m : MonomialOrder.{u_1, u_3} σ} {R : Type u_2} [inst : CommRing R] [NoZeroDivisors R]
    (p₁ p₂ : MvPolynomial σ R) (d₁ d₂ : σ →₀ ℕ) (c₁ c₂ : R) (H : c₁ ≠ 0 ∧ c₂ ≠ 0 ∧ p₁ ≠ 0 ∧ p₂ ≠ 0),
    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
                (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 p₁ ⊔ m.degree p₂) :
              (a : R) → MvPolynomial σ R)
            (c₁ * c₂) :
          MvPolynomial σ R)
        (m.sPolynomial p₁ p₂)
⊢ 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
              (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 p₁ ⊔ m.degree p₂) :
            (a : R) → MvPolynomial σ R)
          (c₁ * c₂) :
        MvPolynomial σ R)
      (m.sPolynomial p₁ p₂)

Tactic:
classical
  wlog! +distrib H : c₁ ≠ 0 ∧ c₂ ≠ 0 ∧ p₁ ≠ 0 ∧ p₂ ≠ 0
  · (obtain rfl | rfl | rfl | rfl := H) <;> simp
  simp [H, degree_mul, sPolynomial_monomial_mul, degree_monomial]

Premises used: MonomialOrder.degree_monomial, MonomialOrder.sPolynomial_monomial_mul, MonomialOrder.degree_mul, rfl