-- 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),
        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₂))
    (H : c₁ = 0 ∨ c₂ = 0 ∨ p₁ = 0 ∨ p₂ = 0),
    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₂)
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),
    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₂)
⊢ 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:
wlog! +distrib H : c₁ ≠ 0 ∧ c₂ ≠ 0 ∧ p₁ ≠ 0 ∧ p₂ ≠ 0