awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R₀ : Type u_1
R : Type u_2
inst : CommRing R₀
inst_1 : CommRing R
inst_2 : Algebra R₀ R
n : ℕ
S : InductionObj R n
revert : ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_3 : Algebra R₀ R], Statement R₀ R n S
⊢ Statement R₀ R n S

Tactic:
revert R₀
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R : Type u_2
inst : CommRing R
n : ℕ
S : InductionObj R n
revert : ∀ (S : InductionObj R n) {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n S
⊢ ∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n S

Tactic:
revert S
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R : Type u_2
inst : CommRing R
n : ℕ
hP₁ :
  ∀ (R : Type u_2) [inst : CommRing R] {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R],
    Statement R₀ R n { val := 0 }
hP₂ :
  ∀ (R : Type u_2) [inst : CommRing R] (e : InductionObj R n) (i : Fin n),
    (e.val i).Monic →
      (∀ (j : Fin n), j ≠ i → e.val j = 0) →
        ∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n e
hP₃ :
  ∀ (R : Type u_2) [inst : CommRing R] (e : InductionObj R n) (i j : Fin n),
    (e.val i).Monic →
      (e.val i).degree ≤ (e.val j).degree →
        i ≠ j →
          (∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R],
              Statement R₀ R n
                { val := Function.update (β := fun (a : Fin n) ↦ R[X]) e.val j (e.val j %ₘ e.val i) :
                  InductionObj R n }) →
            ∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n e
hP₄ :
  ∀ (R : Type u_2) [inst : CommRing R] (c : R) (i : Fin n) (e : InductionObj R n),
    c = (e.val i).leadingCoeff →
      c ≠ 0 →
        (∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra.{u_1, u_2} R₀ (Away c)],
            Statement R₀ (Away c) n
              {
                val :=
                  HSMul.hSMul (α := (Away c)[X]) (β := Fin n → (Away c)[X])
                    ((Polynomial.C : (a : Away c) → (Away c)[X]) (IsLocalization.Away.invSelf c))
                    ((⇑(mapRingHom (algebraMap R (Away c))) : (a : R[X]) → (Away c)[X]) ∘ e.val) :
                InductionObj (Away c) n }) →
          (∀ {R₀ : Type u_1} [inst_1 : CommRing R₀]
              [inst_2 : Algebra.{u_1, u_2} R₀ (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))],
              Statement R₀ (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})) n
                {
                  val :=
                    (⇑(mapRingHom (algebraMap R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})))) :
                        (a : R[X]) → (R ⧸ Ideal.span {c})[X]) ∘
                      e.val }) →
            ∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n e
