awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
p : MvPolynomial σ R
⊢ support.{u_3, u_1} (R := R) ((homogeneousComponent n : (a : MvPolynomial σ R) → MvPolynomial σ R) p) =
    {c ∈ p.support | (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) c = n}

Tactic:
exact support_weightedHomogeneousComponent n p

Premises used: MvPolynomial.support_weightedHomogeneousComponent
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
⊢ SetLike.GradedMonoid (S := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R)

Tactic:
WeightedHomogeneousSubmodule.gradedMonoid

Premises used: MvPolynomial.weightedHomogeneousSubmodule, MvPolynomial.homogeneousSubmodule, setOf, MvPolynomial.IsHomogeneous, MvPolynomial.WeightedHomogeneousSubmodule.gradedMonoid
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
i : ℕ
⊢ (↑((@DirectSum.Decomposition.decompose' _ _ _ instDecidableEqNat _ _ _ _ _ φ :
            (a : ℕ) → ↥(homogeneousSubmodule σ R a))
          i) :
      MvPolynomial σ R) =
    (homogeneousComponent i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ

Tactic:
weightedDecomposition.decompose'_apply R _ φ i

Premises used: MvPolynomial.weightedDecomposition.decompose'_apply
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
rw :
  Eq (α := MvPolynomial σ R → DirectSum ℕ fun (i : ℕ) ↦ ↥(homogeneousSubmodule σ R i))
    (@DirectSum.Decomposition.decompose' _ _ _ instDecidableEqNat _ _ _ _ _) fun (φ : MvPolynomial σ R) ↦
    ((DirectSum.mk (fun (i : ℕ) ↦ ↥(homogeneousSubmodule σ R i))
            (Finset.image (⇑(weight fun (x : σ) ↦ 1) : (a : σ →₀ ℕ) → ℕ) φ.support) :
          ((i : (↑(↑(Finset.image (⇑(weight fun (x : σ) ↦ 1) : (a : σ →₀ ℕ) → ℕ) φ.support) : Set ℕ) : Type)) →
              ↥(homogeneousSubmodule σ R (↑i : ℕ))) →+
            DirectSum ℕ fun (i : ℕ) ↦ ↥(homogeneousSubmodule σ R i)) :
        (a :
            (i : (↑(↑(Finset.image (⇑(weight fun (x : σ) ↦ 1) : (a : σ →₀ ℕ) → ℕ) φ.support) : Set ℕ) : Type)) →
              ↥(homogeneousSubmodule σ R (↑i : ℕ))) →
          DirectSum ℕ fun (i : ℕ) ↦ ↥(homogeneousSubmodule σ R i))
      fun (m : (↑(↑(Finset.image (⇑(weight fun (x : σ) ↦ 1) : (a : σ →₀ ℕ) → ℕ) φ.support) : Set ℕ) : Type)) ↦
      Subtype.mk (p := fun (x : MvPolynomial σ R) ↦
        Membership.mem (γ := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R (↑m : ℕ)) x)
        ((homogeneousComponent (↑m : ℕ) : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) ⋯
⊢ Eq (α := MvPolynomial σ R → DirectSum ℕ fun (i : ℕ) ↦ ↥(homogeneousSubmodule σ R i))
    (@DirectSum.Decomposition.decompose' _ _ _ instDecidableEqNat _ _ _ _ _) fun (φ : MvPolynomial σ R) ↦
    ((DirectSum.mk (fun (i : ℕ) ↦ ↥(homogeneousSubmodule σ R i)) (Finset.image (⇑degree : (a : σ →₀ ℕ) → ℕ) φ.support) :
          ((i : (↑(↑(Finset.image (⇑degree : (a : σ →₀ ℕ) → ℕ) φ.support) : Set ℕ) : Type)) →
              ↥(homogeneousSubmodule σ R (↑i : ℕ))) →+
            DirectSum ℕ fun (i : ℕ) ↦ ↥(homogeneousSubmodule σ R i)) :
        (a :
            (i : (↑(↑(Finset.image (⇑degree : (a : σ →₀ ℕ) → ℕ) φ.support) : Set ℕ) : Type)) →
              ↥(homogeneousSubmodule σ R (↑i : ℕ))) →
          DirectSum ℕ fun (i : ℕ) ↦ ↥(homogeneousSubmodule σ R i))
      fun (m : (↑(↑(Finset.image (⇑degree : (a : σ →₀ ℕ) → ℕ) φ.support) : Set ℕ) : Type)) ↦
      Subtype.mk (p := fun (x : MvPolynomial σ R) ↦
        Membership.mem (γ := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R (↑m : ℕ)) x)
        ((homogeneousComponent (↑m : ℕ) : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) ⋯

Tactic:
rw [degree_eq_weight_one]

Premises used: Finsupp.degree_eq_weight_one
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
⊢ Eq (α := MvPolynomial σ R → DirectSum ℕ fun (i : ℕ) ↦ ↥(homogeneousSubmodule σ R i))
    (@DirectSum.Decomposition.decompose' _ _ _ instDecidableEqNat _ _ _ _ _) fun (φ : MvPolynomial σ R) ↦
    ((DirectSum.mk (fun (i : ℕ) ↦ ↥(homogeneousSubmodule σ R i))
            (Finset.image (⇑(weight fun (x : σ) ↦ 1) : (a : σ →₀ ℕ) → ℕ) φ.support) :
          ((i : (↑(↑(Finset.image (⇑(weight fun (x : σ) ↦ 1) : (a : σ →₀ ℕ) → ℕ) φ.support) : Set ℕ) : Type)) →
              ↥(homogeneousSubmodule σ R (↑i : ℕ))) →+
            DirectSum ℕ fun (i : ℕ) ↦ ↥(homogeneousSubmodule σ R i)) :
        (a :
            (i : (↑(↑(Finset.image (⇑(weight fun (x : σ) ↦ 1) : (a : σ →₀ ℕ) → ℕ) φ.support) : Set ℕ) : Type)) →
              ↥(homogeneousSubmodule σ R (↑i : ℕ))) →
          DirectSum ℕ fun (i : ℕ) ↦ ↥(homogeneousSubmodule σ R i))
      fun (m : (↑(↑(Finset.image (⇑(weight fun (x : σ) ↦ 1) : (a : σ →₀ ℕ) → ℕ) φ.support) : Set ℕ) : Type)) ↦
      Subtype.mk (p := fun (x : MvPolynomial σ R) ↦
        Membership.mem (γ := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R (↑m : ℕ)) x)
        ((homogeneousComponent (↑m : ℕ) : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) ⋯

Tactic:
rfl
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
x : ι → R
⊢ Eq (α := Ideal R) (span (Set.range x))
    (Submodule.map (AlgHom.toLinearMap (MvPolynomial.aeval x)) (MvPolynomial.homogeneousSubmodule ι R 1))

Tactic:
simp [MvPolynomial.homogeneousSubmodule_one_eq_span_X, Submodule.map_span, ← Set.range_comp,
    Function.comp_def]

Premises used: Set.range_comp, Function.comp_def, MvPolynomial.homogeneousSubmodule_one_eq_span_X, Submodule.map_span
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
x : ι → R
n : ℕ
rw :
  HPow.hPow (α := Ideal R) (span (Set.range x)) n =
    Submodule.map (AlgHom.toLinearMap (MvPolynomial.aeval x))
      (HPow.hPow (α := Submodule R (MvPolynomial ι R)) (MvPolynomial.homogeneousSubmodule ι R 1) n)
rw₁ :
  HPow.hPow (α := Ideal R) (span (Set.range x)) n =
    HPow.hPow (α := Submodule R R)
      (Submodule.map (AlgHom.toLinearMap (MvPolynomial.aeval x)) (MvPolynomial.homogeneousSubmodule ι R 1)) n
rw₂ rw₃ :
  HPow.hPow (α := Ideal R)
      (Submodule.map (AlgHom.toLinearMap (MvPolynomial.aeval x)) (MvPolynomial.homogeneousSubmodule ι R 1)) n =
    HPow.hPow (α := Submodule R R)
      (Submodule.map (AlgHom.toLinearMap (MvPolynomial.aeval x)) (MvPolynomial.homogeneousSubmodule ι R 1)) n
⊢ HPow.hPow (α := Ideal R) (span (Set.range x)) n =
    Submodule.map (AlgHom.toLinearMap (MvPolynomial.aeval x)) (MvPolynomial.homogeneousSubmodule ι R n)

Tactic:
rw [← MvPolynomial.homogeneousSubmodule_one_pow, Submodule.map_pow,
    Ideal.span_eq_map_homogeneousSubmodule]

Premises used: Ideal.span_eq_map_homogeneousSubmodule, Submodule.map_pow, MvPolynomial.homogeneousSubmodule_one_pow
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
n : ℕ
x : ι → R
y : R
⊢ y ∈ HPow.hPow (α := Ideal R) (span (Set.range x)) n ↔
    ∃ (p : MvPolynomial ι R), p.IsHomogeneous n ∧ (MvPolynomial.eval x : (a : MvPolynomial ι R) → R) p = y

Tactic:
simp [Ideal.span_pow_eq_map_homogeneousSubmodule]

Premises used: Ideal.span_pow_eq_map_homogeneousSubmodule
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
x : ι → R
y : R
⊢ Membership.mem (γ := Ideal R) (span (Set.range x)) y ↔
    ∃ (p : MvPolynomial ι R), p.IsHomogeneous 1 ∧ (MvPolynomial.eval x : (a : MvPolynomial ι R) → R) p = y

Tactic:
simp [Ideal.span_eq_map_homogeneousSubmodule]

Premises used: Ideal.span_eq_map_homogeneousSubmodule
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
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

Tactic:
AddMonoidAlgebra.mem_ideal_span_of'_image.trans ?_

Premises used: Set.Mem, setOf, AddMonoidAlgebra.mem_ideal_span_of'_image, Iff.trans, AddMonoidAlgebra.of', Finsupp.single
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
refine : (∀ m ∈ x.support, ∃ m' ∈ s, ∃ (d : σ →₀ ℕ), m = d + m') ↔ ∀ xi ∈ x.support, ∃ si ∈ s, si ≤ xi
⊢ 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

Tactic:
refine AddMonoidAlgebra.mem_ideal_span_of'_image.trans ?_

Premises used: AddMonoidAlgebra.mem_ideal_span_of'_image, Iff.trans
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
simp_rw :
  (∀ m ∈ x.support, ∃ m' ∈ s, ∃ (d : σ →₀ ℕ), m = m' + d) ↔ ∀ xi ∈ x.support, ∃ si ∈ s, ∃ (c : σ →₀ ℕ), xi = si + c
⊢ (∀ m ∈ x.support, ∃ m' ∈ s, ∃ (d : σ →₀ ℕ), m = d + m') ↔ ∀ xi ∈ x.support, ∃ si ∈ s, si ≤ xi

Tactic:
simp_rw [le_iff_exists_add, add_comm]

Premises used: le_iff_exists_add, add_comm
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
⊢ (∀ m ∈ x.support, ∃ m' ∈ s, ∃ (d : σ →₀ ℕ), m = m' + d) ↔ ∀ xi ∈ x.support, ∃ si ∈ s, ∃ (c : σ →₀ ℕ), xi = si + c

Tactic:
rfl
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
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)

Tactic:
mem_ideal_span_monomial_image.trans (forall₂_congr fun xi hxi => ?_)

Premises used: forall₂_congr, Iff.trans, MvPolynomial.mem_ideal_span_monomial_image
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
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)
⊢ 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)

Tactic:
refine mem_ideal_span_monomial_image.trans (forall₂_congr fun xi hxi => ?_)

Premises used: forall₂_congr, Iff.trans, MvPolynomial.mem_ideal_span_monomial_image
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
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
simp_rw₃ : (∃ si ∈ s, si ≤ xi) ↔ ∃ si ∈ s, False ∨ 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)

Tactic:
simp_rw [monomial_dvd_monomial, one_dvd, and_true, mem_support_iff.mp hxi, false_or]

Premises used: MvPolynomial.mem_support_iff, and_true, false_or, one_dvd, Iff.mp, MvPolynomial.monomial_dvd_monomial
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
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) '' (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)
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
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 ((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

Premises used: Set.image_image
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
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 : ℕ)

Tactic:
this.trans ?_

Premises used: Set.Mem, setOf, MvPolynomial.X, Iff.trans
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
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
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 : ℕ)
⊢ Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.span (X '' s)) x ↔
    ∀ m ∈ x.support, ∃ i ∈ s, Ne (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)

Tactic:
refine this.trans ?_

Premises used: Iff.trans
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
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
⊢ (∀ 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:
simp [Nat.one_le_iff_ne_zero]

Premises used: Nat.one_le_iff_ne_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : Finite σ
⊢ Ideal.FG (R := MvPolynomial σ R) (idealOfVars σ R)

Tactic:
Submodule.fg_span <| Set.finite_range _

Premises used: Set.finite_range, Submodule.FG, Ideal.FG, Submodule.fg_span
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
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)) ⋯)
a₁ :
  LE.le (α := Ideal (MvPolynomial σ R))
    (restrictSupportIdeal R (Set.preimage (β := ℕ) (⇑degree : (a : σ →₀ ℕ) → ℕ) (Set.Ici 1)) ⋯) (idealOfVars σ R)
