awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
x : PrimeSpectrum R
rw : Eq (α := Set (PrimeSpectrum R[X])) (⋂ (i : Fin n), zeroLocus {g.val i}) (zeroLocus {g.val i})
⊢ Eq (α := Set (PrimeSpectrum R[X])) (zeroLocus (Set.range g.val)) (zeroLocus {g.val i})

Tactic:
rw [Set.range_eq_iUnion, zeroLocus_iUnion]

Premises used: PrimeSpectrum.zeroLocus_iUnion, Set.range_eq_iUnion
-- 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
x : PrimeSpectrum R
⊢ Eq (α := Set (PrimeSpectrum R[X])) (⋂ (i : Fin n), zeroLocus {g.val i}) (zeroLocus {g.val i})

Tactic:
(Set.iInter_subset _ _).antisymm (Set.subset_iInter fun j ↦ ?_)

Premises used: Set.subset_iInter, HasSubset.Subset.antisymm, Set.iInter_subset
-- 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
x : PrimeSpectrum R
refine : ∀ (j : Fin n), Subset (α := Set (PrimeSpectrum R[X])) (zeroLocus {g.val i}) (zeroLocus {g.val j})
⊢ Eq (α := Set (PrimeSpectrum R[X])) (⋂ (i : Fin n), zeroLocus {g.val i}) (zeroLocus {g.val i})

Tactic:
refine (Set.iInter_subset _ _).antisymm (Set.subset_iInter fun j ↦ ?_)

Premises used: Set.subset_iInter, HasSubset.Subset.antisymm, Set.iInter_subset
-- 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
x : PrimeSpectrum R
j : Fin n
pos : ∀ (hij : i = j), Subset (α := Set (PrimeSpectrum R[X])) (zeroLocus {g.val i}) (zeroLocus {g.val j})
neg : ∀ (hij : ¬i = j), Subset (α := Set (PrimeSpectrum R[X])) (zeroLocus {g.val i}) (zeroLocus {g.val j})
⊢ Subset (α := Set (PrimeSpectrum R[X])) (zeroLocus {g.val i}) (zeroLocus {g.val j})

Tactic:
by_cases hij : i = j
-- 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
x : PrimeSpectrum R
j : Fin n
hij : i = j
pos : Subset (α := Set (PrimeSpectrum R[X])) (zeroLocus {g.val i}) (zeroLocus {g.val i})
⊢ Subset (α := Set (PrimeSpectrum R[X])) (zeroLocus {g.val i}) (zeroLocus {g.val j})

Tactic:
subst hij
-- 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
x : PrimeSpectrum R
⊢ Subset (α := Set (PrimeSpectrum R[X])) (zeroLocus {g.val i}) (zeroLocus {g.val i})

Tactic:
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
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
x : PrimeSpectrum R
j : Fin n
hij : ¬i = j
neg : Subset (α := Set (PrimeSpectrum R[X])) (zeroLocus {g.val i}) Set.univ
⊢ Subset (α := Set (PrimeSpectrum R[X])) (zeroLocus {g.val i}) (zeroLocus {g.val j})

Tactic:
rw [hi_min j (.symm hij), zeroLocus_singleton_zero]

Premises used: Ne.symm, PrimeSpectrum.zeroLocus_singleton_zero
-- 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
x : PrimeSpectrum R
j : Fin n
hij : ¬i = j
⊢ Subset (α := Set (PrimeSpectrum R[X])) (zeroLocus {g.val i}) Set.univ

Tactic:
Set.subset_univ _

Premises used: Set.subset_univ
-- 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
x : PrimeSpectrum R
j : Fin n
hij : ¬i = j
⊢ Subset (α := Set (PrimeSpectrum R[X])) (zeroLocus {g.val i}) Set.univ

Tactic:
exact Set.subset_univ _

Premises used: Set.subset_univ
-- 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
x : PrimeSpectrum R
⊢ Eq (α := Set (PrimeSpectrum R[X])) (zeroLocus (Set.range g.val)) (zeroLocus {g.val i})

Tactic:
have : zeroLocus (Set.range g.val) = zeroLocus {g.1 i} := by
        rw [Set.range_eq_iUnion, zeroLocus_iUnion]
        refine (Set.iInter_subset _ _).antisymm (Set.subset_iInter fun j ↦ ?_)
        by_cases hij : i = j
        · subst hij; rfl
        · rw [hi_min j (.symm hij), zeroLocus_singleton_zero]; exact Set.subset_univ _
