awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂ 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₂)
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₂)
inr₂ :
  m.sPolynomial (m.leadingTerm p₁ * 0) (m.leadingTerm p₂ * q₂) =
    HMul.hMul (α := MvPolynomial σ R)
      ((monomial (m.degree (p₁ * 0) ⊔ m.degree (p₂ * q₂) - degree.{u_1, u_2, u_3} m (R := R) 0 ⊔ m.degree q₂) :
            (a : R) → MvPolynomial σ R)
          (m.leadingCoeff p₁ * m.leadingCoeff p₂) :
        MvPolynomial σ R)
      (m.sPolynomial 0 q₂)
inr₃ :
  m.sPolynomial (m.leadingTerm p₁ * q₁) (m.leadingTerm p₂ * 0) =
    HMul.hMul (α := MvPolynomial σ R)
      ((monomial (m.degree (p₁ * q₁) ⊔ m.degree (p₂ * 0) - m.degree q₁ ⊔ degree.{u_1, u_2, u_3} m (R := R) 0) :
            (a : R) → MvPolynomial σ R)
          (m.leadingCoeff p₁ * m.leadingCoeff p₂) :
        MvPolynomial σ R)
      (m.sPolynomial 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:
obtain rfl | rfl | rfl | rfl := H

Premises used: rfl
-- 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₂ 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₂)
⊢ 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:
simp
-- 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₁ 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₂)
⊢ 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:
simp
-- 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₂ 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₂)
⊢ m.sPolynomial (m.leadingTerm p₁ * 0) (m.leadingTerm p₂ * q₂) =
    HMul.hMul (α := MvPolynomial σ R)
      ((monomial (m.degree (p₁ * 0) ⊔ m.degree (p₂ * q₂) - degree.{u_1, u_2, u_3} m (R := R) 0 ⊔ m.degree q₂) :
            (a : R) → MvPolynomial σ R)
          (m.leadingCoeff p₁ * m.leadingCoeff p₂) :
        MvPolynomial σ R)
      (m.sPolynomial 0 q₂)

Tactic:
simp
-- 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₂ 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₂)
⊢ m.sPolynomial (m.leadingTerm p₁ * q₁) (m.leadingTerm p₂ * 0) =
    HMul.hMul (α := MvPolynomial σ R)
      ((monomial (m.degree (p₁ * q₁) ⊔ m.degree (p₂ * 0) - m.degree q₁ ⊔ degree.{u_1, u_2, u_3} m (R := R) 0) :
            (a : R) → MvPolynomial σ R)
          (m.leadingCoeff p₁ * m.leadingCoeff p₂) :
        MvPolynomial σ R)
      (m.sPolynomial q₁ 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
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₂ 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:
simp [H, leadingTerm, sPolynomial_monomial_mul, degree_mul]

Premises used: MonomialOrder.leadingTerm, MonomialOrder.sPolynomial_monomial_mul, MonomialOrder.degree_mul
-- 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₂ 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₂)
wlog! 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₂)
⊢ 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:
classical
  wlog! +distrib H : p₁ ≠ 0 ∧ p₂ ≠ 0 ∧ q₁ ≠ 0 ∧ q₂ ≠ 0
  · (obtain rfl | rfl | rfl | rfl := H) <;> simp
  simp [H, leadingTerm, sPolynomial_monomial_mul, degree_mul]

Premises used: MonomialOrder.leadingTerm, MonomialOrder.sPolynomial_monomial_mul, MonomialOrder.degree_mul, rfl
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
d : m.syn
ι : Type u_3
g : ι → MvPolynomial σ R
hd :
  ∀ (b : ι),
    Membership.mem (γ := Finset ι) ∅ b →
      (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b)) ∨ g b = 0
