awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (hypothesis)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f g : MvPolynomial σ R
hf : m.degree f = 0 ∧ m.degree g = 0
h₁ : m.degree f = 0
⊢ LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.sPolynomial f g)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f ⊔ m.degree g) : m.syn) ∨
    m.sPolynomial f g = 0
have h₂ : m.degree g = 0
Tactic: rcases hf with ⟨h₁, h₂⟩
Cleared hypotheses: hf
-- 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
f g : MvPolynomial σ R
h₁ : m.degree f = 0
h₂ : m.degree g = 0
⊢ LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.sPolynomial f g)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f ⊔ m.degree g) : m.syn) ∨
    m.sPolynomial f g = 0
have pos : m.sPolynomial f g = 0
Tactic: 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
f g : MvPolynomial σ R
h₁ : m.degree f = 0
h₂ : m.degree g = 0
⊢ m.sPolynomial f g = 0
have pos : HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff g) : MvPolynomial σ R) f -
    HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) : MvPolynomial σ R) g =
  0
Tactic: suffices C (m.leadingCoeff g) * f - C (m.leadingCoeff f) * g = 0 by simp_all [sPolynomial_def]
-- 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
f g : MvPolynomial σ R
h₁ : m.degree f = 0
h₂ : m.degree g = 0
⊢ HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff g) : MvPolynomial σ R) f -
      HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) : MvPolynomial σ R) g =
    0
have pos : HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff g) : MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) : MvPolynomial σ R) -
    HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) : MvPolynomial σ R) g =
  0
Tactic: nth_rewrite 1 [degree_eq_zero_iff.mp 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
f g : MvPolynomial σ R
h₁ : m.degree f = 0
h₂ : m.degree g = 0
⊢ HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff g) : MvPolynomial σ R)
        ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) : MvPolynomial σ R) -
      HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) : MvPolynomial σ R) g =
    0
have pos : HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff g) : MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) : MvPolynomial σ R) -
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f) : MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff g) : MvPolynomial σ R) =
  0
Tactic: nth_rewrite 2 [degree_eq_zero_iff.mp 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
f g : MvPolynomial σ R
hf : ¬(m.degree f = 0 ∧ m.degree g = 0)
⊢ LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.sPolynomial f g)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f ⊔ m.degree g) : m.syn) ∨
    m.sPolynomial f g = 0
have neg : ¬m.sPolynomial f g = 0 →
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.sPolynomial f g)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f ⊔ m.degree g) : m.syn)
Tactic: rw [or_iff_not_imp_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
f g : MvPolynomial σ R
hf : ¬(m.degree f = 0 ∧ m.degree g = 0)
hs : ¬m.sPolynomial f g = 0
⊢ LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.sPolynomial f g)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f ⊔ m.degree g) : m.syn)
have neg : Ne.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.sPolynomial f g)) : m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f ⊔ m.degree g) : m.syn)
Tactic: apply (m.degree_sPolynomial_le f g).lt_of_ne
-- 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
f g : MvPolynomial σ R
hf : ¬(m.degree f = 0 ∧ m.degree g = 0)
hs : ¬m.sPolynomial f g = 0
⊢ Ne.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.sPolynomial f g)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f ⊔ m.degree g) : m.syn)
have neg : m.degree (m.sPolynomial f g) ≠ m.degree f ⊔ m.degree g
Tactic: apply m.toSyn.injective.ne
-- 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
f g : MvPolynomial σ R
hf : ¬(m.degree f = 0 ∧ m.degree g = 0)
hs : ¬m.sPolynomial f g = 0
⊢ m.degree (m.sPolynomial f g) ≠ m.degree f ⊔ m.degree g
have neg : ∀ (hs : m.degree (m.sPolynomial f g) = m.degree f ⊔ m.degree g), m.sPolynomial f g = 0
Tactic: contrapose hs
Cleared hypotheses: hs
-- 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
f g : MvPolynomial σ R
hf : ¬(m.degree f = 0 ∧ m.degree g = 0)
hs : m.degree (m.sPolynomial f g) = m.degree f ⊔ m.degree g
⊢ m.sPolynomial f g = 0
have neg : coeff (m.degree (m.sPolynomial f g)) (m.sPolynomial f g) = 0
Tactic: rw [← m.coeff_degree_eq_zero_iff, hs, m.coeff_sPolynomial_sup_eq_zero]
-- 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
f g : MvPolynomial σ R
hf : ¬(m.degree f = 0 ∧ m.degree g = 0)
hs : m.degree (m.sPolynomial f g) = m.degree f ⊔ m.degree g
neg : coeff (m.degree (m.sPolynomial f g)) (m.sPolynomial f g) = 0
⊢ m.sPolynomial f g = 0
have neg₁ : coeff (m.degree f ⊔ m.degree g) (m.sPolynomial f g) = 0
Tactic: rw [← m.coeff_degree_eq_zero_iff, hs, m.coeff_sPolynomial_sup_eq_zero]
-- 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
f g : MvPolynomial σ R
hf : ¬(m.degree f = 0 ∧ m.degree g = 0)
hs : m.degree (m.sPolynomial f g) = m.degree f ⊔ m.degree g
neg : coeff (m.degree (m.sPolynomial f g)) (m.sPolynomial f g) = 0
neg₁ : coeff (m.degree f ⊔ m.degree g) (m.sPolynomial f g) = 0
⊢ m.sPolynomial f g = 0
have neg₂ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [← m.coeff_degree_eq_zero_iff, hs, m.coeff_sPolynomial_sup_eq_zero]
-- 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 ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂) : (a : R) → MvPolynomial σ R)
          (c₁ * c₂) :
        MvPolynomial σ R)
      (m.sPolynomial p₁ p₂)
have simp : 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: simp only [sPolynomial_def]
-- 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
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₂)
have hc1 : c₁ ≠ 0
Tactic: rcases H with ⟨hc1, hc2, hp1, hp2⟩
Cleared hypotheses: H
-- 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
H : c₁ ≠ 0 ∧ c₂ ≠ 0 ∧ p₁ ≠ 0 ∧ p₂ ≠ 0
hc1 : c₁ ≠ 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 hc2 : c₂ ≠ 0
Tactic: rcases H with ⟨hc1, hc2, hp1, hp2⟩
Cleared hypotheses: H
-- 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
H : c₁ ≠ 0 ∧ c₂ ≠ 0 ∧ p₁ ≠ 0 ∧ p₂ ≠ 0
hc1 : c₁ ≠ 0
hc2 : c₂ ≠ 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 hp1 : p₁ ≠ 0
Tactic: rcases H with ⟨hc1, hc2, hp1, hp2⟩
Cleared hypotheses: H
-- 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
H : c₁ ≠ 0 ∧ c₂ ≠ 0 ∧ p₁ ≠ 0 ∧ p₂ ≠ 0
hc1 : c₁ ≠ 0
hc2 : c₂ ≠ 0
hp1 : 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 hp2 : p₂ ≠ 0
Tactic: rcases H with ⟨hc1, hc2, hp1, hp2⟩
Cleared hypotheses: H