Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p₁ p₂ : MvPolynomial σ R
d₁ d₂ : σ →₀ ℕ
c₁ c₂ : R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] [NoZeroDivisors R]
    (p₁ p₂ : MvPolynomial σ R) (d₁ d₂ : σ →₀ ℕ) (c₁ c₂ : R),
    c₁ ≠ 0 ∧ c₂ ≠ 0 ∧ p₁ ≠ 0 ∧ p₂ ≠ 0 →
      (monomial
                (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) -
                  m.degree ((monomial d₁) c₁ * p₁)))
              (m.leadingCoeff ((monomial d₂) c₂ * p₂)) *
            ((monomial d₁) c₁ * p₁) -
          (monomial
                (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) -
                  m.degree ((monomial d₂) c₂ * p₂)))
              (m.leadingCoeff ((monomial d₁) c₁ * p₁)) *
            ((monomial d₂) c₂ * p₂) =
        (monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂)) (c₁ * c₂) *
          ((monomial (m.degree p₁ ⊔ m.degree p₂ - m.degree p₁)) (m.leadingCoeff p₂) * p₁ -
            (monomial (m.degree p₁ ⊔ m.degree p₂ - m.degree p₂)) (m.leadingCoeff p₁) * p₂)
H : c₁ = 0 ∨ c₂ = 0 ∨ p₁ = 0 ∨ p₂ = 0
⊢ (monomial (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) - m.degree ((monomial d₁) c₁ * p₁)))
          (m.leadingCoeff ((monomial d₂) c₂ * p₂)) *
        ((monomial d₁) c₁ * p₁) -
      (monomial
            (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) - m.degree ((monomial d₂) c₂ * p₂)))
          (m.leadingCoeff ((monomial d₁) c₁ * p₁)) *
        ((monomial d₂) c₂ * p₂) =
    (monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂)) (c₁ * c₂) *
      ((monomial (m.degree p₁ ⊔ m.degree p₂ - m.degree p₁)) (m.leadingCoeff p₂) * p₁ -
        (monomial (m.degree p₁ ⊔ m.degree p₂ - m.degree p₂)) (m.leadingCoeff p₁) * p₂)

Tactic:
(obtain rfl | rfl | rfl | rfl := H)

Goal state after:
case inr.inl
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p₁ p₂ : MvPolynomial σ R
d₁ d₂ : σ →₀ ℕ
c₂ : R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] [NoZeroDivisors R]
    (p₁ p₂ : MvPolynomial σ R) (d₁ d₂ : σ →₀ ℕ) (c₁ c₂ : R),
    c₁ ≠ 0 ∧ c₂ ≠ 0 ∧ p₁ ≠ 0 ∧ p₂ ≠ 0 →
      (monomial
                (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) -
                  m.degree ((monomial d₁) c₁ * p₁)))
              (m.leadingCoeff ((monomial d₂) c₂ * p₂)) *
            ((monomial d₁) c₁ * p₁) -
          (monomial
                (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) -
                  m.degree ((monomial d₂) c₂ * p₂)))
              (m.leadingCoeff ((monomial d₁) c₁ * p₁)) *
            ((monomial d₂) c₂ * p₂) =
        (monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂)) (c₁ * c₂) *
          ((monomial (m.degree p₁ ⊔ m.degree p₂ - m.degree p₁)) (m.leadingCoeff p₂) * p₁ -
            (monomial (m.degree p₁ ⊔ m.degree p₂ - m.degree p₂)) (m.leadingCoeff p₁) * p₂)
⊢ (monomial (m.degree ((monomial d₁) 0 * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) - m.degree ((monomial d₁) 0 * p₁)))
          (m.leadingCoeff ((monomial d₂) c₂ * p₂)) *
        ((monomial d₁) 0 * p₁) -
      (monomial (m.degree ((monomial d₁) 0 * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) - m.degree ((monomial d₂) c₂ * p₂)))
          (m.leadingCoeff ((monomial d₁) 0 * p₁)) *
        ((monomial d₂) c₂ * p₂) =
    (monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂)) (0 * c₂) *
      ((monomial (m.degree p₁ ⊔ m.degree p₂ - m.degree p₁)) (m.leadingCoeff p₂) * p₁ -
        (monomial (m.degree p₁ ⊔ m.degree p₂ - m.degree p₂)) (m.leadingCoeff p₁) * p₂)

case inr.inr.inl
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p₁ p₂ : MvPolynomial σ R
d₁ d₂ : σ →₀ ℕ
c₁ : R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] [NoZeroDivisors R]
    (p₁ p₂ : MvPolynomial σ R) (d₁ d₂ : σ →₀ ℕ) (c₁ c₂ : R),
    c₁ ≠ 0 ∧ c₂ ≠ 0 ∧ p₁ ≠ 0 ∧ p₂ ≠ 0 →
      (monomial
                (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) -
                  m.degree ((monomial d₁) c₁ * p₁)))
              (m.leadingCoeff ((monomial d₂) c₂ * p₂)) *
            ((monomial d₁) c₁ * p₁) -
          (monomial
                (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) -
                  m.degree ((monomial d₂) c₂ * p₂)))
              (m.leadingCoeff ((monomial d₁) c₁ * p₁)) *
            ((monomial d₂) c₂ * p₂) =
        (monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂)) (c₁ * c₂) *
          ((monomial (m.degree p₁ ⊔ m.degree p₂ - m.degree p₁)) (m.leadingCoeff p₂) * p₁ -
            (monomial (m.degree p₁ ⊔ m.degree p₂ - m.degree p₂)) (m.leadingCoeff p₁) * p₂)
