awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
Goal:
R₀ : Type u_1
inst : CommRing R₀
n : ℕ
R : Type u_6
inst_1 : CommRing R
inst_2 : Algebra R₀ R
c : R
i : Fin n
e : InductionObj R n
hi : c = (e.val i).leadingCoeff
hc : c ≠ 0
q₁ : R →ₐ[R₀] Localization.Away c := IsScalarTower.toAlgHom R₀ R (Localization.Away c)
q₂ : R →ₐ[R₀] HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}) := Ideal.Quotient.mkₐ R₀ (Ideal.span {c})
q₂_surjective :
  Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})) (⇑q₂ : (a : R) → R ⧸ Ideal.span {c})
e₁ : InductionObj (Localization.Away c) n :=
  {
    val :=
      HSMul.hSMul (α := (Localization.Away c)[X]) (β := Fin n → (Localization.Away c)[X])
        ((Polynomial.C : (a : Localization.Away c) → (Localization.Away c)[X]) (IsLocalization.Away.invSelf c))
        ((⇑(mapRingHom (↑q₁ : R →+* Localization.Away c)) : (a : R[X]) → (Localization.Away c)[X]) ∘ e.val) }
e₂ : InductionObj (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})) n :=
  { val := (⇑(mapRingHom (↑q₂ : R →+* R ⧸ Ideal.span {c})) : (a : R[X]) → (R ⧸ Ideal.span {c})[X]) ∘ e.val }
degBound_e₁_le : e₁.degBound ≤ e.degBound
⊢ (e₂.val i).degree.succ < (e.val i).degree.succ
have refine_2 : (e₂.val i).degree < (e.val i).degree
Tactic: gcongr
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (hypothesis)
Goal:
R₀ : Type u_1
inst : CommRing R₀
n : ℕ
R : Type u_6
inst_1 : CommRing R
inst_2 : Algebra R₀ R
c : R
i : Fin n
e : InductionObj R n
hi : c = (e.val i).leadingCoeff
hc : c ≠ 0
q₁ : R →ₐ[R₀] Localization.Away c := IsScalarTower.toAlgHom R₀ R (Localization.Away c)
q₂ : R →ₐ[R₀] HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}) := Ideal.Quotient.mkₐ R₀ (Ideal.span {c})
q₂_surjective :
  Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})) (⇑q₂ : (a : R) → R ⧸ Ideal.span {c})
e₁ : InductionObj (Localization.Away c) n :=
  {
    val :=
      HSMul.hSMul (α := (Localization.Away c)[X]) (β := Fin n → (Localization.Away c)[X])
        ((Polynomial.C : (a : Localization.Away c) → (Localization.Away c)[X]) (IsLocalization.Away.invSelf c))
        ((⇑(mapRingHom (↑q₁ : R →+* Localization.Away c)) : (a : R[X]) → (Localization.Away c)[X]) ∘ e.val) }
e₂ : InductionObj (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})) n :=
  { val := (⇑(mapRingHom (↑q₂ : R →+* R ⧸ Ideal.span {c})) : (a : R[X]) → (R ⧸ Ideal.span {c})[X]) ∘ e.val }
degBound_e₁_le : e₁.degBound ≤ e.degBound
⊢ Statement R₀ (Localization.Away c) n
      {
        val :=
          HSMul.hSMul (α := (Localization.Away c)[X]) (β := Fin n → (Localization.Away c)[X])
            ((Polynomial.C : (a : Localization.Away c) → (Localization.Away c)[X]) (IsLocalization.Away.invSelf c))
            ((⇑(mapRingHom (algebraMap R (Localization.Away c))) : (a : R[X]) → (Localization.Away c)[X]) ∘ e.val) :
        InductionObj (Localization.Away c) n } →
    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 } →
      Statement R₀ R n e
have degBound_e₂_lt : e₂.degBound < e.degBound
Tactic: have degBound_e₂_lt : e₂.degBound < e.degBound := by
    unfold degBound
    refine Fintype.sum_strictMono <| Pi.lt_def.2 ⟨fun j ↦ ?_, i, ?_⟩
    · dsimp
      gcongr
      exact degree_map_le
    · gcongr
      exact degree_map_lt (by simp [q₂, ← hi]) (by simpa [hi] using hc)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
