awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
f : A
x : PrimeSpectrum R
e :
  A ⊗[R] x.asIdeal.ResidueField ≃ₐ[A]
    TensorProduct.{u_1, u_2, u_1} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span ∅)) x.asIdeal.ResidueField
rw :
  Membership.mem (γ := Set (PrimeSpectrum R)) (comap (algebraMap R A) '' (↑(basicOpen f) : Set (PrimeSpectrum A))) x ↔
    ¬IsNilpotent (R :=
        TensorProduct.{u_1, u_2, u_1} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span ∅)) x.asIdeal.ResidueField)
        ((e : (a : A ⊗[R] x.asIdeal.ResidueField) → (A ⧸ Ideal.span ∅) ⊗[R] x.asIdeal.ResidueField)
            ((algebraMap A (A ⊗[R] x.asIdeal.ResidueField) : (a : A) → A ⊗[R] x.asIdeal.ResidueField) f) :
          TensorProduct.{u_1, u_2, u_1} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span ∅)) x.asIdeal.ResidueField)
rw₁ :
  Membership.mem (γ := Set (PrimeSpectrum R)) (comap (algebraMap R A) '' (↑(basicOpen f) : Set (PrimeSpectrum A))) x ↔
    ¬IsNilpotent (R :=
        TensorProduct.{u_1, u_2, u_1} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span ∅)) x.asIdeal.ResidueField)
        ((algebraMap A
                (TensorProduct.{u_1, u_2, u_1} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span ∅))
                  x.asIdeal.ResidueField) :
              (a : A) → (A ⧸ Ideal.span ∅) ⊗[R] x.asIdeal.ResidueField)
            f :
          TensorProduct.{u_1, u_2, u_1} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span ∅)) x.asIdeal.ResidueField)
rw₂ :
  Membership.mem (γ := Set (PrimeSpectrum R)) (comap (algebraMap R A) '' (↑(basicOpen f) : Set (PrimeSpectrum A))) x ↔
    Membership.mem (γ := Set (PrimeSpectrum R))
      (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (zeroLocus ∅ \ zeroLocus {f})) x
rw₃ :
  Membership.mem (γ := Set (PrimeSpectrum R)) (comap (algebraMap R A) '' (↑(basicOpen f) : Set (PrimeSpectrum A))) x ↔
    Membership.mem (γ := Set (PrimeSpectrum R))
      (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (Set.univ \ zeroLocus {f})) x
rw₄ :
  Membership.mem (γ := Set (PrimeSpectrum R)) (comap (algebraMap R A) '' (↑(basicOpen f) : Set (PrimeSpectrum A))) x ↔
    Membership.mem (γ := Set (PrimeSpectrum R))
      (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (zeroLocus {f})ᶜ) x
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (comap (algebraMap R A) '' (↑(basicOpen f) : Set (PrimeSpectrum A))) x ↔
    ¬IsNilpotent (R := A ⊗[R] x.asIdeal.ResidueField)
        ((algebraMap A (A ⊗[R] x.asIdeal.ResidueField) : (a : A) → A ⊗[R] x.asIdeal.ResidueField) f :
          A ⊗[R] x.asIdeal.ResidueField)
have rw₅ : Membership.mem (γ := Set (PrimeSpectrum R)) (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (zeroLocus {f})ᶜ)
    x ↔
  Membership.mem (γ := Set (PrimeSpectrum R))
    (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (zeroLocus {f})ᶜ) x
Tactic: rw [← IsNilpotent.map_iff e.injective, AlgEquiv.commutes,
    ← mem_image_comap_zeroLocus_sdiff f ∅ x, zeroLocus_empty, ← Set.compl_eq_univ_diff,
    basicOpen_eq_zeroLocus_compl]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_2
A : Type u_1
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
f : A
s : Set A
inst_3 : Module.Finite.{u_2, u_1} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
inst_4 : Module.Free.{u_2, u_1} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
⊢ ∃ (t : Finset R),
    Eq (α := Set (PrimeSpectrum R))
      (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (zeroLocus s \ zeroLocus {f}))
      (zeroLocus (↑t : Set R))ᶜ