⊢ ∀ (S : InductionObj R n) {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n S

Tactic:
apply induction_structure

Premises used: _private.0.ChevalleyThm.PolynomialC.induction_structure
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
hP₁ :
  ∀ [inst : CommRing R] {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n { val := 0 }
⊢ ∀ [inst : CommRing R] {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n { val := 0 }

Tactic:
_
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
R₀ : Type u_1
hP₁ : ∀ [inst : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n { val := 0 }
⊢ ∀ [inst : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n { val := 0 }

Tactic:
_
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
R₀ : Type u_1
inst_2 : CommRing R₀
hP₁ : ∀ [inst : Algebra R₀ R], Statement R₀ R n { val := 0 }
⊢ ∀ [inst : Algebra R₀ R], Statement R₀ R n { val := 0 }

Tactic:
_
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
⊢ ∃ (T : ConstructibleSetData R),
    Eq (α := Set (PrimeSpectrum R))
        (comap Polynomial.C '' (zeroLocus (Set.range (ι := Fin n) (val { val := 0 })) \ zeroLocus {f})) T.toSet ∧
      ∀ C ∈ T,
        C.n ≤ degBound.{u_2} (R := R) (n := n) { val := 0 } ∧
          ∀ (i : Fin C.n),
            C.g i ∈
              HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ (n := n) { val := 0 : InductionObj R n })
                (powBound.{u_2} (R := R) (n := n) { val := 0 : InductionObj R n })

Tactic:
⟨(Finset.range (f.natDegree + 2)).image fun j ↦ ⟨f.coeff j, 0, 0⟩, ?_, ?_⟩

Premises used: PrimeSpectrum.BasicConstructibleSetData.mk, Polynomial.coeff, Finset.range, HAdd.hAdd, And.intro, Exists.intro, Polynomial.natDegree, OfNat.ofNat, Finset.image
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
hP₁ :
  Eq (α := Set (PrimeSpectrum R))
    (comap Polynomial.C '' (zeroLocus (Set.range (ι := Fin n) (val { val := 0 })) \ zeroLocus {f}))
    (ConstructibleSetData.toSet
      (Finset.image (fun (j : ℕ) ↦ { f := f.coeff j, n := 0, g := 0 }) (Finset.range (f.natDegree + 2))))
hP₂ :
  ∀ (C : BasicConstructibleSetData R),
    Membership.mem (γ := ConstructibleSetData R)
        (Finset.image (fun (j : ℕ) ↦ { f := f.coeff j, n := 0, g := 0 }) (Finset.range (f.natDegree + 2))) C →
      C.n ≤ degBound.{u_2} (R := R) (n := n) { val := 0 } ∧
        ∀ (i : Fin C.n),
          C.g i ∈
            HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ (n := n) { val := 0 : InductionObj R n })
              (powBound.{u_2} (R := R) (n := n) { val := 0 : InductionObj R n })
⊢ ∃ (T : ConstructibleSetData R),
    Eq (α := Set (PrimeSpectrum R))
        (comap Polynomial.C '' (zeroLocus (Set.range (ι := Fin n) (val { val := 0 })) \ zeroLocus {f})) T.toSet ∧
      ∀ C ∈ T,
        C.n ≤ degBound.{u_2} (R := R) (n := n) { val := 0 } ∧
          ∀ (i : Fin C.n),
            C.g i ∈
              HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ (n := n) { val := 0 : InductionObj R n })
                (powBound.{u_2} (R := R) (n := n) { val := 0 : InductionObj R n })

Tactic:
refine ⟨(Finset.range (f.natDegree + 2)).image fun j ↦ ⟨f.coeff j, 0, 0⟩, ?_, ?_⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
⊢ comap Polynomial.C '' (↑(basicOpen f) : Set (PrimeSpectrum R[X])) = (zeroLocus coeff(f))ᶜ

Tactic:
image_comap_C_basicOpen f

Premises used: Polynomial.image_comap_C_basicOpen
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
h : zeroLocus (Set.range (ι := Fin n) (val { val := 0 })) \ zeroLocus {f} = (↑(basicOpen f) : Set (PrimeSpectrum R[X]))
h₁ :
  Eq (α := Set (PrimeSpectrum R))
    (ConstructibleSetData.toSet
      (Finset.image (fun (j : ℕ) ↦ { f := f.coeff j, n := 0, g := 0 }) (Finset.range (f.natDegree + 2))))
    (zeroLocus coeff(f))ᶜ
⊢ Eq (α := Set (PrimeSpectrum R))
    (comap Polynomial.C '' (zeroLocus (Set.range (ι := Fin n) (val { val := 0 })) \ zeroLocus {f}))
    (ConstructibleSetData.toSet
      (Finset.image (fun (j : ℕ) ↦ { f := f.coeff j, n := 0, g := 0 }) (Finset.range (f.natDegree + 2))))

Tactic:
convert! image_comap_C_basicOpen f

Premises used: Polynomial.image_comap_C_basicOpen
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
h : Eq (α := Set (PrimeSpectrum R[X])) (zeroLocus (Set.range (ι := Fin n) 0) \ zeroLocus {f}) (Set.univ \ zeroLocus {f})
⊢ zeroLocus (Set.range (ι := Fin n) (val { val := 0 })) \ zeroLocus {f} = (↑(basicOpen f) : Set (PrimeSpectrum R[X]))

Tactic:
simp only [basicOpen_eq_zeroLocus_compl, Set.compl_eq_univ_diff]

Premises used: Set.compl_eq_univ_diff, PrimeSpectrum.basicOpen_eq_zeroLocus_compl
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
h : Eq.{u_2 + 1} (α := Set (PrimeSpectrum R[X])) (zeroLocus (Set.range (ι := Fin n) 0)) Set.univ
⊢ Eq (α := Set (PrimeSpectrum R[X])) (zeroLocus (Set.range (ι := Fin n) 0) \ zeroLocus {f}) (Set.univ \ zeroLocus {f})

Tactic:
congr 1
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
h : Subset.{u_2} (α := Set (PrimeSpectrum R[X])) Set.univ (zeroLocus (Set.range (ι := Fin n) 0))
⊢ Eq.{u_2 + 1} (α := Set (PrimeSpectrum R[X])) (zeroLocus (Set.range (ι := Fin n) 0)) Set.univ

Tactic:
rw [← Set.univ_subset_iff]

Premises used: Set.univ_subset_iff
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
x : PrimeSpectrum R[X]
h : Membership.mem (γ := Set (PrimeSpectrum R[X])) Set.univ x
w : Fin n
⊢ 0 w ∈ (↑x.asIdeal : Set R[X])

Tactic:
zero_mem x.asIdeal

Premises used: Set.Mem, ZeroMemClass.zero_mem, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
x : PrimeSpectrum R[X]
h : Membership.mem (γ := Set (PrimeSpectrum R[X])) Set.univ x
w : Fin n
⊢ 0 w ∈ (↑x.asIdeal : Set R[X])

Tactic:
exact zero_mem x.asIdeal

Premises used: ZeroMemClass.zero_mem, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
this : coeff(f) = ⋃ (i : ℕ), ⋃ (_ : i < f.natDegree + 2), {f.coeff i}
⊢ Eq (α := Set (PrimeSpectrum R))
    (ConstructibleSetData.toSet
      (Finset.image (fun (j : ℕ) ↦ { f := f.coeff j, n := 0, g := 0 }) (Finset.range (f.natDegree + 2))))
    (zeroLocus coeff(f))ᶜ

Tactic:
simp [BasicConstructibleSetData.toSet, ConstructibleSetData.toSet,
            ← Set.compl_eq_univ_diff, eq_compl_comm (y := zeroLocus _), ← zeroLocus_iUnion₂, this]

Premises used: PrimeSpectrum.BasicConstructibleSetData.toSet, PrimeSpectrum.zeroLocus_iUnion₂, Set.compl_eq_univ_diff, PrimeSpectrum.ConstructibleSetData.toSet, eq_compl_comm
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
h : coeff(f) = ⋃ (i : ℕ), ⋃ (_ : i < f.natDegree + 2), {f.coeff i}
⊢ Eq (α := Set (PrimeSpectrum R))
    (ConstructibleSetData.toSet
      (Finset.image (fun (j : ℕ) ↦ { f := f.coeff j, n := 0, g := 0 }) (Finset.range (f.natDegree + 2))))
    (zeroLocus coeff(f))ᶜ

Tactic:
suffices Set.range f.coeff = ⋃ i < f.natDegree + 2, {f.coeff i} by
          simp [BasicConstructibleSetData.toSet, ConstructibleSetData.toSet,
            ← Set.compl_eq_univ_diff, eq_compl_comm (y := zeroLocus _), ← zeroLocus_iUnion₂, this]
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
trans : coeff(f) = f.coeff '' Set.Iio (f.natDegree + 2)
trans₁ : f.coeff '' Set.Iio (f.natDegree + 2) = ⋃ (i : ℕ), ⋃ (_ : i < f.natDegree + 2), {f.coeff i}
⊢ coeff(f) = ⋃ (i : ℕ), ⋃ (_ : i < f.natDegree + 2), {f.coeff i}

Tactic:
trans f.coeff '' (Set.Iio (f.natDegree + 2))

Premises used: Polynomial.coeff, HAdd.hAdd, Polynomial.natDegree, OfNat.ofNat, Set.Iio
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
⊢ coeff(f) = f.coeff '' Set.Iio (f.natDegree + 2)

Tactic:
((Set.image_subset_range _ _).antisymm ?_).symm

Premises used: Set.image_subset_range, HasSubset.Subset.antisymm, Eq.symm
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
refine : coeff(f) ⊆ f.coeff '' Set.Iio (f.natDegree + 2)
⊢ coeff(f) = f.coeff '' Set.Iio (f.natDegree + 2)

Tactic:
refine ((Set.image_subset_range _ _).antisymm ?_).symm

Premises used: Set.image_subset_range, HasSubset.Subset.antisymm, Eq.symm
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
i : ℕ
pos : ∀ (hi : i ≤ f.natDegree), f.coeff i ∈ f.coeff '' Set.Iio (f.natDegree + 2)
neg : ∀ (hi : f.natDegree < i), f.coeff i ∈ f.coeff '' Set.Iio (f.natDegree + 2)
⊢ f.coeff i ∈ f.coeff '' Set.Iio (f.natDegree + 2)

Tactic:
by_cases! hi : i ≤ f.natDegree

Premises used: Polynomial.natDegree
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
i : ℕ
hi : i ≤ f.natDegree
⊢ f.natDegree < f.natDegree + 2

Tactic:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
i : ℕ
hi : i ≤ f.natDegree
⊢ f.coeff i ∈ f.coeff '' Set.Iio (f.natDegree + 2)

Tactic:
exact ⟨i, hi.trans_lt (by simp), rfl⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
i : ℕ
hi : f.natDegree < i
⊢ f.natDegree + 1 ∈ Set.Iio (f.natDegree + 2)

Tactic:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
i : ℕ
hi : f.natDegree < i
⊢ f.coeff (f.natDegree + 1) = f.coeff i

Tactic:
simp [f.coeff_eq_zero_of_natDegree_lt hi]

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
i : ℕ
hi : f.natDegree < i
⊢ f.coeff i ∈ f.coeff '' Set.Iio (f.natDegree + 2)

Tactic:
exact ⟨f.natDegree + 1, by simp, by simp [f.coeff_eq_zero_of_natDegree_lt hi]⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
h :
  ∀ (x : R),
    x ∈ f.coeff '' Set.Iio (f.natDegree + 2) ↔
      Membership.mem (γ := Set R) (⋃ (i : ℕ), ⋃ (_ : i < f.natDegree + 2), {f.coeff i}) x
⊢ f.coeff '' Set.Iio (f.natDegree + 2) = ⋃ (i : ℕ), ⋃ (_ : i < f.natDegree + 2), {f.coeff i}

Tactic:
ext
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
x : R
⊢ x ∈ f.coeff '' Set.Iio (f.natDegree + 2) ↔
    Membership.mem (γ := Set R) (⋃ (i : ℕ), ⋃ (_ : i < f.natDegree + 2), {f.coeff i}) x

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
⊢ ∀ (C : BasicConstructibleSetData R),
    Membership.mem (γ := ConstructibleSetData R)
        (Finset.image (fun (j : ℕ) ↦ { f := f.coeff j, n := 0, g := 0 }) (Finset.range (f.natDegree + 2))) C →
      C.n ≤ degBound.{u_2} (R := R) (n := n) { val := 0 } ∧
        ∀ (i : Fin C.n),
          C.g i ∈
            HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ (n := n) { val := 0 : InductionObj R n })
              (powBound.{u_2} (R := R) (n := n) { val := 0 : InductionObj R n })

Tactic:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
hP₂ :
  ∀ [inst : CommRing R] (e : InductionObj R n) (i : Fin n),
    (e.val i).Monic →
      (∀ (j : Fin n), j ≠ i → e.val j = 0) →
        ∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n e
⊢ ∀ [inst : CommRing R] (e : InductionObj R n) (i : Fin n),
    (e.val i).Monic →
      (∀ (j : Fin n), j ≠ i → e.val j = 0) →
        ∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n e

Tactic:
_
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
g : InductionObj R n
i : Fin n
hi : (g.val i).Monic
hi_min : ∀ (j : Fin n), j ≠ i → g.val j = 0
hP₂ : ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n g
⊢ ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n g

Tactic:
_
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
g : InductionObj R n
i : Fin n
hi : (g.val i).Monic
hi_min : ∀ (j : Fin n), j ≠ i → g.val j = 0
R₀_1 : Type u_1
R₀ : CommRing R₀_1
hP₂ : ∀ [inst : Algebra R₀_1 R], Statement R₀_1 R n g
⊢ ∀ [inst : Algebra R₀_1 R], Statement R₀_1 R n g

Tactic:
_
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
g : InductionObj R n
i : Fin n
hi : (g.val i).Monic
hi_min : ∀ (j : Fin n), j ≠ i → g.val j = 0
R₀_1 : Type u_1
R₀ : CommRing R₀_1
inst_2 : Algebra R₀_1 R
f : R[X]
M : Type u_2 := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.span {g.val i})
⊢ Module.Free R M