⊢ Eq (α := Ideal (MvPolynomial σ R)) (idealOfVars σ R)
    (restrictSupportIdeal R (Set.preimage (β := ℕ) (⇑degree : (a : σ →₀ ℕ) → ℕ) (Set.Ici 1)) ⋯)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
⊢ LE.le (α := Ideal (MvPolynomial σ R)) (idealOfVars σ R)
    (restrictSupportIdeal R (Set.preimage (β := ℕ) (⇑degree : (a : σ →₀ ℕ) → ℕ) (Set.Ici 1)) ⋯)

Tactic:
simp [idealOfVars, Ideal.span_le, Set.range_subset_iff, restrictSupportIdeal, X]

Premises used: Ideal.span_le, MvPolynomial.restrictSupportIdeal, MvPolynomial.X, Set.range_subset_iff, MvPolynomial.idealOfVars
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
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)))
⊢ ∀ ⦃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

Tactic:
rw [← SetLike.le_def, restrictSupport_eq_span, Submodule.span_le, Set.image_subset_iff]

Premises used: SetLike.le_def, Set.image_subset_iff, MvPolynomial.restrictSupport_eq_span, Submodule.span_le
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
x : σ →₀ ℕ
hx : Membership.mem (γ := Set (σ →₀ ℕ)) (Set.preimage (β := ℕ) (⇑degree : (a : σ →₀ ℕ) → ℕ) (Set.Ici 1)) x
⊢ x.support.Nonempty