have h : Eq (α := Set (PrimeSpectrum R))
  (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (zeroLocus s \ zeroLocus {f}))
  (zeroLocus
      (↑(Finset.image
            (coeff
              (LinearMap.charpoly.{u_2, u_1} (M := HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
                ((Algebra.lmul R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) :
                    (a : A ⧸ Ideal.span s) → Module.End R (A ⧸ Ideal.span s))
                  ((Ideal.Quotient.mk (Ideal.span s) : (a : A) → A ⧸ Ideal.span s) f :
                    HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)))))
            (Finset.range (Module.finrank.{u_2, u_1} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))))) :
        Set R))ᶜ
Tactic: use (Finset.range (Module.finrank R (A ⧸ Ideal.span s))).image
    (Algebra.lmul R (A ⧸ Ideal.span s) (Ideal.Quotient.mk _ f)).charpoly.coeff
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_2
A : Type u_1
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
f : A
s : Set A
inst_3 : Module.Finite.{u_2, u_1} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
inst_4 : Module.Free.{u_2, u_1} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
⊢ Eq (α := Set (PrimeSpectrum R))
    (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (zeroLocus s \ zeroLocus {f}))
    (zeroLocus
        (↑(Finset.image
              (coeff
                (LinearMap.charpoly.{u_2, u_1} (M := HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
                  ((Algebra.lmul R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) :
                      (a : A ⧸ Ideal.span s) → Module.End R (A ⧸ Ideal.span s))
                    ((Ideal.Quotient.mk (Ideal.span s) : (a : A) → A ⧸ Ideal.span s) f :
                      HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)))))
              (Finset.range (Module.finrank.{u_2, u_1} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))))) :
          Set R))ᶜ
have h : ∀ (x : PrimeSpectrum R),
  Membership.mem (γ := Set (PrimeSpectrum R))
      (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (zeroLocus s \ zeroLocus {f})) x ↔
    Membership.mem (γ := Set (PrimeSpectrum R))
      (zeroLocus
          (↑(Finset.image
                (coeff
                  (LinearMap.charpoly.{u_2, u_1} (M := HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
                    ((Algebra.lmul R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) :
                        (a : A ⧸ Ideal.span s) → Module.End R (A ⧸ Ideal.span s))
                      ((Ideal.Quotient.mk (Ideal.span s) : (a : A) → A ⧸ Ideal.span s) f :
                        HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)))))
                (Finset.range (Module.finrank.{u_2, u_1} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))))) :
            Set R))ᶜ
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_2
A : Type u_1
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
f : A
s : Set A
inst_3 : Module.Finite.{u_2, u_1} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
inst_4 : Module.Free.{u_2, u_1} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
x : PrimeSpectrum R
⊢ Membership.mem (γ := Set (PrimeSpectrum R))
      (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (zeroLocus s \ zeroLocus {f})) x ↔
    Membership.mem (γ := Set (PrimeSpectrum R))
      (zeroLocus
          (↑(Finset.image
                (coeff
                  (LinearMap.charpoly.{u_2, u_1} (M := HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
                    ((Algebra.lmul R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) :
                        (a : A ⧸ Ideal.span s) → Module.End R (A ⧸ Ideal.span s))
                      ((Ideal.Quotient.mk (Ideal.span s) : (a : A) → A ⧸ Ideal.span s) f :
                        HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)))))
                (Finset.range (Module.finrank.{u_2, u_1} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))))) :
            Set R))ᶜ
      x
have h : (¬∀ i < Module.finrank.{u_2, u_1} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)),
      coeff
          (LinearMap.charpoly.{u_2, u_1} (M := HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
            ((Algebra.lmul R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) :
                (a : A ⧸ Ideal.span s) → Module.End R (A ⧸ Ideal.span s))
              ((algebraMap A (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) : (a : A) → A ⧸ Ideal.span s) f :
                HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))))
          i ∈
        x.asIdeal) ↔
  Membership.mem (γ := Set (PrimeSpectrum R))
    (zeroLocus
        (↑(Finset.image
              (coeff
                (LinearMap.charpoly.{u_2, u_1} (M := HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
                  ((Algebra.lmul R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) :
                      (a : A ⧸ Ideal.span s) → Module.End R (A ⧸ Ideal.span s))
                    ((Ideal.Quotient.mk (Ideal.span s) : (a : A) → A ⧸ Ideal.span s) f :
                      HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)))))
              (Finset.range (Module.finrank.{u_2, u_1} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))))) :
          Set R))ᶜ
    x