Tactic:
have : Module.Free R M := .of_basis (AdjoinRoot.powerBasis' hi).basis
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
g : InductionObj R n
i : Fin n
hi : (g.val i).Monic
hi_min : ∀ (j : Fin n), j ≠ i → g.val j = 0
R₀_1 : Type u_1
R₀ : CommRing R₀_1
inst_2 : Algebra R₀_1 R
f : R[X]
M : Type u_2 := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.span {g.val i})
this : Module.Free R M
⊢ Module.Finite R M

Tactic:
have : Module.Finite R M := .of_basis (AdjoinRoot.powerBasis' hi).basis
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
g : InductionObj R n
i : Fin n
hi : (g.val i).Monic
hi_min : ∀ (j : Fin n), j ≠ i → g.val j = 0
R₀_1 : Type u_1
R₀ : CommRing R₀_1
inst_2 : Algebra R₀_1 R
f : R[X]
M : Type u_2 := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.span {g.val i})
this_1 : Module.Free R M
this : Module.Finite R M
⊢ ∃ (T : ConstructibleSetData R),
    comap Polynomial.C '' (zeroLocus (Set.range g.val) \ zeroLocus {f}) = T.toSet ∧
      ∀ C ∈ T,
        C.n ≤ g.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ HPow.hPow (α := Submodule R₀_1 R) (coeffSubmodule R₀_1 g) g.powBound