Tactic:
aesop
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
x : σ →₀ ℕ
hx : Membership.mem (γ := Set (σ →₀ ℕ)) (Set.preimage (β := ℕ) (⇑degree : (a : σ →₀ ℕ) → ℕ) (Set.Ici 1)) x
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
⊢ 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

Premises used: Finsupp.support, Finset.Nonempty
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
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
simp_all :
  ∀ (hx : LE.le (α := ℕ) (1 : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) x : ℕ))
    (hi : ¬Eq (α := ℕ) ((x : (a : σ) → ℕ) i : ℕ) (0 : ℕ)), LE.le (α := ℕ) (1 : ℕ) ((x : (a : σ) → ℕ) i : ℕ)
⊢ single i 1 ≤ x

Tactic:
simp_all
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
x : σ →₀ ℕ
i : σ
hx : LE.le (α := ℕ) (1 : ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) x : ℕ)
hi : ¬Eq (α := ℕ) ((x : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
⊢ LE.le (α := ℕ) (1 : ℕ) ((x : (a : σ) → ℕ) i : ℕ)

Tactic:
lia
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
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
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)
⊢ Membership.mem (γ := Set (σ →₀ ℕ))
    ((fun (x : σ →₀ ℕ) ↦ (monomial x : (a : R) → MvPolynomial σ R) 1) ⁻¹'
      (↑(Submodule.restrictScalars R (idealOfVars σ R)) : Set (MvPolynomial σ R)))
    x

Tactic:
obtain ⟨c, rfl⟩ := le_iff_exists_add'.mp (show single i 1 ≤ x by simp_all; lia)

Premises used: Iff.mp, le_iff_exists_add', rfl
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
i : σ
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 (MvPolynomial σ R)) (Set.range X) (X i)

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
i : σ
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:
simpa [monomial_add_single] using Ideal.mul_mem_left _ _ (Ideal.subset_span (by simp))

