awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (hypothesis)
Goal:
σ_1 : Type u_1
m_1 : MonomialOrder.{u_1, u_3} σ_1
R_1 : Type u_2
inst : CommRing R_1
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst_1 : CommRing R
inst_2 : NoZeroDivisors R
p₁ p₂ : MvPolynomial σ R
d₁ d₂ : σ →₀ ℕ
c₁ c₂ : R
hc1 : c₁ ≠ 0
hc2 : c₂ ≠ 0
hp1 : p₁ ≠ 0
hp2 : 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₂)
have hm1 : ¬Eq (α := MvPolynomial σ R) ((monomial d₁ : (a : R) → MvPolynomial σ R) c₁ : MvPolynomial σ R) (0 : MvPolynomial σ R)
Tactic: have hm1 := (monomial_eq_zero (s := d₁)).not.mpr hc1
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ_1 : Type u_1
m_1 : MonomialOrder.{u_1, u_3} σ_1
R_1 : Type u_2
inst : CommRing R_1
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst_1 : CommRing R
inst_2 : NoZeroDivisors R
p₁ p₂ : MvPolynomial σ R
d₁ d₂ : σ →₀ ℕ
c₁ c₂ : R
hc1 : c₁ ≠ 0
hc2 : c₂ ≠ 0
hp1 : p₁ ≠ 0
hp2 : p₂ ≠ 0
hm1 :
  ¬Eq (α := MvPolynomial σ R) ((monomial d₁ : (a : R) → MvPolynomial σ R) c₁ : MvPolynomial σ R) (0 : MvPolynomial σ R)
hm2 :
  ¬Eq (α := MvPolynomial σ R) ((monomial d₂ : (a : R) → MvPolynomial σ R) c₂ : MvPolynomial σ R) (0 : MvPolynomial σ R)
⊢ HMul.hMul (α := MvPolynomial σ R)
        ((monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - (d₁ + m.degree p₁) + d₁) : (a : R) → MvPolynomial σ R)
            (c₁ * c₂ * m.leadingCoeff p₂) :
          MvPolynomial σ R)
        p₁ -
      HMul.hMul (α := MvPolynomial σ R)
        ((monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - (d₂ + m.degree p₂) + d₂) : (a : R) → MvPolynomial σ R)
            (c₁ * c₂ * m.leadingCoeff p₁) :
          MvPolynomial σ R)
        p₂ =
    HMul.hMul (α := MvPolynomial σ R)
        ((monomial
                ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂ +
                  (m.degree p₁ ⊔ m.degree p₂ - m.degree p₁)) :
              (a : R) → MvPolynomial σ R)
            (c₁ * c₂ * m.leadingCoeff p₂) :
          MvPolynomial σ R)
        p₁ -
      HMul.hMul (α := MvPolynomial σ R)
        ((monomial
                ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂ +
                  (m.degree p₁ ⊔ m.degree p₂ - m.degree p₂)) :
              (a : R) → MvPolynomial σ R)
            (c₁ * c₂ * m.leadingCoeff p₁) :
          MvPolynomial σ R)
        p₂
have rw : HMul.hMul (α := MvPolynomial σ R)
      ((monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - (d₁ + m.degree p₁) + d₁) : (a : R) → MvPolynomial σ R)
          (c₁ * c₂ * m.leadingCoeff p₂) :
        MvPolynomial σ R)
      p₁ -
    HMul.hMul (α := MvPolynomial σ R)
      ((monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - (d₂ + m.degree p₂) + d₂) : (a : R) → MvPolynomial σ R)
          (c₁ * c₂ * m.leadingCoeff p₁) :
        MvPolynomial σ R)
      p₂ =
  HMul.hMul (α := MvPolynomial σ R)
      ((monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁) : (a : R) → MvPolynomial σ R)
          (c₁ * c₂ * m.leadingCoeff p₂) :
        MvPolynomial σ R)
      p₁ -
    HMul.hMul (α := MvPolynomial σ R)
      ((monomial
              ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂ +
                (m.degree p₁ ⊔ m.degree p₂ - m.degree p₂)) :
            (a : R) → MvPolynomial σ R)
          (c₁ * c₂ * m.leadingCoeff p₁) :
        MvPolynomial σ R)
      p₂