-- 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_2 : Module.Finite R M
x : PrimeSpectrum R
this : Eq (α := Set (PrimeSpectrum R[X])) (zeroLocus (Set.range g.val)) (zeroLocus {g.val i})
hP₂ :
  (¬∀ i_1 < Module.finrank R M,
        Polynomial.coeff
            (LinearMap.charpoly (M := M)
              ((Algebra.lmul R M : (a : M) → Module.End R M) ((algebraMap R[X] M : (a : R[X]) → M) f)))
            i_1 ∈
          x.asIdeal) ↔
    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
⊢ 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

Tactic:
rw [this, ← Polynomial.algebraMap_eq, mem_image_comap_zeroLocus_sdiff,
        IsScalarTower.algebraMap_apply R[X] M, isNilpotent_tensor_residueField_iff]

Premises used: Polynomial, isNilpotent_tensor_residueField_iff, PrimeSpectrum.mem_image_comap_zeroLocus_sdiff, IsScalarTower.algebraMap_apply, Polynomial.algebraMap_eq
-- 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_2 : Module.Finite R M
x : PrimeSpectrum R
this : Eq (α := Set (PrimeSpectrum R[X])) (zeroLocus (Set.range g.val)) (zeroLocus {g.val i})
⊢ (¬∀ i_1 < Module.finrank R M,
        Polynomial.coeff
            (LinearMap.charpoly (M := M)
              ((Algebra.lmul R M : (a : M) → Module.End R M) ((algebraMap R[X] M : (a : R[X]) → M) f)))
            i_1 ∈
          x.asIdeal) ↔
    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

Tactic:
simp [BasicConstructibleSetData.toSet, ConstructibleSetData.toSet, Set.subset_def, M]

Premises used: PrimeSpectrum.BasicConstructibleSetData.toSet, Set.subset_def, PrimeSpectrum.ConstructibleSetData.toSet
-- 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
⊢ ∀ (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

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 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
⊢ ∀ [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

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
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_2 : Algebra R₀ R],
    Statement R₀ R n
      { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) : InductionObj R n }
R₀ : Type u_1
hP₃ : ∀ [inst : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n c
⊢ ∀ [inst : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n c

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
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_3 : Algebra R₀ R],
    Statement R₀ R n
      { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) : InductionObj R n }
R₀ : Type u_1
inst_2 : CommRing R₀
hP₃ : ∀ [inst : Algebra R₀ R], Statement R₀ R n c
⊢ ∀ [inst : Algebra R₀ R], Statement R₀ R n c

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
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_4 : Algebra R₀ R],
    Statement R₀ R n
      { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) : InductionObj R n }
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
hP₃ :
  Subsingleton R →
    ∃ (T : ConstructibleSetData R),
      comap Polynomial.C '' (zeroLocus (Set.range c.val) \ zeroLocus {f}) = T.toSet ∧
        ∀ C ∈ T,
          C.n ≤ c.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) c.powBound
hP₄ :
  Nontrivial R →
    ∃ (T : ConstructibleSetData R),
      comap Polynomial.C '' (zeroLocus (Set.range c.val) \ zeroLocus {f}) = T.toSet ∧
        ∀ C ∈ T,
          C.n ≤ c.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) c.powBound
⊢ ∃ (T : ConstructibleSetData R),
    comap Polynomial.C '' (zeroLocus (Set.range c.val) \ zeroLocus {f}) = T.toSet ∧
      ∀ C ∈ T,
        C.n ≤ c.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) c.powBound

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- 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
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_4 : Algebra R₀ R],
    Statement R₀ R n
      { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) : InductionObj R n }
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
h_1 : Subsingleton R
h :
  comap Polynomial.C '' (zeroLocus (Set.range c.val) \ zeroLocus {f}) = ConstructibleSetData.toSet ∅ ∧
    ∀ (C : BasicConstructibleSetData R),
      Membership.mem (γ := ConstructibleSetData R) ∅ C →
        C.n ≤ c.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) c.powBound