Tactic: rw [mem_image_comap_zeroLocus_sdiff, IsScalarTower.algebraMap_apply A (A ⧸ Ideal.span s),
    isNilpotent_tensor_residueField_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_2
A : Type u_1
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
f : A
s : Set A
inst_3 : Module.Finite.{u_2, u_1} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
inst_4 : Module.Free.{u_2, u_1} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
⊢ ∃ (t : Finset R),
    Eq (α := Set (PrimeSpectrum R))
      (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (zeroLocus s \ zeroLocus {f}))
      (zeroLocus (↑t : Set R))ᶜ
have w : Finset R
Tactic: classical
  use (Finset.range (Module.finrank R (A ⧸ Ideal.span s))).image
    (Algebra.lmul R (A ⧸ Ideal.span s) (Ideal.Quotient.mk _ f)).charpoly.coeff
  ext x
  rw [mem_image_comap_zeroLocus_sdiff, IsScalarTower.algebraMap_apply A (A ⧸ Ideal.span s),
    isNilpotent_tensor_residueField_iff]
  simp [Set.subset_def]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_2
A : Type u_1
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
f : A
s : Set A
inst_3 : Module.Finite.{u_2, u_1} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
inst_4 : Module.Free.{u_2, u_1} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
w : Finset R
⊢ ∃ (t : Finset R),
    Eq (α := Set (PrimeSpectrum R))
      (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (zeroLocus s \ zeroLocus {f}))
      (zeroLocus (↑t : Set R))ᶜ
have h : Eq (α := Set (PrimeSpectrum R))
  (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (zeroLocus s \ zeroLocus {f}))
  (zeroLocus
      (↑(Finset.image
            (coeff
              (LinearMap.charpoly.{u_2, u_1} (M := HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
                ((Algebra.lmul R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) :
                    (a : A ⧸ Ideal.span s) → Module.End R (A ⧸ Ideal.span s))
                  ((Ideal.Quotient.mk (Ideal.span s) : (a : A) → A ⧸ Ideal.span s) f :
                    HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)))))
            (Finset.range (Module.finrank.{u_2, u_1} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))))) :
        Set R))ᶜ
Tactic: classical
  use (Finset.range (Module.finrank R (A ⧸ Ideal.span s))).image
    (Algebra.lmul R (A ⧸ Ideal.span s) (Ideal.Quotient.mk _ f)).charpoly.coeff
  ext x
  rw [mem_image_comap_zeroLocus_sdiff, IsScalarTower.algebraMap_apply A (A ⧸ Ideal.span s),
    isNilpotent_tensor_residueField_iff]
  simp [Set.subset_def]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_2
A : Type u_1
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
f : A
s : Set A
inst_3 : Module.Finite.{u_2, u_1} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
inst_4 : Module.Free.{u_2, u_1} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
w : Finset R
h h₁ :
  Eq (α := Set (PrimeSpectrum R))
    (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (zeroLocus s \ zeroLocus {f}))
    (zeroLocus
        (↑(Finset.image
              (coeff
                (LinearMap.charpoly.{u_2, u_1} (M := HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
                  ((Algebra.lmul R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) :
                      (a : A ⧸ Ideal.span s) → Module.End R (A ⧸ Ideal.span s))
                    ((Ideal.Quotient.mk (Ideal.span s) : (a : A) → A ⧸ Ideal.span s) f :
                      HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)))))
              (Finset.range (Module.finrank.{u_2, u_1} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))))) :
          Set R))ᶜ
⊢ ∃ (t : Finset R),
    Eq (α := Set (PrimeSpectrum R))
      (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (zeroLocus s \ zeroLocus {f}))
      (zeroLocus (↑t : Set R))ᶜ