hfd : (m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ ∅, g b)) < d
⊢ ∃ (c : ι → ι → R),
    Eq (α := MvPolynomial σ R) (∑ b ∈ ∅, g b) (∑ b₁ ∈ ∅, ∑ b₂ ∈ ∅, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
d : m.syn
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
h :
  ∀ (hd : ∀ b ∈ B, (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b)) ∨ g b = 0)
    (hfd : (m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) < d),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
hd :
  ∀ b_1 ∈ insert b B,
    (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b_1)) = d ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0
hfd : (m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ insert b B, g b)) < d
pos :
  ∀ (hb0 : g b = 0),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ insert b B, g b)
        (∑ b₁ ∈ insert b B, ∑ b₂ ∈ insert b B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
neg :
  ∀ (hb0 : ¬g b = 0),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ insert b B, g b)
        (∑ b₁ ∈ insert b B, ∑ b₂ ∈ insert b B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
⊢ ∃ (c : ι → ι → R),
    Eq (α := MvPolynomial σ R) (∑ b ∈ insert b B, g b)
      (∑ b₁ ∈ insert b B, ∑ b₂ ∈ insert b B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))

Tactic:
by_cases hb0 : g b = 0
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
d : m.syn
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
h :
  ∀ (hd : ∀ b ∈ B, (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b)) ∨ g b = 0)
    (hfd : (m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) < d),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
hd :
  ∀ b_1 ∈ insert b B,
    (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b_1)) = d ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0
hfd : (m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ insert b B, g b)) < d
hb0 : g b = 0
⊢ ∃ (c : ι → ι → R),
    Eq (α := MvPolynomial σ R) (∑ b ∈ insert b B, g b)
      (∑ b₁ ∈ insert b B, ∑ b₂ ∈ insert b B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))

Tactic:
simp_all
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
d : m.syn
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
h :
  ∀ (hd : ∀ b ∈ B, (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b)) ∨ g b = 0)
    (hfd : (m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) < d),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
hd :
  ∀ b_1 ∈ insert b B,
    (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b_1)) = d ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0
hfd : (m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ insert b B, g b)) < d
hb0 : ¬g b = 0
⊢ (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b + ∑ b ∈ B, g b)) < d

Tactic:
simp only [Finset.sum_insert hb, Finset.mem_insert, forall_eq_or_imp, hb0, or_false]
        at hfd hd

Premises used: Finset.mem_insert, forall_eq_or_imp, or_false, Finset.sum_insert
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
d : m.syn
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
h :
  ∀ (hd : ∀ b ∈ B, (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b)) ∨ g b = 0)
    (hfd : (m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) < d),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
hd :
  ∀ b_1 ∈ insert b B,
    (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b_1)) = d ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0
hfd : (m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ insert b B, g b)) < d
hb0 : ¬g b = 0
hfd₁ : (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b + ∑ b ∈ B, g b)) < d
⊢ ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b))) ∧
    ∀ a ∈ B, (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g a)) = d ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0

Tactic:
simp only [Finset.sum_insert hb, Finset.mem_insert, forall_eq_or_imp, hb0, or_false]
        at hfd hd

Premises used: Finset.mem_insert, forall_eq_or_imp, or_false, Finset.sum_insert
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
d : m.syn
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
h :
  ∀ (hd : ∀ b ∈ B, (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b)) ∨ g b = 0)
    (hfd : (m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) < d),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
hd :
  ∀ b_1 ∈ insert b B,
    (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b_1)) = d ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0
hfd : (m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ insert b B, g b)) < d
hb0 : ¬g b = 0
⊢ (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b + ∑ b ∈ B, g b)) < d

Tactic:
simp? [Finset.sum_insert hb, hb0] at hfd hd says
      simp only [Finset.sum_insert hb, Finset.mem_insert, forall_eq_or_imp, hb0, or_false]
        at hfd hd

Premises used: Finset.mem_insert, forall_eq_or_imp, or_false, Finset.sum_insert
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
d : m.syn
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
h :
  ∀ (hd : ∀ b ∈ B, (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b)) ∨ g b = 0)
    (hfd : (m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) < d),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