Tactic:
⟨(Finset.range (Module.finrank R M)).image
      fun j ↦ ⟨(Algebra.lmul R M (Ideal.Quotient.mk _ f)).charpoly.coeff j, 0, 0⟩, ?_, ?_⟩

Premises used: _private.0.ChevalleyThm.PolynomialC.InductionObj.val, Algebra.lmul, Ideal.Quotient.mk, PrimeSpectrum.BasicConstructibleSetData.mk, Polynomial.coeff, Finset.range, And.intro, Exists.intro, Ideal.span, Singleton.singleton, OfNat.ofNat, DFunLike.coe, Finset.image, LinearMap.charpoly, Module.finrank
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
g : InductionObj R n
i : Fin n
hi : (g.val i).Monic
hi_min : ∀ (j : Fin n), j ≠ i → g.val j = 0
R₀_1 : Type u_1
R₀ : CommRing R₀_1
inst_2 : Algebra R₀_1 R
f : R[X]
M : Type u_2 := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.span {g.val i})
this_1 : Module.Free R M
this : Module.Finite R M
hP₂ :
  comap Polynomial.C '' (zeroLocus (Set.range g.val) \ zeroLocus {f}) =
    ConstructibleSetData.toSet
      (Finset.image
        (fun (j : ℕ) ↦
          {
            f :=
              Polynomial.coeff
                (LinearMap.charpoly (M := M)
                  ((Algebra.lmul R M : (a : M) → Module.End R M)
                    ((Ideal.Quotient.mk (Ideal.span {g.val i}) : (a : R[X]) → R[X] ⧸ Ideal.span {g.val i}) f)))
                j,
            n := 0, g := 0 })
        (Finset.range (Module.finrank R M)))