Goal:
R₀ : Type u_1
inst : CommRing R₀
n : ℕ
R : Type u_6
inst_1 : CommRing R
inst_2 : Algebra R₀ R
c : R
i : Fin n
e : InductionObj R n
hi : c = (e.val i).leadingCoeff
hc : c ≠ 0
q₁ : R →ₐ[R₀] Localization.Away c := IsScalarTower.toAlgHom R₀ R (Localization.Away c)
q₂ : R →ₐ[R₀] HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}) := Ideal.Quotient.mkₐ R₀ (Ideal.span {c})
q₂_surjective :
  Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})) (⇑q₂ : (a : R) → R ⧸ Ideal.span {c})
e₁ : InductionObj (Localization.Away c) n :=
  {
    val :=
      HSMul.hSMul (α := (Localization.Away c)[X]) (β := Fin n → (Localization.Away c)[X])
        ((Polynomial.C : (a : Localization.Away c) → (Localization.Away c)[X]) (IsLocalization.Away.invSelf c))
        ((⇑(mapRingHom (↑q₁ : R →+* Localization.Away c)) : (a : R[X]) → (Localization.Away c)[X]) ∘ e.val) }
e₂ : InductionObj (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})) n :=
  { val := (⇑(mapRingHom (↑q₂ : R →+* R ⧸ Ideal.span {c})) : (a : R[X]) → (R ⧸ Ideal.span {c})[X]) ∘ e.val }
degBound_e₁_le : e₁.degBound ≤ e.degBound
degBound_e₂_lt : e₂.degBound < e.degBound
H₁ : Statement R₀ (Localization.Away c) n e₁
⊢ 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 } →
    Statement R₀ R n e
have Statement : ∀ (H₂ : Statement R₀ (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})) n e₂), Statement R₀ R n e
Tactic: (H₂ : Statement R₀ _ _ e₂)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
Goal:
R₀ : Type u_1
inst : CommRing R₀
n : ℕ
R : Type u_6
inst_1 : CommRing R
inst_2 : Algebra R₀ R
c : R
i : Fin n
e : InductionObj R n
hi : c = (e.val i).leadingCoeff
hc : c ≠ 0
q₁ : R →ₐ[R₀] Localization.Away c := IsScalarTower.toAlgHom R₀ R (Localization.Away c)
q₂ : R →ₐ[R₀] HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}) := Ideal.Quotient.mkₐ R₀ (Ideal.span {c})
q₂_surjective :
  Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})) (⇑q₂ : (a : R) → R ⧸ Ideal.span {c})
e₁ : InductionObj (Localization.Away c) n :=
  {
    val :=
      HSMul.hSMul (α := (Localization.Away c)[X]) (β := Fin n → (Localization.Away c)[X])
        ((Polynomial.C : (a : Localization.Away c) → (Localization.Away c)[X]) (IsLocalization.Away.invSelf c))
        ((⇑(mapRingHom (↑q₁ : R →+* Localization.Away c)) : (a : R[X]) → (Localization.Away c)[X]) ∘ e.val) }
e₂ : InductionObj (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})) n :=
  { val := (⇑(mapRingHom (↑q₂ : R →+* R ⧸ Ideal.span {c})) : (a : R[X]) → (R ⧸ Ideal.span {c})[X]) ∘ e.val }
degBound_e₁_le : e₁.degBound ≤ e.degBound
degBound_e₂_lt : e₂.degBound < e.degBound
H₁ : Statement R₀ (Localization.Away c) n e₁
H₂ : Statement R₀ (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})) n e₂
f : R[X]
⊢ ∃ (T : ConstructibleSetData R),
    comap Polynomial.C '' (zeroLocus (Set.range e.val) \ zeroLocus {f}) = T.toSet ∧
      ∀ C ∈ T,
        C.n ≤ e.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ e) e.powBound
have obtain : ∀ (T₁ : ConstructibleSetData (Localization.Away c))
  (hT₁ :
    comap Polynomial.C ''
          (zeroLocus (Set.range e₁.val) \
            zeroLocus
              (singleton (α := (Localization.Away c)[X])
                ((mapRingHom (↑q₁ : R →+* Localization.Away c) : (a : R[X]) → (Localization.Away c)[X]) f :
                  (Localization.Away c)[X]))) =
        T₁.toSet ∧
      ∀ C ∈ T₁,
        C.n ≤ e₁.degBound ∧
          ∀ (i : Fin C.n),
            C.g i ∈ HPow.hPow (α := Submodule R₀ (Localization.Away c)) (coeffSubmodule R₀ e₁) e₁.powBound),
  ∃ (T : ConstructibleSetData R),
    comap Polynomial.C '' (zeroLocus (Set.range e.val) \ zeroLocus {f}) = T.toSet ∧
      ∀ C ∈ T,
        C.n ≤ e.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ e) e.powBound