⊢ ∃ (T : ConstructibleSetData R),
    comap Polynomial.C '' (zeroLocus (Set.range c.val) \ zeroLocus {f}) = T.toSet ∧
      ∀ C ∈ T,
        C.n ≤ c.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) c.powBound

Tactic:
use ∅
-- 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
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_4 : Algebra R₀ R],
    Statement R₀ R n
      { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) : InductionObj R n }
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
h : Subsingleton R
⊢ comap Polynomial.C '' (zeroLocus (Set.range c.val) \ zeroLocus {f}) = ConstructibleSetData.toSet ∅ ∧
    ∀ (C : BasicConstructibleSetData R),
      Membership.mem (γ := ConstructibleSetData R) ∅ C →
        C.n ≤ c.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) c.powBound

Tactic:
simp [ConstructibleSetData.toSet, Subsingleton.elim f 0]

Premises used: Subsingleton.elim, OfNat.ofNat, PrimeSpectrum.ConstructibleSetData.toSet
-- 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
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_4 : Algebra R₀ R],
    Statement R₀ R n
      { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) : InductionObj R n }
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
h : Nontrivial R
hP₃ :
  ∀ (S : ConstructibleSetData R)
    (hS :
      comap Polynomial.C ''
          (zeroLocus
              (Set.range
                { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) :
                    InductionObj R n }.val) \
            zeroLocus {f}) =
        S.toSet)
    (hS' :
      ∀ C ∈ S,
        C.n ≤
            { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) :
                InductionObj R n }.degBound ∧
          ∀ (i_1 : Fin C.n),
            C.g i_1 ∈
              HPow.hPow (α := Submodule R₀ R)
                (coeffSubmodule R₀
                  { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) :
                    InductionObj R n })
                { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) :
                    InductionObj R n }.powBound),
    ∃ (T : ConstructibleSetData R),
      comap Polynomial.C '' (zeroLocus (Set.range c.val) \ zeroLocus {f}) = T.toSet ∧
        ∀ C ∈ T,
          C.n ≤ c.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) c.powBound
⊢ ∃ (T : ConstructibleSetData R),
    comap Polynomial.C '' (zeroLocus (Set.range c.val) \ zeroLocus {f}) = T.toSet ∧
      ∀ C ∈ T,
        C.n ≤ c.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) c.powBound

Tactic:
obtain ⟨S, hS, hS'⟩ := H (R₀ := R₀) f
-- 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
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_4 : Algebra R₀ R],
    Statement R₀ R n
      { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) : InductionObj R n }
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
h : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus
          (Set.range
            { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) :
                InductionObj R n }.val) \
        zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤
        { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) :
            InductionObj R n }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          HPow.hPow (α := Submodule R₀ R)
            (coeffSubmodule R₀
              { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) : InductionObj R n })
            { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) :
                InductionObj R n }.powBound
⊢ ∃ (T : ConstructibleSetData R),
    comap Polynomial.C '' (zeroLocus (Set.range c.val) \ zeroLocus {f}) = T.toSet ∧
      ∀ C ∈ T,
        C.n ≤ c.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) c.powBound

Tactic:
⟨S, Eq.trans ?_ hS, ?_⟩

Premises used: And.intro, Exists.intro, Eq.trans
-- 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
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_4 : Algebra R₀ R],
    Statement R₀ R n
      { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) : InductionObj R n }
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
h : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus
          (Set.range
            { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) :
                InductionObj R n }.val) \
        zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤
        { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) :
            InductionObj R n }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          HPow.hPow (α := Submodule R₀ R)
            (coeffSubmodule R₀
              { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) : InductionObj R n })
            { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) :
                InductionObj R n }.powBound
hP₃ :
  comap Polynomial.C '' (zeroLocus (Set.range c.val) \ zeroLocus {f}) =
    comap Polynomial.C ''
      (zeroLocus
          (Set.range
            { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) :
                InductionObj R n }.val) \
        zeroLocus {f})
hP₄ :
  ∀ C ∈ S, C.n ≤ c.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) c.powBound
⊢ ∃ (T : ConstructibleSetData R),
    comap Polynomial.C '' (zeroLocus (Set.range c.val) \ zeroLocus {f}) = T.toSet ∧
      ∀ C ∈ T,
        C.n ≤ c.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) c.powBound

Tactic:
refine ⟨S, Eq.trans ?_ hS, ?_⟩