awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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 : ℕ
⊢ f.coeff i ∈ f.coeff '' Set.Iio (f.natDegree + 2)
have pos : ∀ (hi : i ≤ f.natDegree), f.coeff i ∈ f.coeff '' Set.Iio (f.natDegree + 2)
Tactic: by_cases! hi : i ≤ f.natDegree
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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)
⊢ f.coeff i ∈ f.coeff '' Set.Iio (f.natDegree + 2)
have neg : ∀ (hi : f.natDegree < i), f.coeff i ∈ f.coeff '' Set.Iio (f.natDegree + 2)
Tactic: by_cases! hi : i ≤ f.natDegree
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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]
⊢ f.coeff '' Set.Iio (f.natDegree + 2) = ⋃ (i : ℕ), ⋃ (_ : i < f.natDegree + 2), {f.coeff i}
have h : ∀ (x : R),
  x ∈ f.coeff '' Set.Iio (f.natDegree + 2) ↔
    Membership.mem (γ := Set R) (⋃ (i : ℕ), ⋃ (_ : i < f.natDegree + 2), {f.coeff i}) x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (hypothesis)
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})
⊢ ∃ (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
have this : Module.Free R M
Tactic: have : Module.Free R M := .of_basis (AdjoinRoot.powerBasis' hi).basis
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (hypothesis)
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
⊢ ∃ (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
have this₁ : Module.Finite R M
Tactic: have : Module.Finite R M := .of_basis (AdjoinRoot.powerBasis' hi).basis
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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
have 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)))
Tactic: refine ⟨(Finset.range (Module.finrank R M)).image
      fun j ↦ ⟨(Algebra.lmul R M (Ideal.Quotient.mk _ f)).charpoly.coeff j, 0, 0⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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)))
⊢ ∃ (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
have 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
Tactic: refine ⟨(Finset.range (Module.finrank R M)).image
      fun j ↦ ⟨(Algebra.lmul R M (Ideal.Quotient.mk _ f)).charpoly.coeff j, 0, 0⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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
⊢ 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)))
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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})
have rw : Eq (α := Set (PrimeSpectrum R[X])) (⋂ (i : Fin n), zeroLocus {g.val i}) (zeroLocus {g.val i})
Tactic: rw [Set.range_eq_iUnion, zeroLocus_iUnion]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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})
have refine : ∀ (j : Fin n), Subset (α := Set (PrimeSpectrum R[X])) (zeroLocus {g.val i}) (zeroLocus {g.val j})
Tactic: refine (Set.iInter_subset _ _).antisymm (Set.subset_iInter fun j ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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
⊢ Subset (α := Set (PrimeSpectrum R[X])) (zeroLocus {g.val i}) (zeroLocus {g.val j})
have pos : ∀ (hij : i = j), Subset (α := Set (PrimeSpectrum R[X])) (zeroLocus {g.val i}) (zeroLocus {g.val j})
Tactic: by_cases hij : i = j
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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})
⊢ Subset (α := Set (PrimeSpectrum R[X])) (zeroLocus {g.val i}) (zeroLocus {g.val j})
have neg : ∀ (hij : ¬i = j), Subset (α := Set (PrimeSpectrum R[X])) (zeroLocus {g.val i}) (zeroLocus {g.val j})
Tactic: by_cases hij : i = j
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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}) (zeroLocus {g.val j})
have pos : Subset (α := Set (PrimeSpectrum R[X])) (zeroLocus {g.val i}) (zeroLocus {g.val i})
Tactic: subst hij
Cleared hypotheses: j, hij
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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}) (zeroLocus {g.val j})
have neg : Subset (α := Set (PrimeSpectrum R[X])) (zeroLocus {g.val i}) Set.univ
Tactic: rw [hi_min j (.symm hij), zeroLocus_singleton_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (hypothesis)
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
⊢ 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
have this₁ : 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 _
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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})
⊢ 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
have 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
Tactic: rw [this, ← Polynomial.algebraMap_eq, mem_image_comap_zeroLocus_sdiff,
        IsScalarTower.algebraMap_apply R[X] M, isNilpotent_tensor_residueField_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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]
⊢ ∃ (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
have 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
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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
⊢ ∃ (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
have 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
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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
⊢ ∃ (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
have 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
Tactic: use ∅
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨S, hS, hS'⟩ := H (R₀ := R₀) f
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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
have 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})
Tactic: refine ⟨S, Eq.trans ?_ hS, ?_⟩