⊢ (monomial (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) 0 * p₂) - m.degree ((monomial d₁) c₁ * p₁)))
          (m.leadingCoeff ((monomial d₂) 0 * p₂)) *
        ((monomial d₁) c₁ * p₁) -
      (monomial (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) 0 * p₂) - m.degree ((monomial d₂) 0 * p₂)))
          (m.leadingCoeff ((monomial d₁) c₁ * p₁)) *
        ((monomial d₂) 0 * p₂) =
    (monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂)) (c₁ * 0) *
      ((monomial (m.degree p₁ ⊔ m.degree p₂ - m.degree p₁)) (m.leadingCoeff p₂) * p₁ -
        (monomial (m.degree p₁ ⊔ m.degree p₂ - m.degree p₂)) (m.leadingCoeff p₁) * p₂)

case inr.inr.inr.inl
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p₂ : MvPolynomial σ R
d₁ d₂ : σ →₀ ℕ
c₁ c₂ : R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] [NoZeroDivisors R]
    (p₁ p₂ : MvPolynomial σ R) (d₁ d₂ : σ →₀ ℕ) (c₁ c₂ : R),
    c₁ ≠ 0 ∧ c₂ ≠ 0 ∧ p₁ ≠ 0 ∧ p₂ ≠ 0 →
      (monomial
                (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) -
                  m.degree ((monomial d₁) c₁ * p₁)))
              (m.leadingCoeff ((monomial d₂) c₂ * p₂)) *
            ((monomial d₁) c₁ * p₁) -
          (monomial
                (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) -
                  m.degree ((monomial d₂) c₂ * p₂)))
              (m.leadingCoeff ((monomial d₁) c₁ * p₁)) *
            ((monomial d₂) c₂ * p₂) =
        (monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂)) (c₁ * c₂) *
          ((monomial (m.degree p₁ ⊔ m.degree p₂ - m.degree p₁)) (m.leadingCoeff p₂) * p₁ -
            (monomial (m.degree p₁ ⊔ m.degree p₂ - m.degree p₂)) (m.leadingCoeff p₁) * p₂)
⊢ (monomial (m.degree ((monomial d₁) c₁ * 0) ⊔ m.degree ((monomial d₂) c₂ * p₂) - m.degree ((monomial d₁) c₁ * 0)))
          (m.leadingCoeff ((monomial d₂) c₂ * p₂)) *
        ((monomial d₁) c₁ * 0) -
      (monomial (m.degree ((monomial d₁) c₁ * 0) ⊔ m.degree ((monomial d₂) c₂ * p₂) - m.degree ((monomial d₂) c₂ * p₂)))
          (m.leadingCoeff ((monomial d₁) c₁ * 0)) *
        ((monomial d₂) c₂ * p₂) =
    (monomial ((d₁ + m.degree 0) ⊔ (d₂ + m.degree p₂) - m.degree 0 ⊔ m.degree p₂)) (c₁ * c₂) *
      ((monomial (m.degree 0 ⊔ m.degree p₂ - m.degree 0)) (m.leadingCoeff p₂) * 0 -
        (monomial (m.degree 0 ⊔ m.degree p₂ - m.degree p₂)) (m.leadingCoeff 0) * p₂)

case inr.inr.inr.inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p₁ : MvPolynomial σ R
d₁ d₂ : σ →₀ ℕ
c₁ c₂ : R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] [NoZeroDivisors R]
    (p₁ p₂ : MvPolynomial σ R) (d₁ d₂ : σ →₀ ℕ) (c₁ c₂ : R),
    c₁ ≠ 0 ∧ c₂ ≠ 0 ∧ p₁ ≠ 0 ∧ p₂ ≠ 0 →
      (monomial
                (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) -
                  m.degree ((monomial d₁) c₁ * p₁)))
              (m.leadingCoeff ((monomial d₂) c₂ * p₂)) *
            ((monomial d₁) c₁ * p₁) -
          (monomial
                (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) -
                  m.degree ((monomial d₂) c₂ * p₂)))
              (m.leadingCoeff ((monomial d₁) c₁ * p₁)) *
            ((monomial d₂) c₂ * p₂) =
        (monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂)) (c₁ * c₂) *
          ((monomial (m.degree p₁ ⊔ m.degree p₂ - m.degree p₁)) (m.leadingCoeff p₂) * p₁ -
            (monomial (m.degree p₁ ⊔ m.degree p₂ - m.degree p₂)) (m.leadingCoeff p₁) * p₂)
⊢ (monomial (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * 0) - m.degree ((monomial d₁) c₁ * p₁)))
          (m.leadingCoeff ((monomial d₂) c₂ * 0)) *
        ((monomial d₁) c₁ * p₁) -
      (monomial (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * 0) - m.degree ((monomial d₂) c₂ * 0)))
          (m.leadingCoeff ((monomial d₁) c₁ * p₁)) *
        ((monomial d₂) c₂ * 0) =
    (monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree 0) - m.degree p₁ ⊔ m.degree 0)) (c₁ * c₂) *
      ((monomial (m.degree p₁ ⊔ m.degree 0 - m.degree p₁)) (m.leadingCoeff 0) * p₁ -
        (monomial (m.degree p₁ ⊔ m.degree 0 - m.degree 0)) (m.leadingCoeff p₁) * 0)