Tactic: 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]
-- 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
              (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₂)
have 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₂)
Tactic: wlog! +distrib H : c₁ ≠ 0 ∧ c₂ ≠ 0 ∧ p₁ ≠ 0 ∧ p₂ ≠ 0
-- 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
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₂)
have 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₂)
Tactic: obtain rfl | rfl | rfl | rfl := H
Cleared hypotheses: c₁, H
-- 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
              (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₂)
have 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₂)
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]
-- 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₂ q₁ q₂ : MvPolynomial σ R
⊢ m.sPolynomial (m.leadingTerm p₁ * q₁) (m.leadingTerm p₂ * q₂) =
    HMul.hMul (α := MvPolynomial σ R)
      ((monomial (m.degree (p₁ * q₁) ⊔ m.degree (p₂ * q₂) - m.degree q₁ ⊔ m.degree q₂) : (a : R) → MvPolynomial σ R)
          (m.leadingCoeff p₁ * m.leadingCoeff p₂) :
        MvPolynomial σ R)
      (m.sPolynomial q₁ q₂)
have inr : ∀
  (this :
    ∀ {σ : Type u_1} {m : MonomialOrder.{u_1, u_3} σ} {R : Type u_2} [inst : CommRing R] [NoZeroDivisors R]
      (p₁ p₂ q₁ q₂ : MvPolynomial σ R) (H : p₁ ≠ 0 ∧ p₂ ≠ 0 ∧ q₁ ≠ 0 ∧ q₂ ≠ 0),
      m.sPolynomial (m.leadingTerm p₁ * q₁) (m.leadingTerm p₂ * q₂) =
        HMul.hMul (α := MvPolynomial σ R)
          ((monomial (m.degree (p₁ * q₁) ⊔ m.degree (p₂ * q₂) - m.degree q₁ ⊔ m.degree q₂) : (a : R) → MvPolynomial σ R)
              (m.leadingCoeff p₁ * m.leadingCoeff p₂) :
            MvPolynomial σ R)
          (m.sPolynomial q₁ q₂))
  (H : p₁ = 0 ∨ p₂ = 0 ∨ q₁ = 0 ∨ q₂ = 0),
  m.sPolynomial (m.leadingTerm p₁ * q₁) (m.leadingTerm p₂ * q₂) =
    HMul.hMul (α := MvPolynomial σ R)
      ((monomial (m.degree (p₁ * q₁) ⊔ m.degree (p₂ * q₂) - m.degree q₁ ⊔ m.degree q₂) : (a : R) → MvPolynomial σ R)
          (m.leadingCoeff p₁ * m.leadingCoeff p₂) :
        MvPolynomial σ R)
      (m.sPolynomial q₁ q₂)