have h₂ : ∀ (x : PrimeSpectrum R),
  Membership.mem (γ := Set (PrimeSpectrum R))
      (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (zeroLocus s \ zeroLocus {f})) x ↔
    Membership.mem (γ := Set (PrimeSpectrum R))
      (zeroLocus
          (↑(Finset.image
                (coeff
                  (LinearMap.charpoly.{u_2, u_1} (M := HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
                    ((Algebra.lmul R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) :
                        (a : A ⧸ Ideal.span s) → Module.End R (A ⧸ Ideal.span s))
                      ((Ideal.Quotient.mk (Ideal.span s) : (a : A) → A ⧸ Ideal.span s) f :
                        HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)))))
                (Finset.range (Module.finrank.{u_2, u_1} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))))) :
            Set R))ᶜ
      x
Tactic: classical
  use (Finset.range (Module.finrank R (A ⧸ Ideal.span s))).image
    (Algebra.lmul R (A ⧸ Ideal.span s) (Ideal.Quotient.mk _ f)).charpoly.coeff
  ext x
  rw [mem_image_comap_zeroLocus_sdiff, IsScalarTower.algebraMap_apply A (A ⧸ Ideal.span s),
    isNilpotent_tensor_residueField_iff]
  simp [Set.subset_def]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
x : PrimeSpectrum R
⊢ x ∈ comap C '' (↑(basicOpen f) : Set (PrimeSpectrum R[X])) ↔ ∃ (i : ℕ), f.coeff i ∉ x.asIdeal
have trans : x ∈ comap C '' (↑(basicOpen f) : Set (PrimeSpectrum R[X])) ↔
  Ne (α := x.asIdeal.ResidueField[X]) (map (algebraMap R x.asIdeal.ResidueField) f) 0
Tactic: trans f.map (algebraMap R x.asIdeal.ResidueField) ≠ 0
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
x : PrimeSpectrum R
trans :
  x ∈ comap C '' (↑(basicOpen f) : Set (PrimeSpectrum R[X])) ↔
    Ne (α := x.asIdeal.ResidueField[X]) (map (algebraMap R x.asIdeal.ResidueField) f) 0
⊢ x ∈ comap C '' (↑(basicOpen f) : Set (PrimeSpectrum R[X])) ↔ ∃ (i : ℕ), f.coeff i ∉ x.asIdeal
have trans₁ : Ne (α := x.asIdeal.ResidueField[X]) (map (algebraMap R x.asIdeal.ResidueField) f) 0 ↔ ∃ (i : ℕ), f.coeff i ∉ x.asIdeal
Tactic: trans f.map (algebraMap R x.asIdeal.ResidueField) ≠ 0
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
x : PrimeSpectrum R
⊢ x ∈ comap C '' (↑(basicOpen f) : Set (PrimeSpectrum R[X])) ↔
    Ne (α := x.asIdeal.ResidueField[X]) (map (algebraMap R x.asIdeal.ResidueField) f) 0
have refine : IsNilpotent (R := R[X] ⊗[R] x.asIdeal.ResidueField)
    ((algebraMap R[X] (R[X] ⊗[R] x.asIdeal.ResidueField) : (a : R[X]) → R[X] ⊗[R] x.asIdeal.ResidueField) f :
      R[X] ⊗[R] x.asIdeal.ResidueField) ↔
  Eq (α := x.asIdeal.ResidueField[X]) (map (algebraMap R x.asIdeal.ResidueField) f) 0
Tactic: refine (mem_image_comap_basicOpen _ _).trans (not_iff_not.mpr ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
x : PrimeSpectrum R
e : R[X] ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] x.asIdeal.ResidueField[X] :=
  AlgEquiv.trans (Algebra.TensorProduct.comm R R[X] x.asIdeal.ResidueField)
    (AlgEquiv.symm (polyEquivTensor R x.asIdeal.ResidueField))
