awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
⊢ Membership.mem (γ := Ideal (MvPolynomial σ R))
      (Ideal.span ((fun (s : σ →₀ ℕ) ↦ (monomial s : (a : R) → MvPolynomial σ R) 1) '' s)) x ↔
    ∀ xi ∈ x.support, ∃ si ∈ s, si ≤ xi
have refine : (∀ m ∈ x.support, ∃ m' ∈ s, ∃ (d : σ →₀ ℕ), m = d + m') ↔ ∀ xi ∈ x.support, ∃ si ∈ s, si ≤ xi
Tactic: refine AddMonoidAlgebra.mem_ideal_span_of'_image.trans ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
⊢ (∀ m ∈ x.support, ∃ m' ∈ s, ∃ (d : σ →₀ ℕ), m = d + m') ↔ ∀ xi ∈ x.support, ∃ si ∈ s, si ≤ xi
have simp_rw : (∀ m ∈ x.support, ∃ m' ∈ s, ∃ (d : σ →₀ ℕ), m = m' + d) ↔ ∀ xi ∈ x.support, ∃ si ∈ s, ∃ (c : σ →₀ ℕ), xi = si + c
Tactic: simp_rw [le_iff_exists_add, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
⊢ Membership.mem (γ := Ideal (MvPolynomial σ R))
      (Ideal.span ((fun (s : σ →₀ ℕ) ↦ (monomial s : (a : R) → MvPolynomial σ R) 1) '' s)) x ↔
    ∀ xi ∈ x.support,
      ∃ si ∈ s,
        Dvd.dvd (α := MvPolynomial σ R) ((monomial si : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
          ((monomial xi : (a : R) → MvPolynomial σ R) (coeff xi x) : MvPolynomial σ R)
have refine : ∀ (xi : σ →₀ ℕ) (hxi : xi ∈ x.support),
  (∃ si ∈ s, si ≤ xi) ↔
    ∃ si ∈ s,
      Dvd.dvd (α := MvPolynomial σ R) ((monomial si : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
        ((monomial xi : (a : R) → MvPolynomial σ R) (coeff xi x) : MvPolynomial σ R)
Tactic: refine mem_ideal_span_monomial_image.trans (forall₂_congr fun xi hxi => ?_)
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
xi : σ →₀ ℕ
hxi : xi ∈ x.support
⊢ (∃ si ∈ s, si ≤ xi) ↔
    ∃ si ∈ s,
      Dvd.dvd (α := MvPolynomial σ R) ((monomial si : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
        ((monomial xi : (a : R) → MvPolynomial σ R) (coeff xi x) : MvPolynomial σ R)
have simp_rw : (∃ si ∈ s, si ≤ xi) ↔ ∃ si ∈ s, (coeff xi x = 0 ∨ si ≤ xi) ∧ 1 ∣ coeff xi x
Tactic: simp_rw [monomial_dvd_monomial, one_dvd, and_true, mem_support_iff.mp hxi, false_or]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
xi : σ →₀ ℕ
hxi : xi ∈ x.support
simp_rw : (∃ si ∈ s, si ≤ xi) ↔ ∃ si ∈ s, (coeff xi x = 0 ∨ si ≤ xi) ∧ 1 ∣ coeff xi x
⊢ (∃ si ∈ s, si ≤ xi) ↔
    ∃ si ∈ s,
      Dvd.dvd (α := MvPolynomial σ R) ((monomial si : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
        ((monomial xi : (a : R) → MvPolynomial σ R) (coeff xi x) : MvPolynomial σ R)
have simp_rw₁ : (∃ si ∈ s, si ≤ xi) ↔ ∃ si ∈ s, (coeff xi x = 0 ∨ si ≤ xi) ∧ True
Tactic: simp_rw [monomial_dvd_monomial, one_dvd, and_true, mem_support_iff.mp hxi, false_or]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
xi : σ →₀ ℕ
hxi : xi ∈ x.support
simp_rw : (∃ si ∈ s, si ≤ xi) ↔ ∃ si ∈ s, (coeff xi x = 0 ∨ si ≤ xi) ∧ 1 ∣ coeff xi x
simp_rw₁ : (∃ si ∈ s, si ≤ xi) ↔ ∃ si ∈ s, (coeff xi x = 0 ∨ si ≤ xi) ∧ True
⊢ (∃ si ∈ s, si ≤ xi) ↔
    ∃ si ∈ s,
      Dvd.dvd (α := MvPolynomial σ R) ((monomial si : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
        ((monomial xi : (a : R) → MvPolynomial σ R) (coeff xi x) : MvPolynomial σ R)
have simp_rw₂ : (∃ si ∈ s, si ≤ xi) ↔ ∃ si ∈ s, coeff xi x = 0 ∨ si ≤ xi
Tactic: simp_rw [monomial_dvd_monomial, one_dvd, and_true, mem_support_iff.mp hxi, false_or]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
xi : σ →₀ ℕ
hxi : xi ∈ x.support
simp_rw : (∃ si ∈ s, si ≤ xi) ↔ ∃ si ∈ s, (coeff xi x = 0 ∨ si ≤ xi) ∧ 1 ∣ coeff xi x
simp_rw₁ : (∃ si ∈ s, si ≤ xi) ↔ ∃ si ∈ s, (coeff xi x = 0 ∨ si ≤ xi) ∧ True
simp_rw₂ : (∃ si ∈ s, si ≤ xi) ↔ ∃ si ∈ s, coeff xi x = 0 ∨ si ≤ xi
⊢ (∃ si ∈ s, si ≤ xi) ↔
    ∃ si ∈ s,
      Dvd.dvd (α := MvPolynomial σ R) ((monomial si : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
        ((monomial xi : (a : R) → MvPolynomial σ R) (coeff xi x) : MvPolynomial σ R)
have simp_rw₃ : (∃ si ∈ s, si ≤ xi) ↔ ∃ si ∈ s, False ∨ si ≤ xi
Tactic: simp_rw [monomial_dvd_monomial, one_dvd, and_true, mem_support_iff.mp hxi, false_or]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
x : MvPolynomial σ R
s : Set σ
⊢ Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.span (X '' s)) x ↔
    ∀ m ∈ x.support, ∃ i ∈ s, Ne (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
have this : Membership.mem (γ := Ideal (MvPolynomial σ R))
    (Ideal.span
      ((fun (s : σ →₀ ℕ) ↦ (monomial s : (a : R) → MvPolynomial σ R) 1) '' (fun (i : σ) ↦ Finsupp.single i 1) '' s))
    x ↔
  ∀ xi ∈ x.support,
    ∃ (si : σ →₀ ℕ), Membership.mem (γ := Set (σ →₀ ℕ)) ((fun (i : σ) ↦ Finsupp.single i 1) '' s) si ∧ si ≤ xi
Tactic: have := @mem_ideal_span_monomial_image σ R _ x ((fun i => Finsupp.single i 1) '' s)
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
x : MvPolynomial σ R
s : Set σ
this :
  Membership.mem (γ := Ideal (MvPolynomial σ R))
      (Ideal.span
        ((fun (s : σ →₀ ℕ) ↦ (monomial s : (a : R) → MvPolynomial σ R) 1) '' (fun (i : σ) ↦ Finsupp.single i 1) '' s))
      x ↔
    ∀ xi ∈ x.support,
      ∃ (si : σ →₀ ℕ), Membership.mem (γ := Set (σ →₀ ℕ)) ((fun (i : σ) ↦ Finsupp.single i 1) '' s) si ∧ si ≤ xi
⊢ Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.span (X '' s)) x ↔
    ∀ m ∈ x.support, ∃ i ∈ s, Ne (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
have this₁ : Membership.mem (γ := Ideal (MvPolynomial σ R))
    (Ideal.span ((fun (x : σ) ↦ (monomial (Finsupp.single x 1) : (a : R) → MvPolynomial σ R) 1) '' s)) x ↔
  ∀ xi ∈ x.support,
    ∃ (si : σ →₀ ℕ), Membership.mem (γ := Set (σ →₀ ℕ)) ((fun (i : σ) ↦ Finsupp.single i 1) '' s) si ∧ si ≤ xi
Tactic: rw [Set.image_image] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
x : MvPolynomial σ R
s : Set σ
this :
  Membership.mem (γ := Ideal (MvPolynomial σ R))
      (Ideal.span ((fun (x : σ) ↦ (monomial (Finsupp.single x 1) : (a : R) → MvPolynomial σ R) 1) '' s)) x ↔
    ∀ xi ∈ x.support,
      ∃ (si : σ →₀ ℕ), Membership.mem (γ := Set (σ →₀ ℕ)) ((fun (i : σ) ↦ Finsupp.single i 1) '' s) si ∧ si ≤ xi
⊢ Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.span (X '' s)) x ↔
    ∀ m ∈ x.support, ∃ i ∈ s, Ne (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
have refine : (∀ xi ∈ x.support,
    ∃ (si : σ →₀ ℕ), Membership.mem (γ := Set (σ →₀ ℕ)) ((fun (i : σ) ↦ Finsupp.single i 1) '' s) si ∧ si ≤ xi) ↔
  ∀ m ∈ x.support, ∃ i ∈ s, Ne (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
Tactic: refine this.trans ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
⊢ Eq (α := Ideal (MvPolynomial σ R)) (idealOfVars σ R)
    (restrictSupportIdeal R (Set.preimage (β := ℕ) (⇑degree : (a : σ →₀ ℕ) → ℕ) (Set.Ici 1)) ⋯)
have a : LE.le (α := Ideal (MvPolynomial σ R)) (idealOfVars σ R)
  (restrictSupportIdeal R (Set.preimage (β := ℕ) (⇑degree : (a : σ →₀ ℕ) → ℕ) (Set.Ici 1)) sorry)
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
a :
  LE.le (α := Ideal (MvPolynomial σ R)) (idealOfVars σ R)
    (restrictSupportIdeal R (Set.preimage (β := ℕ) (⇑degree : (a : σ →₀ ℕ) → ℕ) (Set.Ici 1)) ⋯)
⊢ Eq (α := Ideal (MvPolynomial σ R)) (idealOfVars σ R)
    (restrictSupportIdeal R (Set.preimage (β := ℕ) (⇑degree : (a : σ →₀ ℕ) → ℕ) (Set.Ici 1)) ⋯)
have a₁ : LE.le (α := Ideal (MvPolynomial σ R))
  (restrictSupportIdeal R (Set.preimage (β := ℕ) (⇑degree : (a : σ →₀ ℕ) → ℕ) (Set.Ici 1)) sorry) (idealOfVars σ R)
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
⊢ ∀ ⦃x : MvPolynomial σ R⦄,
    Membership.mem (γ := Submodule R (MvPolynomial σ R))
        (restrictSupport R (Set.preimage (β := ℕ) (⇑degree : (a : σ →₀ ℕ) → ℕ) (Set.Ici 1))) x →
      Membership.mem (γ := Submodule R (MvPolynomial σ R)) (Submodule.restrictScalars R (idealOfVars σ R)) x
have a : Subset.{u_1} (α := Set (σ →₀ ℕ)) (Set.preimage (β := ℕ) (⇑degree : (a : σ →₀ ℕ) → ℕ) (Set.Ici 1))
  ((fun (x : σ →₀ ℕ) ↦ (monomial x : (a : R) → MvPolynomial σ R) 1) ⁻¹'
    (↑(Submodule.restrictScalars R (idealOfVars σ R)) : Set (MvPolynomial σ R)))
Tactic: rw [← SetLike.le_def, restrictSupport_eq_span, Submodule.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
x : σ →₀ ℕ
hx : Membership.mem (γ := Set (σ →₀ ℕ)) (Set.preimage (β := ℕ) (⇑degree : (a : σ →₀ ℕ) → ℕ) (Set.Ici 1)) x
⊢ Membership.mem (γ := Set (σ →₀ ℕ))
    ((fun (x : σ →₀ ℕ) ↦ (monomial x : (a : R) → MvPolynomial σ R) 1) ⁻¹'
      (↑(Submodule.restrictScalars R (idealOfVars σ R)) : Set (MvPolynomial σ R)))
    x
have a : ∀ (i : σ) (hi : i ∈ x.support),
  Membership.mem (γ := Set (σ →₀ ℕ))
    ((fun (x : σ →₀ ℕ) ↦ (monomial x : (a : R) → MvPolynomial σ R) 1) ⁻¹'
      (↑(Submodule.restrictScalars R (idealOfVars σ R)) : Set (MvPolynomial σ R)))
    x
Tactic: obtain ⟨i, hi⟩ : x.support.Nonempty := by aesop
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
x : σ →₀ ℕ
hx : Membership.mem (γ := Set (σ →₀ ℕ)) (Set.preimage (β := ℕ) (⇑degree : (a : σ →₀ ℕ) → ℕ) (Set.Ici 1)) x
i : σ
hi : i ∈ x.support
⊢ single i 1 ≤ x
have simp_all : ∀ (hx : LE.le (α := ℕ) (1 : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) x : ℕ))
  (hi : ¬Eq (α := ℕ) ((x : (a : σ) → ℕ) i : ℕ) (0 : ℕ)), LE.le (α := ℕ) (1 : ℕ) ((x : (a : σ) → ℕ) i : ℕ)
Tactic: simp_all
Cleared hypotheses: hx, hi
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
x : σ →₀ ℕ
hx : Membership.mem (γ := Set (σ →₀ ℕ)) (Set.preimage (β := ℕ) (⇑degree : (a : σ →₀ ℕ) → ℕ) (Set.Ici 1)) x
i : σ
hi : i ∈ x.support
⊢ Membership.mem (γ := Set (σ →₀ ℕ))
    ((fun (x : σ →₀ ℕ) ↦ (monomial x : (a : R) → MvPolynomial σ R) 1) ⁻¹'
      (↑(Submodule.restrictScalars R (idealOfVars σ R)) : Set (MvPolynomial σ R)))
    x
have a : ∀ (c : σ →₀ ℕ)
  (hx :
    Membership.mem (γ := Set (σ →₀ ℕ)) (Set.preimage (β := ℕ) (⇑degree : (a : σ →₀ ℕ) → ℕ) (Set.Ici 1))
      (c + single i 1))
  (hi : i ∈ (c + single i 1).support),
  Membership.mem (γ := Set (σ →₀ ℕ))
    ((fun (x : σ →₀ ℕ) ↦ (monomial x : (a : R) → MvPolynomial σ R) 1) ⁻¹'
      (↑(Submodule.restrictScalars R (idealOfVars σ R)) : Set (MvPolynomial σ R)))
    (c + single i 1)
Tactic: obtain ⟨c, rfl⟩ := le_iff_exists_add'.mp (show single i 1 ≤ x by simp_all; lia)
Cleared hypotheses: x, hx, hi
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : ℕ
⊢ HPow.hPow (α := Ideal (MvPolynomial σ R)) (idealOfVars σ R) n =
    restrictSupportIdeal R ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' Set.Ici n) ⋯
have rw : HPow.hPow (α := Ideal (MvPolynomial σ R))
    (restrictSupportIdeal R (Set.preimage (β := ℕ) (⇑degree : (a : σ →₀ ℕ) → ℕ) (Set.Ici 1)) sorry) n =
  restrictSupportIdeal R ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' Set.Ici n) sorry
Tactic: rw [idealOfVars_eq_restrictSupportIdeal]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : ℕ
⊢ HPow.hPow (α := Ideal (MvPolynomial σ R))
      (restrictSupportIdeal R (Set.preimage (β := ℕ) (⇑degree : (a : σ →₀ ℕ) → ℕ) (Set.Ici 1)) ⋯) n =
    restrictSupportIdeal R ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' Set.Ici n) ⋯
have a : Eq (α := Submodule R (MvPolynomial σ R))
  (Submodule.restrictScalars R
    (HPow.hPow (α := Ideal (MvPolynomial σ R))
      (restrictSupportIdeal R (Set.preimage (β := ℕ) (⇑degree : (a : σ →₀ ℕ) → ℕ) (Set.Ici 1)) sorry) n))
  (Submodule.restrictScalars R (restrictSupportIdeal R ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' Set.Ici n) sorry))
Tactic: apply Submodule.restrictScalars_injective R
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
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) ⋯))
have pos : ∀ (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)) sorry) n))
    (Submodule.restrictScalars R (restrictSupportIdeal R ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' Set.Ici n) sorry))
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : ℕ
pos :
  ∀ (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) ⋯))
⊢ 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) ⋯))
have neg : ∀ (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)) sorry) n))
    (Submodule.restrictScalars R (restrictSupportIdeal R ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' Set.Ici n) sorry))
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
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) ⋯))
have neg : HPow.hPow (α := Submodule R (MvPolynomial σ R))
    (Submodule.restrictScalars R
      (restrictSupportIdeal R (Set.preimage (β := ℕ) (⇑degree : (a : σ →₀ ℕ) → ℕ) (Set.Ici 1)) sorry))
    n =
  Submodule.restrictScalars R (restrictSupportIdeal R ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' Set.Ici n) sorry)
Tactic: rw [Submodule.restrictScalars_pow hn]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
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})
have 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}))
Tactic: rw [idealOfVars, Ideal.span, Submodule.span_pow, ← Set.image_univ,
    image_pow_eq_finsuppProd_image]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
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 ∈ p.support, n ≤ (degree : (a : σ →₀ ℕ) → ℕ) x
have rw : Membership.mem (γ := Ideal (MvPolynomial σ R)) (restrictSupportIdeal R ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' Set.Ici n) sorry)
    p ↔
  ∀ x ∈ p.support, n ≤ (degree : (a : σ →₀ ℕ) → ℕ) x
Tactic: rw [pow_idealOfVars]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : ℕ
r : R
⊢ Membership.mem (α := MvPolynomial σ R) (HPow.hPow (α := Ideal (MvPolynomial σ R)) (idealOfVars σ R) n)
      ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
    r = 0 ∨ n = 0
have 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
Tactic: by_cases h : r = 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
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
⊢ Membership.mem (α := MvPolynomial σ R) (HPow.hPow (α := Ideal (MvPolynomial σ R)) (idealOfVars σ R) n)
      ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
    r = 0 ∨ n = 0
have 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
Tactic: by_cases h : r = 0
-- 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)
⊢ Ideal.Quotient.mkₐ A I =
    aeval fun (d : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) (X d)
have 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)
Tactic: ext d
-- 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)
⊢ 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)
have 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
Tactic: ext d
-- 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
⊢ 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)
  ((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)
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)
⊢ 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)
  ((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)
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)
⊢ 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 : σ) ↦
        (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)
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]