hd :
  ∀ b_1 ∈ insert b B,
    (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b_1)) = d ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0
hfd : (m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ insert b B, g b)) < d
hb0 : ¬g b = 0
hfd₁ : (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b + ∑ b ∈ B, g b)) < d
⊢ ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b))) ∧
    ∀ a ∈ B, (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g a)) = d ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0

Tactic:
simp? [Finset.sum_insert hb, hb0] at hfd hd says
      simp only [Finset.sum_insert hb, Finset.mem_insert, forall_eq_or_imp, hb0, or_false]
        at hfd hd

Premises used: Finset.mem_insert, forall_eq_or_imp, or_false, Finset.sum_insert
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
d : m.syn
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
h :
  ∀ (hd : ∀ b ∈ B, (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b)) ∨ g b = 0)
    (hfd : (m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) < d),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
hb0 : ¬g b = 0
hfd : (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b + ∑ b ∈ B, g b)) < d
hd :
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b))) ∧
    ∀ a ∈ B, (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g a)) = d ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
⊢ IsUnit (m.leadingCoeff (g b))

Tactic:
obtain ⟨⟨rfl, isunit_gb⟩, hd⟩ := hd

Premises used: rfl
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
d : m.syn
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
h :
  ∀ (hd : ∀ b ∈ B, (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b)) ∨ g b = 0)
    (hfd : (m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) < d),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
hb0 : ¬g b = 0
hfd : (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b + ∑ b ∈ B, g b)) < d
hd :
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b))) ∧
    ∀ a ∈ B, (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g a)) = d ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
⊢ ∀
    (hd :
      ∀ b_1 ∈ B,
        Eq.{u_4 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b_1)) : m.syn)
              ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn) ∧
            IsUnit (m.leadingCoeff (g b_1)) ∨
          g b_1 = 0)
    (hfd :
      LT.lt.{u_4} (α := m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))

Tactic:
obtain ⟨⟨rfl, isunit_gb⟩, hd⟩ := hd

Premises used: rfl
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
d : m.syn
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
h :
  ∀ (hd : ∀ b ∈ B, (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b)) ∨ g b = 0)
    (hfd : (m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) < d),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
hb0 : ¬g b = 0
hfd : (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b + ∑ b ∈ B, g b)) < d
hd :
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b))) ∧
    ∀ a ∈ B, (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g a)) = d ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
h₁ :
  ∀
    (hd :
      ∀ b_1 ∈ B,
        Eq.{u_4 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b_1)) : m.syn)
              ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn) ∧
            IsUnit (m.leadingCoeff (g b_1)) ∨
          g b_1 = 0)
    (hfd :
      LT.lt.{u_4} (α := m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
⊢ LT.lt.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b + ∑ b ∈ B, g b)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)

Tactic:
obtain ⟨⟨rfl, isunit_gb⟩, hd⟩ := hd

Premises used: rfl
-- Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
d : m.syn
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
h :
  ∀ (hd : ∀ b ∈ B, (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b)) ∨ g b = 0)
    (hfd : (m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) < d),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
hb0 : ¬g b = 0
hfd : (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b + ∑ b ∈ B, g b)) < d
hd :
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b))) ∧
    ∀ a ∈ B, (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g a)) = d ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
h₁ :
  ∀
    (hd :
      ∀ b_1 ∈ B,
        Eq.{u_4 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b_1)) : m.syn)
              ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn) ∧
            IsUnit (m.leadingCoeff (g b_1)) ∨
          g b_1 = 0)
    (hfd :
      LT.lt.{u_4} (α := m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
hfd₁ :
  LT.lt.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b + ∑ b ∈ B, g b)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)
⊢ ∀ a ∈ B,
    Eq.{u_4 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g a)) : m.syn)
          ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn) ∧
        IsUnit (m.leadingCoeff (g a)) ∨
      g a = 0

Tactic:
obtain ⟨⟨rfl, isunit_gb⟩, hd⟩ := hd

Premises used: rfl