Tactic: wlog! +distrib H : p₁ ≠ 0 ∧ p₂ ≠ 0 ∧ q₁ ≠ 0 ∧ q₂ ≠ 0
-- 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₂ q₁ q₂ : MvPolynomial σ R
inr :
  ∀
    (this :
      ∀ {σ : Type u_1} {m : MonomialOrder.{u_1, u_3} σ} {R : Type u_2} [inst : CommRing R] [NoZeroDivisors R]
        (p₁ p₂ q₁ q₂ : MvPolynomial σ R) (H : p₁ ≠ 0 ∧ p₂ ≠ 0 ∧ q₁ ≠ 0 ∧ q₂ ≠ 0),
        m.sPolynomial (m.leadingTerm p₁ * q₁) (m.leadingTerm p₂ * q₂) =
          HMul.hMul (α := MvPolynomial σ R)
            ((monomial (m.degree (p₁ * q₁) ⊔ m.degree (p₂ * q₂) - m.degree q₁ ⊔ m.degree q₂) :
                  (a : R) → MvPolynomial σ R)
                (m.leadingCoeff p₁ * m.leadingCoeff p₂) :
              MvPolynomial σ R)
            (m.sPolynomial q₁ q₂))
    (H : p₁ = 0 ∨ p₂ = 0 ∨ q₁ = 0 ∨ q₂ = 0),
    m.sPolynomial (m.leadingTerm p₁ * q₁) (m.leadingTerm p₂ * q₂) =
      HMul.hMul (α := MvPolynomial σ R)
        ((monomial (m.degree (p₁ * q₁) ⊔ m.degree (p₂ * q₂) - m.degree q₁ ⊔ m.degree q₂) : (a : R) → MvPolynomial σ R)
            (m.leadingCoeff p₁ * m.leadingCoeff p₂) :
          MvPolynomial σ R)
        (m.sPolynomial q₁ q₂)
⊢ m.sPolynomial (m.leadingTerm p₁ * q₁) (m.leadingTerm p₂ * q₂) =
    HMul.hMul (α := MvPolynomial σ R)
      ((monomial (m.degree (p₁ * q₁) ⊔ m.degree (p₂ * q₂) - m.degree q₁ ⊔ m.degree q₂) : (a : R) → MvPolynomial σ R)
          (m.leadingCoeff p₁ * m.leadingCoeff p₂) :
        MvPolynomial σ R)
      (m.sPolynomial q₁ q₂)
have wlog! : ∀ {σ : Type u_1} {m : MonomialOrder.{u_1, u_3} σ} {R : Type u_2} [inst : CommRing R] [NoZeroDivisors R]
  (p₁ p₂ q₁ q₂ : MvPolynomial σ R) (H : p₁ ≠ 0 ∧ p₂ ≠ 0 ∧ q₁ ≠ 0 ∧ q₂ ≠ 0),
  m.sPolynomial (m.leadingTerm p₁ * q₁) (m.leadingTerm p₂ * q₂) =
    HMul.hMul (α := MvPolynomial σ R)
      ((monomial (m.degree (p₁ * q₁) ⊔ m.degree (p₂ * q₂) - m.degree q₁ ⊔ m.degree q₂) : (a : R) → MvPolynomial σ R)
          (m.leadingCoeff p₁ * m.leadingCoeff p₂) :
        MvPolynomial σ R)
      (m.sPolynomial q₁ q₂)
Tactic: wlog! +distrib H : p₁ ≠ 0 ∧ p₂ ≠ 0 ∧ q₁ ≠ 0 ∧ q₂ ≠ 0
Cleared hypotheses: inst_1, p₁, p₂, q₁, q₂
-- 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₂ q₁ q₂ : MvPolynomial σ R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder.{u_1, u_3} σ} {R : Type u_2} [inst : CommRing R] [NoZeroDivisors R]
    (p₁ p₂ q₁ q₂ : MvPolynomial σ R) (H : p₁ ≠ 0 ∧ p₂ ≠ 0 ∧ q₁ ≠ 0 ∧ q₂ ≠ 0),
    m.sPolynomial (m.leadingTerm p₁ * q₁) (m.leadingTerm p₂ * q₂) =
      HMul.hMul (α := MvPolynomial σ R)
        ((monomial (m.degree (p₁ * q₁) ⊔ m.degree (p₂ * q₂) - m.degree q₁ ⊔ m.degree q₂) : (a : R) → MvPolynomial σ R)
            (m.leadingCoeff p₁ * m.leadingCoeff p₂) :
          MvPolynomial σ R)
        (m.sPolynomial q₁ q₂)
