awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
Goal:
A : Type u_3
σ : Type u_4
inst : CommRing A
I : Ideal (MvPolynomial σ A)
d : MvPolynomial σ A
h :
  Eq (α := MvPolynomial σ A ⧸ I)
    ((Ideal.Quotient.mk I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) d : MvPolynomial σ A ⧸ I)
    (eval₂ (algebraMap A (MvPolynomial σ A ⧸ I))
        (fun (d : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) (X d)) d :
      MvPolynomial σ A ⧸ I)
h₁ :
  Eq (α := MvPolynomial σ A ⧸ I)
    ((Ideal.Quotient.mkₐ A I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) d : MvPolynomial σ A ⧸ I)
    (eval₂ (algebraMap A (MvPolynomial σ A ⧸ I))
        (fun (d : σ) ↦ (Ideal.Quotient.mkₐ A I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) (X d)) d :
      MvPolynomial σ A ⧸ I)
h₂ :
  Eq (α := MvPolynomial σ A ⧸ I)
    ((aeval fun (d : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) (X d) :
          (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I)
        d :
      MvPolynomial σ A ⧸ I)
    (eval₂ (algebraMap A (MvPolynomial σ A ⧸ I))
        (fun (d : σ) ↦
          (aeval fun (d : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) (X d) :
              (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I)
            (X d))
        d :
      MvPolynomial σ A ⧸ I)
⊢ 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
have h₃ : Eq (α := MvPolynomial σ A ⧸ I)
  ((aeval fun (d : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) (X d) :
        (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I)
      d :
    MvPolynomial σ A ⧸ I)
  (eval₂ (algebraMap A (MvPolynomial σ A ⧸ I))
      (fun (d : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) (X d)) d :
    MvPolynomial σ A ⧸ I)
Tactic: simp_rw [RingHom.toFun_eq_coe, ← Ideal.Quotient.mkₐ_eq_mk A, mkₐ_eq_aeval, aeval_X, aeval,
    AlgHom.coe_mk, coe_eval₂Hom]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
Goal:
A : Type u_3
σ : Type u_4
inst : CommRing A
I : Ideal (MvPolynomial σ A)
d : MvPolynomial σ A
h :
  Eq (α := MvPolynomial σ A ⧸ I)
    ((Ideal.Quotient.mk I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) d : MvPolynomial σ A ⧸ I)
    (eval₂ (algebraMap A (MvPolynomial σ A ⧸ I))
        (fun (d : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) (X d)) d :
      MvPolynomial σ A ⧸ I)
h₁ :
  Eq (α := MvPolynomial σ A ⧸ I)
    ((Ideal.Quotient.mkₐ A I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) d : MvPolynomial σ A ⧸ I)
    (eval₂ (algebraMap A (MvPolynomial σ A ⧸ I))
        (fun (d : σ) ↦ (Ideal.Quotient.mkₐ A I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) (X d)) d :
      MvPolynomial σ A ⧸ I)
h₂ :
  Eq (α := MvPolynomial σ A ⧸ I)
    ((aeval fun (d : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) (X d) :
          (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I)
        d :
      MvPolynomial σ A ⧸ I)
    (eval₂ (algebraMap A (MvPolynomial σ A ⧸ I))
        (fun (d : σ) ↦
          (aeval fun (d : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) (X d) :
              (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I)
            (X d))
        d :
      MvPolynomial σ A ⧸ I)
h₃ :
  Eq (α := MvPolynomial σ A ⧸ I)
    ((aeval fun (d : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) (X d) :
          (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I)
        d :
      MvPolynomial σ A ⧸ I)
    (eval₂ (algebraMap A (MvPolynomial σ A ⧸ I))
        (fun (d : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) (X d)) d :
      MvPolynomial σ A ⧸ I)
⊢ 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
have h₄ : Eq (α := MvPolynomial σ A ⧸ I)
  (({
          toRingHom :=
            eval₂Hom (algebraMap A (MvPolynomial σ A ⧸ I)) fun (d : σ) ↦
              (Ideal.Quotient.mk I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) (X d),
          commutes' := sorry } :
        (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I)
      d :
    MvPolynomial σ A ⧸ I)
  (eval₂ (algebraMap A (MvPolynomial σ A ⧸ I))
      (fun (d : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) (X d)) d :
    MvPolynomial σ A ⧸ I)
Tactic: simp_rw [RingHom.toFun_eq_coe, ← Ideal.Quotient.mkₐ_eq_mk A, mkₐ_eq_aeval, aeval_X, aeval,
    AlgHom.coe_mk, coe_eval₂Hom]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
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 '' insert 0 B)) (span (m.leadingTerm '' B))
have pos : ∀ (h : 0 ∈ B), Eq (α := Ideal (MvPolynomial σ R)) (span (m.leadingTerm '' insert 0 B)) (span (m.leadingTerm '' B))
Tactic: by_cases h : 0 ∈ B
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
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))
⊢ Eq (α := Ideal (MvPolynomial σ R)) (span (m.leadingTerm '' insert 0 B)) (span (m.leadingTerm '' B))
have neg : ∀ (h : 0 ∉ B), Eq (α := Ideal (MvPolynomial σ R)) (span (m.leadingTerm '' insert 0 B)) (span (m.leadingTerm '' B))
Tactic: by_cases h : 0 ∈ B
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
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))
have pos : Eq (α := Ideal (MvPolynomial σ R)) (span (m.leadingTerm '' B)) (span (m.leadingTerm '' B))
Tactic: rw [Set.insert_eq_of_mem h]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
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)
⊢ Eq (α := Ideal (MvPolynomial σ R)) (span (m.leadingTerm '' B))
    (span ((fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) '' B))
have 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))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
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))
⊢ Eq (α := Ideal (MvPolynomial σ R)) (span (m.leadingTerm '' B))
    (span ((fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) '' B))
