awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂)
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₂)
⊢ 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₁ * 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: obtain rfl | rfl | rfl | rfl := H
Cleared hypotheses: q₁, 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₂)
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₂)
⊢ 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 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: obtain rfl | rfl | rfl | rfl := H
Cleared hypotheses: q₂, 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
⊢ 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: 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]
-- 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: 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]
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_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
⊢ ∃ (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₂))
have 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₂))
Tactic: by_cases hb0 : g b = 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
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₂))
⊢ ∃ (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₂))
have 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₂))
Tactic: by_cases hb0 : g b = 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (hypothesis)
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₂))
have hfd₁ : (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
Cleared hypotheses: hd, hfd
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (hypothesis)
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
⊢ ∃ (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₂))
have 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
Tactic: simp only [Finset.sum_insert hb, Finset.mem_insert, forall_eq_or_imp, hb0, or_false]
        at hfd hd
Cleared hypotheses: hd, hfd
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (hypothesis)
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₂))
have hfd₁ : (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
Cleared hypotheses: hd, hfd
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (hypothesis)
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
⊢ ∃ (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₂))
have 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
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
Cleared hypotheses: hd, hfd
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (hypothesis)
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
⊢ ∃ (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₂))
have isunit_gb : IsUnit (m.leadingCoeff (g b))
Tactic: obtain ⟨⟨rfl, isunit_gb⟩, hd⟩ := hd
Cleared hypotheses: d, h, hfd, hd
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (hypothesis)
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))
⊢ ∃ (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₂))
have 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₂))
Tactic: obtain ⟨⟨rfl, isunit_gb⟩, hd⟩ := hd
Cleared hypotheses: d, h, hfd, hd
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (hypothesis)
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₂))
⊢ ∃ (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₂))
have 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)
Tactic: obtain ⟨⟨rfl, isunit_gb⟩, hd⟩ := hd
Cleared hypotheses: d, h, hfd, hd
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (hypothesis)
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)
⊢ ∃ (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₂))
have hd₁ : ∀ 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
Cleared hypotheses: d, h, hfd, hd