Premises used: Ideal.subset_span, MvPolynomial.monomial_add_single, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : ℕ
rw :
  HPow.hPow (α := Ideal (MvPolynomial σ R))
      (restrictSupportIdeal R (Set.preimage (β := ℕ) (⇑degree : (a : σ →₀ ℕ) → ℕ) (Set.Ici 1)) ⋯) n =
    restrictSupportIdeal R ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' Set.Ici n) ⋯
⊢ HPow.hPow (α := Ideal (MvPolynomial σ R)) (idealOfVars σ R) n =
    restrictSupportIdeal R ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' Set.Ici n) ⋯

Tactic:
rw [idealOfVars_eq_restrictSupportIdeal]

Premises used: MvPolynomial.idealOfVars_eq_restrictSupportIdeal
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
n : ℕ
a :
  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) ⋯))
⊢ HPow.hPow (α := Ideal (MvPolynomial σ R))
      (restrictSupportIdeal R (Set.preimage (β := ℕ) (⇑degree : (a : σ →₀ ℕ) → ℕ) (Set.Ici 1)) ⋯) n =
    restrictSupportIdeal R ((⇑degree : (a : σ →₀ ℕ) → ℕ) ⁻¹' Set.Ici n) ⋯

Tactic:
apply Submodule.restrictScalars_injective R

Premises used: Submodule.restrictScalars_injective
-- Module: Mathlib.RingTheory.MvPolynomial.Ideal
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) ⋯))
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)) ⋯) 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:
by_cases hn : n = 0