-- 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
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
inr :
  m.sPolynomial ((monomial d₁ : (a : R) → MvPolynomial σ R) 0 * p₁)
      (HMul.hMul (α := MvPolynomial σ R) ((monomial d₂ : (a : R) → MvPolynomial σ R) c₂ : MvPolynomial σ R) p₂) =
    HMul.hMul (α := MvPolynomial σ R)
      ((monomial
              (m.degree ((monomial d₁ : (a : R) → MvPolynomial σ R) 0 * 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)
          (0 * c₂) :
        MvPolynomial σ R)
      (m.sPolynomial p₁ p₂)
inr₁ :
  m.sPolynomial
      (HMul.hMul (α := MvPolynomial σ R) ((monomial d₁ : (a : R) → MvPolynomial σ R) c₁ : MvPolynomial σ R) p₁)
      ((monomial d₂ : (a : R) → MvPolynomial σ R) 0 * p₂) =
    HMul.hMul (α := MvPolynomial σ R)
      ((monomial
              (m.degree
                    (HMul.hMul (α := MvPolynomial σ R)
                      ((monomial d₁ : (a : R) → MvPolynomial σ R) c₁ : MvPolynomial σ R) p₁) ⊔
                  m.degree ((monomial d₂ : (a : R) → MvPolynomial σ R) 0 * p₂) -
                m.degree p₁ ⊔ m.degree p₂) :
            (a : R) → MvPolynomial σ R)
          (c₁ * 0) :
        MvPolynomial σ R)
      (m.sPolynomial p₁ p₂)
inr₂ :
  m.sPolynomial
      (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((monomial d₁ : (a : R) → MvPolynomial σ R) c₁ : MvPolynomial σ R) (0 : 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) (β := MvPolynomial σ R)
                      ((monomial d₁ : (a : R) → MvPolynomial σ R) c₁ : MvPolynomial σ R) (0 : MvPolynomial σ R)) ⊔
                  m.degree
                    (HMul.hMul (α := MvPolynomial σ R)
                      ((monomial d₂ : (a : R) → MvPolynomial σ R) c₂ : MvPolynomial σ R) p₂) -
                degree.{u_1, u_2, u_3} m (R := R) 0 ⊔ m.degree p₂) :
            (a : R) → MvPolynomial σ R)
          (c₁ * c₂) :
        MvPolynomial σ R)
      (m.sPolynomial 0 p₂)
inr₃ :
  m.sPolynomial
      (HMul.hMul (α := MvPolynomial σ R) ((monomial d₁ : (a : R) → MvPolynomial σ R) c₁ : MvPolynomial σ R) p₁)
      (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((monomial d₂ : (a : R) → MvPolynomial σ R) c₂ : MvPolynomial σ R) (0 : MvPolynomial σ R)) =
    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) (β := MvPolynomial σ R)
                      ((monomial d₂ : (a : R) → MvPolynomial σ R) c₂ : MvPolynomial σ R) (0 : MvPolynomial σ R)) -
                m.degree p₁ ⊔ degree.{u_1, u_2, u_3} m (R := R) 0) :
            (a : R) → MvPolynomial σ R)
          (c₁ * c₂) :
        MvPolynomial σ R)
      (m.sPolynomial 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₂)

Tactic:
obtain rfl | rfl | rfl | rfl := H

Premises used: rfl