Tactic: obtain ⟨T₁, hT₁⟩ := H₁ (mapRingHom q₁ f)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
Goal:
R₀ : Type u_1
inst : CommRing R₀
n : ℕ
R : Type u_6
inst_1 : CommRing R
inst_2 : Algebra R₀ R
c : R
i : Fin n
e : InductionObj R n
hi : c = (e.val i).leadingCoeff
hc : c ≠ 0
q₁ : R →ₐ[R₀] Localization.Away c := IsScalarTower.toAlgHom R₀ R (Localization.Away c)
q₂ : R →ₐ[R₀] HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}) := Ideal.Quotient.mkₐ R₀ (Ideal.span {c})
q₂_surjective :
  Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})) (⇑q₂ : (a : R) → R ⧸ Ideal.span {c})
e₁ : InductionObj (Localization.Away c) n :=
  {
    val :=
      HSMul.hSMul (α := (Localization.Away c)[X]) (β := Fin n → (Localization.Away c)[X])
        ((Polynomial.C : (a : Localization.Away c) → (Localization.Away c)[X]) (IsLocalization.Away.invSelf c))
        ((⇑(mapRingHom (↑q₁ : R →+* Localization.Away c)) : (a : R[X]) → (Localization.Away c)[X]) ∘ e.val) }
e₂ : InductionObj (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})) n :=
  { val := (⇑(mapRingHom (↑q₂ : R →+* R ⧸ Ideal.span {c})) : (a : R[X]) → (R ⧸ Ideal.span {c})[X]) ∘ e.val }
degBound_e₁_le : e₁.degBound ≤ e.degBound
degBound_e₂_lt : e₂.degBound < e.degBound
H₁ : Statement R₀ (Localization.Away c) n e₁
H₂ : Statement R₀ (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})) n e₂
f : R[X]
T₁ : ConstructibleSetData (Localization.Away c)
hT₁ :
  comap Polynomial.C ''
        (zeroLocus (Set.range e₁.val) \
          zeroLocus
            (singleton (α := (Localization.Away c)[X])
              ((mapRingHom (↑q₁ : R →+* Localization.Away c) : (a : R[X]) → (Localization.Away c)[X]) f :
                (Localization.Away c)[X]))) =
      T₁.toSet ∧
    ∀ C ∈ T₁,
      C.n ≤ e₁.degBound ∧
        ∀ (i : Fin C.n), C.g i ∈ HPow.hPow (α := Submodule R₀ (Localization.Away c)) (coeffSubmodule R₀ e₁) e₁.powBound
⊢ ∃ (T : ConstructibleSetData R),
    comap Polynomial.C '' (zeroLocus (Set.range e.val) \ zeroLocus {f}) = T.toSet ∧
      ∀ C ∈ T,
        C.n ≤ e.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ e) e.powBound
have obtain : ∀ (T₂ : ConstructibleSetData (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})))
  (hT₂ :
    comap Polynomial.C ''
          (zeroLocus (Set.range e₂.val) \
            zeroLocus
              (singleton (α := (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))[X])
                ((mapRingHom (↑q₂ : R →+* R ⧸ Ideal.span {c}) : (a : R[X]) → (R ⧸ Ideal.span {c})[X]) f :
                  (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))[X]))) =
        T₂.toSet ∧
      ∀ C ∈ T₂,
        C.n ≤ e₂.degBound ∧
          ∀ (i : Fin C.n),
            C.g i ∈
              HPow.hPow (α := Submodule R₀ (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})))
                (coeffSubmodule R₀ e₂) e₂.powBound),
  ∃ (T : ConstructibleSetData R),
    comap Polynomial.C '' (zeroLocus (Set.range e.val) \ zeroLocus {f}) = T.toSet ∧
      ∀ C ∈ T,
        C.n ≤ e.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ e) e.powBound
