awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : ℕ
hn : n = 0
⊢ Eq (α := Submodule R (MvPolynomial σ R))
    (Submodule.restrictScalars R
      (HPow.hPow (α := Ideal (MvPolynomial σ R))
        (restrictSupportIdeal R (Set.preimage (β := ℕ) (⇑degree : (a : σ →₀ ℕ) → ℕ) (Set.Ici 1)) ⋯) n))
    (Submodule.restrictScalars R (restrictSupportIdeal R ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' Set.Ici n) ⋯))

Tactic:
simp [hn, Set.Ici_zero_eq_univ]

Premises used: Set.Ici_zero_eq_univ
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : ℕ
hn : ¬n = 0
neg :
  HPow.hPow (α := Submodule R (MvPolynomial σ R))
      (Submodule.restrictScalars R
        (restrictSupportIdeal R (Set.preimage (β := ℕ) (⇑degree : (a : σ →₀ ℕ) → ℕ) (Set.Ici 1)) ⋯))
      n =
    Submodule.restrictScalars R (restrictSupportIdeal R ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' Set.Ici n) ⋯)
⊢ Eq (α := Submodule R (MvPolynomial σ R))
    (Submodule.restrictScalars R
      (HPow.hPow (α := Ideal (MvPolynomial σ R))
        (restrictSupportIdeal R (Set.preimage (β := ℕ) (⇑degree : (a : σ →₀ ℕ) → ℕ) (Set.Ici 1)) ⋯) n))
    (Submodule.restrictScalars R (restrictSupportIdeal R ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' Set.Ici n) ⋯))

Tactic:
rw [Submodule.restrictScalars_pow hn]

Premises used: Submodule.restrictScalars_pow
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : ℕ
hn : ¬n = 0
⊢ HPow.hPow (α := Submodule R (MvPolynomial σ R))
      (Submodule.restrictScalars R
        (restrictSupportIdeal R (Set.preimage (β := ℕ) (⇑degree : (a : σ →₀ ℕ) → ℕ) (Set.Ici 1)) ⋯))
      n =
    Submodule.restrictScalars R (restrictSupportIdeal R ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' Set.Ici n) ⋯)

Tactic:
simp [← restrictSupport_nsmul, ← degree_preimage_nsmul, hn, Set.Ici_nsmul_eq]

Premises used: Set.Ici_nsmul_eq, MvPolynomial.restrictSupport_nsmul, Finsupp.degree_preimage_nsmul
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : ℕ
rw :
  Eq (α := Ideal (MvPolynomial σ R))
    (Submodule.span (MvPolynomial σ R)
      ((fun (x : σ →₀ ℕ) ↦ x.prod fun (x1 : σ) (x2 : ℕ) ↦ HPow.hPow (α := MvPolynomial σ R) (X x1) x2) ''
        {x : σ →₀ ℕ | (degree : (a : σ →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set σ) ⊆ Set.univ}))
    (Ideal.span
      ((fun (x : σ →₀ ℕ) ↦ (monomial x : (a : R) → MvPolynomial σ R) 1) ''
        Set.preimage (β := ℕ) (⇑degree : (a : σ →₀ ℕ) → ℕ) {n}))
⊢ HPow.hPow (α := Ideal (MvPolynomial σ R)) (idealOfVars σ R) n =
    Ideal.span
      ((fun (x : σ →₀ ℕ) ↦ (monomial x : (a : R) → MvPolynomial σ R) 1) ''
        Set.preimage (β := ℕ) (⇑degree : (a : σ →₀ ℕ) → ℕ) {n})

Tactic:
rw [idealOfVars, Ideal.span, Submodule.span_pow, ← Set.image_univ,
    image_pow_eq_finsuppProd_image]

Premises used: Set.image_univ, Submodule.span_pow, Ideal.span, MvPolynomial.idealOfVars, Finsupp.image_pow_eq_finsuppProd_image
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : ℕ
⊢ Eq (α := Ideal (MvPolynomial σ R))
    (Submodule.span (MvPolynomial σ R)
      ((fun (x : σ →₀ ℕ) ↦ x.prod fun (x1 : σ) (x2 : ℕ) ↦ HPow.hPow (α := MvPolynomial σ R) (X x1) x2) ''
        {x : σ →₀ ℕ | (degree : (a : σ →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set σ) ⊆ Set.univ}))
    (Ideal.span
      ((fun (x : σ →₀ ℕ) ↦ (monomial x : (a : R) → MvPolynomial σ R) 1) ''
        Set.preimage (β := ℕ) (⇑degree : (a : σ →₀ ℕ) → ℕ) {n}))

Tactic:
simp [monomial_eq, Set.preimage, degree]

Premises used: Finsupp.degree, Set.preimage, MvPolynomial.monomial_eq
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : ℕ
p : MvPolynomial σ R
rw :
  Membership.mem (γ := Ideal (MvPolynomial σ R)) (restrictSupportIdeal R ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' Set.Ici n) ⋯)
      p ↔
    ∀ x ∈ p.support, n ≤ (degree : (a : σ →₀ ℕ) → ℕ) x
⊢ p ∈ HPow.hPow (α := Ideal (MvPolynomial σ R)) (idealOfVars σ R) n ↔ ∀ x ∈ p.support, n ≤ (degree : (a : σ →₀ ℕ) → ℕ) x

Tactic:
rw [pow_idealOfVars]

Premises used: MvPolynomial.pow_idealOfVars
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : ℕ
p : MvPolynomial σ R
⊢ Membership.mem (γ := Ideal (MvPolynomial σ R)) (restrictSupportIdeal R ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' Set.Ici n) ⋯)
      p ↔
    ∀ x ∈ p.support, n ≤ (degree : (a : σ →₀ ℕ) → ℕ) x

Tactic:
simp [restrictSupportIdeal, mem_restrictSupport_iff, Set.subset_def]

Premises used: MvPolynomial.restrictSupportIdeal, Set.subset_def, MvPolynomial.mem_restrictSupport_iff
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : ℕ
p : MvPolynomial σ R
⊢ p ∈ HPow.hPow (α := Ideal (MvPolynomial σ R)) (idealOfVars σ R) n ↔
    ∀ (x : σ →₀ ℕ), (degree : (a : σ →₀ ℕ) → ℕ) x < n → coeff x p = 0

Tactic:
grind only [mem_pow_idealOfVars_iff, mem_support_iff]

Premises used: MvPolynomial.mem_support_iff, MvPolynomial.mem_pow_idealOfVars_iff
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : ℕ
x : σ →₀ ℕ
r : R
h : r ≠ 0
⊢ Membership.mem (α := MvPolynomial σ R) (HPow.hPow (α := Ideal (MvPolynomial σ R)) (idealOfVars σ R) n)
      ((monomial x : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
    n ≤ (degree : (a : σ →₀ ℕ) → ℕ) x

Tactic:
grind only [mem_pow_idealOfVars_iff, mem_support_iff, coeff_monomial]

Premises used: MvPolynomial.mem_support_iff, MvPolynomial.mem_pow_idealOfVars_iff, MvPolynomial.coeff_monomial
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : ℕ
x : σ →₀ ℕ
r : R
h : r ≠ 0
⊢ Membership.mem (α := MvPolynomial σ R) (HPow.hPow (α := Ideal (MvPolynomial σ R)) (idealOfVars σ R) n)
      ((monomial x : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
    n ≤ (degree : (a : σ →₀ ℕ) → ℕ) x

Tactic:
classical
  grind only [mem_pow_idealOfVars_iff, mem_support_iff, coeff_monomial]

Premises used: MvPolynomial.mem_support_iff, MvPolynomial.mem_pow_idealOfVars_iff, MvPolynomial.coeff_monomial
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : ℕ
r : R
pos :
  ∀ (h : r = 0),
    Membership.mem (α := MvPolynomial σ R) (HPow.hPow (α := Ideal (MvPolynomial σ R)) (idealOfVars σ R) n)
        ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
      r = 0 ∨ n = 0
neg :
  ∀ (h : ¬r = 0),
    Membership.mem (α := MvPolynomial σ R) (HPow.hPow (α := Ideal (MvPolynomial σ R)) (idealOfVars σ R) n)
        ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
      r = 0 ∨ n = 0
⊢ Membership.mem (α := MvPolynomial σ R) (HPow.hPow (α := Ideal (MvPolynomial σ R)) (idealOfVars σ R) n)
      ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
    r = 0 ∨ n = 0

Tactic:
by_cases h : r = 0
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : ℕ
r : R
h : r = 0
⊢ Membership.mem (α := MvPolynomial σ R) (HPow.hPow (α := Ideal (MvPolynomial σ R)) (idealOfVars σ R) n)
      ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
    r = 0 ∨ n = 0

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : ℕ
r : R
h : ¬r = 0
⊢ Membership.mem (α := MvPolynomial σ R) (HPow.hPow (α := Ideal (MvPolynomial σ R)) (idealOfVars σ R) n)
      ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
    r = 0 ∨ n = 0

Tactic:
simpa [h] using monomial_mem_pow_idealOfVars_iff (σ := σ) n 0 h

Premises used: MvPolynomial.monomial_mem_pow_idealOfVars_iff, OfNat.ofNat
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
A : Type u_3
σ : Type u_4
inst : CommRing A
I : Ideal (MvPolynomial σ A)
hf :
  ∀ (d : σ),
    Eq (α := MvPolynomial σ A ⧸ I)
      ((Ideal.Quotient.mkₐ A I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) (X d) : MvPolynomial σ A ⧸ I)
      ((aeval fun (d : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) (X d) :
            (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I)
          (X d) :
        MvPolynomial σ A ⧸ I)
⊢ Ideal.Quotient.mkₐ A I =
    aeval fun (d : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) (X d)

Tactic:
ext d
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
A : Type u_3
σ : Type u_4
inst : CommRing A
I : Ideal (MvPolynomial σ A)
d : σ
⊢ Eq (α := MvPolynomial σ A ⧸ I)
    ((Ideal.Quotient.mkₐ A I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) (X d) : MvPolynomial σ A ⧸ I)
    ((aeval fun (d : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) (X d) :
          (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I)
        (X d) :
      MvPolynomial σ A ⧸ I)

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
A : Type u_3
σ : Type u_4
inst : CommRing A
I : Ideal (MvPolynomial σ A)
h :
  ∀ (d : MvPolynomial σ A),
    OneHom.toFun
        (↑(↑(Ideal.Quotient.mk I) : MvPolynomial σ A →* MvPolynomial σ A ⧸ I) :
          OneHom (MvPolynomial σ A) (MvPolynomial σ A ⧸ I))
        d =
      eval₂ (algebraMap A (MvPolynomial σ A ⧸ I))
        (fun (d : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) (X d)) d
⊢ OneHom.toFun
      (↑(↑(Ideal.Quotient.mk I) : MvPolynomial σ A →* MvPolynomial σ A ⧸ I) :
        OneHom (MvPolynomial σ A) (MvPolynomial σ A ⧸ I)) =
    eval₂ (algebraMap A (MvPolynomial σ A ⧸ I)) fun (d : σ) ↦
      (Ideal.Quotient.mk I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) (X d)

Tactic:
ext d
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
m : MonomialOrder.{u_1, u_3} σ
B : Set (MvPolynomial σ R)
⊢ Eq (α := Ideal (MvPolynomial σ R)) (span (m.leadingTerm '' (B \ {0}))) (span (m.leadingTerm '' B))

Tactic:
m.image_leadingTerm_sdiff_singleton_zero B ▸ Ideal.span_sdiff_singleton_zero

Premises used: MonomialOrder.image_leadingTerm_sdiff_singleton_zero, Ideal.span_sdiff_singleton_zero, Eq.rec, Eq.symm
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
m : MonomialOrder.{u_1, u_3} σ
B : Set (MvPolynomial σ R)
pos : ∀ (h : 0 ∈ B), Eq (α := Ideal (MvPolynomial σ R)) (span (m.leadingTerm '' insert 0 B)) (span (m.leadingTerm '' B))
neg : ∀ (h : 0 ∉ B), Eq (α := Ideal (MvPolynomial σ R)) (span (m.leadingTerm '' insert 0 B)) (span (m.leadingTerm '' B))
⊢ Eq (α := Ideal (MvPolynomial σ R)) (span (m.leadingTerm '' insert 0 B)) (span (m.leadingTerm '' B))

Tactic:
by_cases h : 0 ∈ B
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
m : MonomialOrder.{u_1, u_3} σ
B : Set (MvPolynomial σ R)
h : 0 ∈ B
pos pos₁ : Eq (α := Ideal (MvPolynomial σ R)) (span (m.leadingTerm '' B)) (span (m.leadingTerm '' B))
⊢ Eq (α := Ideal (MvPolynomial σ R)) (span (m.leadingTerm '' insert 0 B)) (span (m.leadingTerm '' B))

Tactic:
rw [Set.insert_eq_of_mem h]

Premises used: Set.insert_eq_of_mem
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
m : MonomialOrder.{u_1, u_3} σ
B : Set (MvPolynomial σ R)
h : 0 ∉ B
⊢ Eq (α := Ideal (MvPolynomial σ R)) (span (m.leadingTerm '' insert 0 B)) (span (m.leadingTerm '' B))

Tactic:
simp [image_leadingTerm_insert_zero]

Premises used: MonomialOrder.image_leadingTerm_insert_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
m : MonomialOrder.{u_1, u_3} σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
a :
  LE.le (α := Ideal (MvPolynomial σ R)) (span (m.leadingTerm '' B))
    (span ((fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) '' B))
a₁ :
  LE.le (α := Ideal (MvPolynomial σ R))
    (span ((fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) '' B))
    (span (m.leadingTerm '' B))
⊢ Eq (α := Ideal (MvPolynomial σ R)) (span (m.leadingTerm '' B))
    (span ((fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) '' B))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
m : MonomialOrder.{u_1, u_3} σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
a :
  B ⊆
    m.leadingTerm ⁻¹'
      (↑(span
            ((fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) '' B)) :
        Set (MvPolynomial σ R))
⊢ LE.le (α := Ideal (MvPolynomial σ R)) (span (m.leadingTerm '' B))
    (span ((fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) '' B))

Tactic:
rw [Ideal.span_le, Set.image_subset_iff]

Premises used: Ideal.span_le, Set.image_subset_iff
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
m : MonomialOrder.{u_1, u_3} σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
a :
  B ⊆
    (fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) ⁻¹'
      (↑(span (m.leadingTerm '' B)) : Set (MvPolynomial σ R))
⊢ LE.le (α := Ideal (MvPolynomial σ R))
    (span ((fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) '' B))
    (span (m.leadingTerm '' B))

Tactic:
rw [Ideal.span_le, Set.image_subset_iff]

Premises used: Ideal.span_le, Set.image_subset_iff
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
m : MonomialOrder.{u_1, u_3} σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
p : MvPolynomial σ R
hp : p ∈ B
a :
  Membership.mem (γ := Ideal (MvPolynomial σ R))
    (span ((fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) '' B))
    (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((MvPolynomial.C : (a : R) → MvPolynomial σ R) (m.leadingCoeff p) : MvPolynomial σ R)
      ((MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R))
⊢ p ∈
    m.leadingTerm ⁻¹'
      (↑(span
            ((fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) '' B)) :
        Set (MvPolynomial σ R))

Tactic:
rw [Set.mem_preimage, SetLike.mem_coe, ← C_mul_leadingCoeff_monomial_degree]

Premises used: SetLike.mem_coe, MonomialOrder.C_mul_leadingCoeff_monomial_degree, Set.mem_preimage
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
m : MonomialOrder.{u_1, u_3} σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
p : MvPolynomial σ R
hp : p ∈ B
⊢ Membership.mem (γ := Ideal (MvPolynomial σ R))
    (span ((fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) '' B))
    (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((MvPolynomial.C : (a : R) → MvPolynomial σ R) (m.leadingCoeff p) : MvPolynomial σ R)
      ((MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R))

Tactic:
Ideal.mul_mem_left _ _ (Ideal.subset_span ⟨_, hp, rfl⟩)

Premises used: Ideal.subset_span, Set.Mem, And.intro, Exists.intro, Ideal.mul_mem_left, rfl
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
m : MonomialOrder.{u_1, u_3} σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
p : MvPolynomial σ R
hp : p ∈ B
⊢ Membership.mem (γ := Ideal (MvPolynomial σ R))
    (span ((fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) '' B))
    (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((MvPolynomial.C : (a : R) → MvPolynomial σ R) (m.leadingCoeff p) : MvPolynomial σ R)
      ((MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R))

Tactic:
exact Ideal.mul_mem_left _ _ (Ideal.subset_span ⟨_, hp, rfl⟩)
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
m : MonomialOrder.{u_1, u_3} σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
p : MvPolynomial σ R
hp : p ∈ B
⊢ Membership.mem (γ := Ideal (MvPolynomial σ R)) (span (m.leadingTerm '' B))
    (HMul.hMul (α := MvPolynomial σ R)
      ((MvPolynomial.C : (a : R) → MvPolynomial σ R) (↑⋯.unit⁻¹ : R) : MvPolynomial σ R) (m.leadingTerm p))

Tactic:
(span <| m.leadingTerm '' B).mul_mem_left (MvPolynomial.C (hB p hp).unit⁻¹.val) <|
        subset_span ⟨p, hp, rfl⟩

Premises used: Units.val, Ideal.subset_span, MonomialOrder.leadingTerm, Inv.inv, And.intro, Exists.intro, IsUnit.unit, Set.image, Ideal.span, Ideal.mul_mem_left, MvPolynomial.C, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
m : MonomialOrder.{u_1, u_3} σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
p : MvPolynomial σ R
hp : p ∈ B
h :
  (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1 =
    HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) (↑⋯.unit⁻¹ : R) : MvPolynomial σ R)
      (m.leadingTerm p)
⊢ Membership.mem (γ := Ideal (MvPolynomial σ R)) (span (m.leadingTerm '' B))
    ((MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1)

Tactic:
convert!
      (span <| m.leadingTerm '' B).mul_mem_left (MvPolynomial.C (hB p hp).unit⁻¹.val) <|
        subset_span ⟨p, hp, rfl⟩

Premises used: Units.val, MonomialOrder.leadingTerm, Inv.inv, IsUnit.unit, Set.image, Ideal.span, Ideal.mul_mem_left, MvPolynomial.C, DFunLike.coe
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
m : MonomialOrder.{u_1, u_3} σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
p : MvPolynomial σ R
hp : p ∈ B
h :
  (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1 =
    HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) (↑⋯.unit⁻¹ : R) : MvPolynomial σ R)
      (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((MvPolynomial.C : (a : R) → MvPolynomial σ R) (m.leadingCoeff p) : MvPolynomial σ R)
        ((MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R))
h₁ :
  (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1 =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((MvPolynomial.C : (a : R) → MvPolynomial σ R) (↑⋯.unit⁻¹ : R) : MvPolynomial σ R)
        ((MvPolynomial.C : (a : R) → MvPolynomial σ R) (m.leadingCoeff p) : MvPolynomial σ R) *
      (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1
h₂ :
  (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1 =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((MvPolynomial.C : (a : R) → MvPolynomial σ R) ((↑⋯.unit⁻¹ : R) * m.leadingCoeff p) : MvPolynomial σ R)
      ((MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
h₃ :
  (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1 =
    HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) 1)
      ((MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1)
h₄ :
  (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1 =
    HMul.hMul (α := MvPolynomial σ R) 1 ((MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1)
h₅ h₆ :
  Eq (α := MvPolynomial σ R) ((MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1)
    ((MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1)
⊢ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1 =
    HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) (↑⋯.unit⁻¹ : R) : MvPolynomial σ R)
      (m.leadingTerm p)

Tactic:
rw [← C_mul_leadingCoeff_monomial_degree, ← mul_assoc, ← map_mul,
      IsUnit.val_inv_mul, MvPolynomial.C_1, one_mul]

Premises used: mul_assoc, MvPolynomial.C_1, map_mul, IsUnit.val_inv_mul, MonomialOrder.C_mul_leadingCoeff_monomial_degree, one_mul
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
m : MonomialOrder.{u_1, u_3} σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
a :
  LE.le (α := Ideal (MvPolynomial σ R)) (span (m.leadingTerm '' B))
    (span ((fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) '' B))
a₁ :
  LE.le (α := Ideal (MvPolynomial σ R))
    (span ((fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) '' B))
    (span (m.leadingTerm '' B))
a₂ :
  ∀ ⦃p : MvPolynomial σ R⦄ (hp : p ∈ B),
    p ∈
      m.leadingTerm ⁻¹'
        (↑(span
              ((fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) ''
                B)) :
          Set (MvPolynomial σ R))
a₃ a₄ :
  ∀ ⦃p : MvPolynomial σ R⦄ (hp : p ∈ B),
    Membership.mem (γ := Set (MvPolynomial σ R))
      ((fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) ⁻¹'
        (↑(span (m.leadingTerm '' B)) : Set (MvPolynomial σ R)))
      p
⊢ Eq (α := Ideal (MvPolynomial σ R)) (span (m.leadingTerm '' B))
    (span ((fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) '' B))

Tactic:
classical
  apply le_antisymm
  all_goals
    rw [Ideal.span_le, Set.image_subset_iff]
    intro p hp
  · rw [Set.mem_preimage, SetLike.mem_coe, ← C_mul_leadingCoeff_monomial_degree]
    exact Ideal.mul_mem_left _ _ (Ideal.subset_span ⟨_, hp, rfl⟩)
  · rw [Set.mem_preimage, SetLike.mem_coe]
    convert!
      (span <| m.leadingTerm '' B).mul_mem_left (MvPolynomial.C (hB p hp).unit⁻¹.val) <|
        subset_span ⟨p, hp, rfl⟩
    rw [← C_mul_leadingCoeff_monomial_degree, ← mul_assoc, ← map_mul,
      IsUnit.val_inv_mul, MvPolynomial.C_1, one_mul]

Premises used: Ideal.span_le, mul_assoc, MvPolynomial.C_1, map_mul, le_antisymm, SetLike.mem_coe, Set.image_subset_iff, IsUnit.val_inv_mul, MonomialOrder.C_mul_leadingCoeff_monomial_degree, one_mul, Set.mem_preimage
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
m : MonomialOrder.{u_1, u_3} σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p) ∨ p = 0
rw :
  Eq (α := Ideal (MvPolynomial σ R)) (span (m.leadingTerm '' (B \ {0})))
    (span
      ((fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) '' (B \ {0})))
⊢ Eq (α := Ideal (MvPolynomial σ R)) (span (m.leadingTerm '' B))
    (span
      ((fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) '' (B \ {0})))

Tactic:
rw [← m.span_leadingTerm_sdiff_singleton_zero]

Premises used: MonomialOrder.span_leadingTerm_sdiff_singleton_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
m : MonomialOrder.{u_1, u_3} σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p) ∨ p = 0
hB₁ : ∀ p ∈ B \ {0}, IsUnit (m.leadingCoeff p)
⊢ Eq (α := Ideal (MvPolynomial σ R)) (span (m.leadingTerm '' (B \ {0})))
    (span
      ((fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) '' (B \ {0})))

Tactic:
apply span_leadingTerm_eq_span_monomial

Premises used: MonomialOrder.span_leadingTerm_eq_span_monomial
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
m : MonomialOrder.{u_1, u_3} σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p) ∨ p = 0
⊢ ∀ p ∈ B \ {0}, IsUnit (m.leadingCoeff p)

Tactic:
simp_intro .. [or_iff_not_imp_right.mp (hB _ _)]

Premises used: Classical.or_iff_not_imp_right, Iff.mp