⊢ IsNilpotent (R := R[X] ⊗[R] x.asIdeal.ResidueField)
      ((algebraMap R[X] (R[X] ⊗[R] x.asIdeal.ResidueField) : (a : R[X]) → R[X] ⊗[R] x.asIdeal.ResidueField) f :
        R[X] ⊗[R] x.asIdeal.ResidueField) ↔
    Eq (α := x.asIdeal.ResidueField[X]) (map (algebraMap R x.asIdeal.ResidueField) f) 0
have rw : Eq (α := x.asIdeal.ResidueField[X])
    ((e : (a : R[X] ⊗[R] x.asIdeal.ResidueField) → x.asIdeal.ResidueField[X])
        ((algebraMap R[X] (R[X] ⊗[R] x.asIdeal.ResidueField) : (a : R[X]) → R[X] ⊗[R] x.asIdeal.ResidueField) f) :
      x.asIdeal.ResidueField[X])
    (0 : x.asIdeal.ResidueField[X]) ↔
  Eq (α := x.asIdeal.ResidueField[X]) (map (algebraMap R x.asIdeal.ResidueField) f) 0
Tactic: rw [← IsNilpotent.map_iff e.injective, isNilpotent_iff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
⊢ comap C '' (↑(basicOpen f) : Set (PrimeSpectrum R[X])) = (zeroLocus (Set.range f.coeff))ᶜ
have h : ∀ (p : PrimeSpectrum R),
  p ∈ comap C '' (↑(basicOpen f) : Set (PrimeSpectrum R[X])) ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (Set.range f.coeff))ᶜ p
Tactic: ext p
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
p : PrimeSpectrum R
⊢ p ∈ comap C '' (↑(basicOpen f) : Set (PrimeSpectrum R[X])) ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (Set.range f.coeff))ᶜ p
have h : (∃ (i : ℕ), f.coeff i ∉ p.asIdeal) ↔ Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (Set.range f.coeff))ᶜ p
Tactic: rw [mem_image_comap_C_basicOpen]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
U : Set (PrimeSpectrum R[X])
hU : IsOpen U
⊢ IsOpen (comap C '' U)
have obtain : ∀ (S : Set (Set (PrimeSpectrum R[X]))) (hS : S ⊆ Set.range fun (r : R[X]) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R[X])))
  (hU : IsOpen (⋃₀ S)), IsOpen (comap C '' ⋃₀ S)
Tactic: obtain ⟨S, hS, rfl⟩ := isTopologicalBasis_basic_opens.open_eq_sUnion hU
Cleared hypotheses: U, hU
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Set (Set (PrimeSpectrum R[X]))
hS : S ⊆ Set.range fun (r : R[X]) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R[X]))
hU : IsOpen (⋃₀ S)
⊢ IsOpen (comap C '' ⋃₀ S)
have rw : IsOpen (⋃₀ (Set.image (comap C) '' S))
Tactic: rw [Set.image_sUnion]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Set (Set (PrimeSpectrum R[X]))
hS : S ⊆ Set.range fun (r : R[X]) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R[X]))
hU : IsOpen (⋃₀ S)
⊢ IsOpen (⋃₀ (Set.image (comap C) '' S))
have h : ∀ t ∈ Set.image (comap C) '' S, IsOpen t
Tactic: apply isOpen_sUnion
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Set (Set (PrimeSpectrum R[X]))
hS : S ⊆ Set.range fun (r : R[X]) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R[X]))
hU : IsOpen (⋃₀ S)
t : Set (PrimeSpectrum R[X])
ht : t ∈ S
⊢ IsOpen (comap C '' t)
have h : ∀ (r : R[X]) (ht : (fun (r : R[X]) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R[X]))) r ∈ S),
  IsOpen.{u_1} (X := PrimeSpectrum R) (comap C '' (fun (r : R[X]) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R[X]))) r)