Tactic: obtain ⟨T₂, hT₂⟩ := H₂ (mapRingHom q₂ f)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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
⊢ Statement R₀ R n S
have revert : ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_3 : Algebra R₀ R], Statement R₀ R n S
Tactic: revert R₀
Cleared hypotheses: R₀, inst, inst_2
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
Goal:
R : Type u_2
inst : CommRing R
n : ℕ
S : InductionObj R n
⊢ ∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n S
have revert : ∀ (S : InductionObj R n) {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n S
Tactic: revert S
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
Goal:
R : Type u_2
inst : CommRing R
n : ℕ
⊢ ∀ (S : InductionObj R n) {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n S
have 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 }
Tactic: apply induction_structure
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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 }
⊢ ∀ (S : InductionObj R n) {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n S
have 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
Tactic: apply induction_structure
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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
⊢ ∀ (S : InductionObj R n) {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n S
have 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
Tactic: apply induction_structure
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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
⊢ ∀ (S : InductionObj R n) {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n S
have 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
Tactic: apply induction_structure
-- 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]
⊢ ∃ (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 })
have 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))))
Tactic: refine ⟨(Finset.range (f.natDegree + 2)).image fun j ↦ ⟨f.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
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))))
⊢ ∃ (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 })
have 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 })
Tactic: refine ⟨(Finset.range (f.natDegree + 2)).image fun j ↦ ⟨f.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
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
⊢ 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))))
have h : zeroLocus (Set.range (ι := Fin n) (val { val := 0 })) \ zeroLocus {f} = (↑(basicOpen f) : Set (PrimeSpectrum R[X]))
Tactic: convert! image_comap_C_basicOpen 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
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]))
⊢ 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))))
have 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))ᶜ
Tactic: convert! image_comap_C_basicOpen 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
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
⊢ zeroLocus (Set.range (ι := Fin n) (val { val := 0 })) \ zeroLocus {f} = (↑(basicOpen f) : Set (PrimeSpectrum R[X]))
have h : Eq (α := Set (PrimeSpectrum R[X])) (zeroLocus (Set.range (ι := Fin n) 0) \ zeroLocus {f}) (Set.univ \ zeroLocus {f})
Tactic: simp only [basicOpen_eq_zeroLocus_compl, Set.compl_eq_univ_diff]
-- 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]
⊢ Eq (α := Set (PrimeSpectrum R[X])) (zeroLocus (Set.range (ι := Fin n) 0) \ zeroLocus {f}) (Set.univ \ zeroLocus {f})
have h : Eq.{u_2 + 1} (α := Set (PrimeSpectrum R[X])) (zeroLocus (Set.range (ι := Fin n) 0)) Set.univ
Tactic: congr 1
-- 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]
⊢ Eq.{u_2 + 1} (α := Set (PrimeSpectrum R[X])) (zeroLocus (Set.range (ι := Fin n) 0)) Set.univ
have h : Subset.{u_2} (α := Set (PrimeSpectrum R[X])) Set.univ (zeroLocus (Set.range (ι := Fin n) 0))
Tactic: rw [← Set.univ_subset_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
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
⊢ 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))ᶜ
have h : coeff(f) = ⋃ (i : ℕ), ⋃ (_ : i < f.natDegree + 2), {f.coeff i}
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]
-- 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]
⊢ coeff(f) = ⋃ (i : ℕ), ⋃ (_ : i < f.natDegree + 2), {f.coeff i}
have trans : coeff(f) = f.coeff '' Set.Iio (f.natDegree + 2)
Tactic: trans f.coeff '' (Set.Iio (f.natDegree + 2))
-- 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]
trans : coeff(f) = f.coeff '' Set.Iio (f.natDegree + 2)
⊢ coeff(f) = ⋃ (i : ℕ), ⋃ (_ : i < f.natDegree + 2), {f.coeff i}
have trans₁ : f.coeff '' Set.Iio (f.natDegree + 2) = ⋃ (i : ℕ), ⋃ (_ : i < f.natDegree + 2), {f.coeff i}
Tactic: trans f.coeff '' (Set.Iio (f.natDegree + 2))
-- 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]
⊢ coeff(f) = f.coeff '' Set.Iio (f.natDegree + 2)
have refine : coeff(f) ⊆ f.coeff '' Set.Iio (f.natDegree + 2)
Tactic: refine ((Set.image_subset_range _ _).antisymm ?_).symm