hP₃ :
  ∀ (C : BasicConstructibleSetData R),
    Membership.mem (γ := ConstructibleSetData R)
        (Finset.image
          (fun (j : ℕ) ↦
            {
              f :=
                Polynomial.coeff
                  (LinearMap.charpoly (M := M)
                    ((Algebra.lmul R M : (a : M) → Module.End R M)
                      ((Ideal.Quotient.mk (Ideal.span {g.val i}) : (a : R[X]) → R[X] ⧸ Ideal.span {g.val i}) f)))
                  j,
              n := 0, g := 0 })
          (Finset.range (Module.finrank R M)))
        C →
      C.n ≤ g.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ HPow.hPow (α := Submodule R₀_1 R) (coeffSubmodule R₀_1 g) g.powBound
⊢ ∃ (T : ConstructibleSetData R),
    comap Polynomial.C '' (zeroLocus (Set.range g.val) \ zeroLocus {f}) = T.toSet ∧
      ∀ C ∈ T,
        C.n ≤ g.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ HPow.hPow (α := Submodule R₀_1 R) (coeffSubmodule R₀_1 g) g.powBound

Tactic:
refine ⟨(Finset.range (Module.finrank R M)).image
      fun j ↦ ⟨(Algebra.lmul R M (Ideal.Quotient.mk _ f)).charpoly.coeff j, 0, 0⟩, ?_, ?_⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