H : p₁ = 0 ∨ p₂ = 0 ∨ q₁ = 0 ∨ q₂ = 0
⊢ m.sPolynomial (m.leadingTerm p₁ * q₁) (m.leadingTerm p₂ * q₂) =
    HMul.hMul (α := MvPolynomial σ R)
      ((monomial (m.degree (p₁ * q₁) ⊔ m.degree (p₂ * q₂) - m.degree q₁ ⊔ m.degree q₂) : (a : R) → MvPolynomial σ R)
          (m.leadingCoeff p₁ * m.leadingCoeff p₂) :
        MvPolynomial σ R)
      (m.sPolynomial q₁ q₂)
have inr : m.sPolynomial (m.leadingTerm 0 * q₁) (m.leadingTerm p₂ * q₂) =
  HMul.hMul (α := MvPolynomial σ R)
    ((monomial (m.degree (0 * q₁) ⊔ m.degree (p₂ * q₂) - m.degree q₁ ⊔ m.degree q₂) : (a : R) → MvPolynomial σ R)
        (m.leadingCoeff 0 * m.leadingCoeff p₂) :
      MvPolynomial σ R)
    (m.sPolynomial q₁ q₂)
Tactic: obtain rfl | rfl | rfl | rfl := H
Cleared hypotheses: p₁, H
-- 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₂ q₁ q₂ : MvPolynomial σ R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder.{u_1, u_3} σ} {R : Type u_2} [inst : CommRing R] [NoZeroDivisors R]
    (p₁ p₂ q₁ q₂ : MvPolynomial σ R) (H : p₁ ≠ 0 ∧ p₂ ≠ 0 ∧ q₁ ≠ 0 ∧ q₂ ≠ 0),
    m.sPolynomial (m.leadingTerm p₁ * q₁) (m.leadingTerm p₂ * q₂) =
      HMul.hMul (α := MvPolynomial σ R)
        ((monomial (m.degree (p₁ * q₁) ⊔ m.degree (p₂ * q₂) - m.degree q₁ ⊔ m.degree q₂) : (a : R) → MvPolynomial σ R)
            (m.leadingCoeff p₁ * m.leadingCoeff p₂) :
          MvPolynomial σ R)
        (m.sPolynomial q₁ q₂)
H : p₁ = 0 ∨ p₂ = 0 ∨ q₁ = 0 ∨ q₂ = 0
inr :
  m.sPolynomial (m.leadingTerm 0 * q₁) (m.leadingTerm p₂ * q₂) =
    HMul.hMul (α := MvPolynomial σ R)
      ((monomial (m.degree (0 * q₁) ⊔ m.degree (p₂ * q₂) - m.degree q₁ ⊔ m.degree q₂) : (a : R) → MvPolynomial σ R)
          (m.leadingCoeff 0 * m.leadingCoeff p₂) :
        MvPolynomial σ R)
      (m.sPolynomial q₁ q₂)
⊢ m.sPolynomial (m.leadingTerm p₁ * q₁) (m.leadingTerm p₂ * q₂) =
    HMul.hMul (α := MvPolynomial σ R)
      ((monomial (m.degree (p₁ * q₁) ⊔ m.degree (p₂ * q₂) - m.degree q₁ ⊔ m.degree q₂) : (a : R) → MvPolynomial σ R)
          (m.leadingCoeff p₁ * m.leadingCoeff p₂) :
        MvPolynomial σ R)
      (m.sPolynomial q₁ q₂)
have inr₁ : m.sPolynomial (m.leadingTerm p₁ * q₁) (m.leadingTerm 0 * q₂) =
  HMul.hMul (α := MvPolynomial σ R)
    ((monomial (m.degree (p₁ * q₁) ⊔ m.degree (0 * q₂) - m.degree q₁ ⊔ m.degree q₂) : (a : R) → MvPolynomial σ R)
        (m.leadingCoeff p₁ * m.leadingCoeff 0) :
      MvPolynomial σ R)
    (m.sPolynomial q₁ q₂)
Tactic: obtain rfl | rfl | rfl | rfl := H
Cleared hypotheses: p₂, H