have 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))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
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)
⊢ 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))
have a : B ⊆
  m.leadingTerm ⁻¹'
    (↑(span ((fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) '' B)) :
      Set (MvPolynomial σ R))
Tactic: rw [Ideal.span_le, Set.image_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
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)
⊢ 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))
have a : B ⊆
  (fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) ⁻¹'
    (↑(span (m.leadingTerm '' B)) : Set (MvPolynomial σ R))
Tactic: rw [Ideal.span_le, Set.image_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
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
⊢ p ∈
    m.leadingTerm ⁻¹'
      (↑(span
            ((fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) '' B)) :
        Set (MvPolynomial σ R))
have 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))
Tactic: rw [Set.mem_preimage, SetLike.mem_coe, ← C_mul_leadingCoeff_monomial_degree]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
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))
    ((MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1)
have h : (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1 =
  HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) (↑sorry.unit⁻¹ : R) : MvPolynomial σ R)
    (m.leadingTerm p)
Tactic: convert!
      (span <| m.leadingTerm '' B).mul_mem_left (MvPolynomial.C (hB p hp).unit⁻¹.val) <|
        subset_span ⟨p, hp, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
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
⊢ (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)
have h : (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1 =
  HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) (↑sorry.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))
Tactic: rw [← C_mul_leadingCoeff_monomial_degree, ← mul_assoc, ← map_mul,
      IsUnit.val_inv_mul, MvPolynomial.C_1, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
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))
⊢ (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)
have h₁ : (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1 =
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((MvPolynomial.C : (a : R) → MvPolynomial σ R) (↑sorry.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
Tactic: rw [← C_mul_leadingCoeff_monomial_degree, ← mul_assoc, ← map_mul,
      IsUnit.val_inv_mul, MvPolynomial.C_1, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
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
⊢ (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)
have h₂ : (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1 =
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
    ((MvPolynomial.C : (a : R) → MvPolynomial σ R) ((↑sorry.unit⁻¹ : R) * m.leadingCoeff p) : MvPolynomial σ R)
    ((MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
Tactic: rw [← C_mul_leadingCoeff_monomial_degree, ← mul_assoc, ← map_mul,
      IsUnit.val_inv_mul, MvPolynomial.C_1, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
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)
⊢ (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)
have 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)
Tactic: rw [← C_mul_leadingCoeff_monomial_degree, ← mul_assoc, ← map_mul,
      IsUnit.val_inv_mul, MvPolynomial.C_1, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
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)
⊢ (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)
have 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)
Tactic: rw [← C_mul_leadingCoeff_monomial_degree, ← mul_assoc, ← map_mul,
      IsUnit.val_inv_mul, MvPolynomial.C_1, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
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)
⊢ (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)
have h₅ : Eq (α := MvPolynomial σ R) ((MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1)
  ((MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1)
Tactic: rw [← C_mul_leadingCoeff_monomial_degree, ← mul_assoc, ← map_mul,
      IsUnit.val_inv_mul, MvPolynomial.C_1, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
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)
⊢ Eq (α := Ideal (MvPolynomial σ R)) (span (m.leadingTerm '' B))
    (span ((fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) '' B))
have 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))
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
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))
⊢ Eq (α := Ideal (MvPolynomial σ R)) (span (m.leadingTerm '' B))
    (span ((fun (p : MvPolynomial σ R) ↦ (MvPolynomial.monomial (m.degree p) : (a : R) → MvPolynomial σ R) 1) '' B))
have 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))
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]