Tactic: obtain ⟨r, rfl⟩ := hS ht
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Set (Set (PrimeSpectrum R[X]))
hS : S ⊆ Set.range fun (r : R[X]) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R[X]))
hU : IsOpen (⋃₀ S)
r : R[X]
ht : (fun (r : R[X]) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R[X]))) r ∈ S
⊢ IsOpen.{u_1} (X := PrimeSpectrum R) (comap C '' (fun (r : R[X]) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R[X]))) r)
have h : IsOpen (X := PrimeSpectrum R) (zeroLocus (Set.range r.coeff))ᶜ
Tactic: simp only [image_comap_C_basicOpen]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
x : PrimeSpectrum R
⊢ ∃ (a : PrimeSpectrum R[X]), comap C a = x
have refine : comap C (comap (evalRingHom 0) x) = x
Tactic: refine ⟨comap (evalRingHom 0) x, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
x : PrimeSpectrum R
⊢ Eq (α := R →+* R) (RingHom.comp (evalRingHom 0) C) (RingHom.id R)
have a : ∀ (x : R), Eq (α := R) ((RingHom.comp (evalRingHom 0) C : (a : R) → R) x : R) ((RingHom.id R : (a : R) → R) x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
x : PrimeSpectrum R
⊢ comap C (comap (evalRingHom 0) x) = x
have rw : comap (RingHom.comp (evalRingHom 0) C) x = x
Tactic: rw [← comap_comp_apply, (show (evalRingHom 0).comp C = .id R by ext; simp),
    comap_id]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
x : PrimeSpectrum R
rw : comap (RingHom.comp (evalRingHom 0) C) x = x
⊢ comap C (comap (evalRingHom 0) x) = x
have rw₁ : comap (RingHom.id R) x = x
Tactic: rw [← comap_comp_apply, (show (evalRingHom 0).comp C = .id R by ext; simp),
    comap_id]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
x : PrimeSpectrum R
rw : comap (RingHom.comp (evalRingHom 0) C) x = x
rw₁ : comap (RingHom.id R) x = x
⊢ comap C (comap (evalRingHom 0) x) = x
have rw₂ : (fun (x : PrimeSpectrum R) ↦ x) x = x
Tactic: rw [← comap_comp_apply, (show (evalRingHom 0).comp C = .id R by ext; simp),
    comap_id]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hg : g.Monic
⊢ ∃ (t : Finset R),
    Eq (α := Set (PrimeSpectrum R)) (comap C '' (zeroLocus {g} \ zeroLocus {f})) (zeroLocus (↑t : Set R))ᶜ
have inst : Module.Finite R (HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.span {g}))
Tactic: apply +allowSynthFailures exists_image_comap_of_finite_of_free
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_1
inst_1 : CommRing R
f g : R[X]
hg : g.Monic
inst : Module.Finite R (HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.span {g}))
⊢ ∃ (t : Finset R),
    Eq (α := Set (PrimeSpectrum R)) (comap C '' (zeroLocus {g} \ zeroLocus {f})) (zeroLocus (↑t : Set R))ᶜ
have inst₁ : Module.Free R (HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.span {g}))
Tactic: apply +allowSynthFailures exists_image_comap_of_finite_of_free
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hg : g.Monic
⊢ IsCompact (X := PrimeSpectrum R) (comap C '' (zeroLocus {g} \ zeroLocus {f}))
have obtain : ∀ (t : Finset R)
  (ht : Eq (α := Set (PrimeSpectrum R)) (comap C '' (zeroLocus {g} \ zeroLocus {f})) (zeroLocus (↑t : Set R))ᶜ),
  IsCompact (X := PrimeSpectrum R) (comap C '' (zeroLocus {g} \ zeroLocus {f}))
Tactic: obtain ⟨t, ht⟩ := exists_image_comap_of_monic f g hg
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hg : g.Monic
t : Finset R
ht : Eq (α := Set (PrimeSpectrum R)) (comap C '' (zeroLocus {g} \ zeroLocus {f})) (zeroLocus (↑t : Set R))ᶜ
⊢ IsCompact (X := PrimeSpectrum R) (comap C '' (zeroLocus {g} \ zeroLocus {f}))
have rw : IsCompact.{u_1} (X := PrimeSpectrum R) (⋃ (i : (↑(↑t : Set R) : Type u_1)), (zeroLocus {(↑i : R)})ᶜ)
Tactic: rw [ht, ← (t : Set R).iUnion_of_singleton_coe, zeroLocus_iUnion, Set.compl_iInter]