g : InductionObj R n
i : Fin n
hi : (g.val i).Monic
hi_min : ∀ (j : Fin n), j ≠ i → g.val j = 0
R₀_1 : Type u_1
R₀ : CommRing R₀_1
inst_2 : Algebra R₀_1 R
f : R[X]
M : Type u_2 := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.span {g.val i})
this_1 : Module.Free R M
this : Module.Finite R M
hP₂ :
  ∀ (x : PrimeSpectrum R),
    x ∈ comap Polynomial.C '' (zeroLocus (Set.range g.val) \ zeroLocus {f}) ↔
      Membership.mem (γ := Set (PrimeSpectrum R))
        (ConstructibleSetData.toSet
          (Finset.image
            (fun (j : ℕ) ↦
              {
                f :=
                  Polynomial.coeff
                    (LinearMap.charpoly (M := M)
                      ((Algebra.lmul R M : (a : M) → Module.End R M)
                        ((Ideal.Quotient.mk (Ideal.span {g.val i}) : (a : R[X]) → R[X] ⧸ Ideal.span {g.val i}) f)))
                    j,
                n := 0, g := 0 })
            (Finset.range (Module.finrank R M))))
        x
⊢ comap Polynomial.C '' (zeroLocus (Set.range g.val) \ zeroLocus {f}) =
    ConstructibleSetData.toSet
      (Finset.image
        (fun (j : ℕ) ↦
          {
            f :=
              Polynomial.coeff
                (LinearMap.charpoly (M := M)
                  ((Algebra.lmul R M : (a : M) → Module.End R M)
                    ((Ideal.Quotient.mk (Ideal.span {g.val i}) : (a : R[X]) → R[X] ⧸ Ideal.span {g.val i}) f)))
                j,
            n := 0, g := 0 })
        (Finset.range (Module.finrank R M)))

Tactic:
ext x