awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
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
x : PrimeSpectrum R
q :
  Ideal (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField)
hq : q.IsPrime
hfq :
  ((Ideal.Quotient.mk (Ideal.span s) : (a : A) → A ⧸ Ideal.span s) f ⊗ₜ[R] 1 :
      TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField) ∉
    q
this :
  ∀ a ∈ s,
    Membership.mem (α :=
      TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField) q
      ((Ideal.Quotient.mk (Ideal.span s) : (a : A) → A ⧸ Ideal.span s) a ⊗ₜ[R] 1 :
        TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField)
mpr : comap (S := x.asIdeal.ResidueField) (algebraMap R x.asIdeal.ResidueField) ⊥ = x
⊢ comap (algebraMap R A)
      (comap
        (algebraMap A
          (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
            x.asIdeal.ResidueField))
        { asIdeal := q, isPrime := hq :
          PrimeSpectrum
            (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
              x.asIdeal.ResidueField) }) =
    x

Tactic:
rw [← comap_comp_apply, ← IsScalarTower.algebraMap_eq,
      ← Algebra.TensorProduct.includeRight.comp_algebraMap, comap_comp_apply,
      Subsingleton.elim (α := PrimeSpectrum x.asIdeal.ResidueField) (comap _ _) ⊥]

Premises used: AlgHom.comp_algebraMap, PrimeSpectrum.comap_comp_apply, Bot.bot, IsScalarTower.algebraMap_eq, PrimeSpectrum.comap, Subsingleton.elim, Algebra.TensorProduct.includeRight
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
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
x : PrimeSpectrum R
q :
  Ideal (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField)
hq : q.IsPrime
hfq :
  ((Ideal.Quotient.mk (Ideal.span s) : (a : A) → A ⧸ Ideal.span s) f ⊗ₜ[R] 1 :
      TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField) ∉
    q
this :
  ∀ a ∈ s,
    Membership.mem (α :=
      TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField) q
      ((Ideal.Quotient.mk (Ideal.span s) : (a : A) → A ⧸ Ideal.span s) a ⊗ₜ[R] 1 :
        TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField)
mpr :
  ∀ (a : R),
    Membership.mem (γ := Ideal R)
        (asIdeal (comap (S := x.asIdeal.ResidueField) (algebraMap R x.asIdeal.ResidueField) ⊥)) a ↔
      a ∈ x.asIdeal
⊢ comap (S := x.asIdeal.ResidueField) (algebraMap R x.asIdeal.ResidueField) ⊥ = x

Tactic:
ext a
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
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
x : PrimeSpectrum R
q :
  Ideal (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField)
hq : q.IsPrime
hfq :
  ((Ideal.Quotient.mk (Ideal.span s) : (a : A) → A ⧸ Ideal.span s) f ⊗ₜ[R] 1 :
      TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField) ∉
    q
this :
  ∀ a ∈ s,
    Membership.mem (α :=
      TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField) q
      ((Ideal.Quotient.mk (Ideal.span s) : (a : A) → A ⧸ Ideal.span s) a ⊗ₜ[R] 1 :
        TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField)
a : R
⊢ Membership.mem (γ := Ideal R) (asIdeal (comap (S := x.asIdeal.ResidueField) (algebraMap R x.asIdeal.ResidueField) ⊥))
      a ↔
    a ∈ x.asIdeal

Tactic:
congr(a ∈ $(Ideal.ker_algebraMap_residueField _))

Premises used: Ideal.ker_algebraMap_residueField, congrArg, Membership.mem, id, PrimeSpectrum.asIdeal, iff_of_eq
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
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
x : PrimeSpectrum R
q :
  Ideal (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField)
hq : q.IsPrime
hfq :
  ((Ideal.Quotient.mk (Ideal.span s) : (a : A) → A ⧸ Ideal.span s) f ⊗ₜ[R] 1 :
      TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField) ∉
    q
this :
  ∀ a ∈ s,
    Membership.mem (α :=
      TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField) q
      ((Ideal.Quotient.mk (Ideal.span s) : (a : A) → A ⧸ Ideal.span s) a ⊗ₜ[R] 1 :
        TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField)
a : R
⊢ Membership.mem (γ := Ideal R) (asIdeal (comap (S := x.asIdeal.ResidueField) (algebraMap R x.asIdeal.ResidueField) ⊥))
      a ↔
    a ∈ x.asIdeal

Tactic:
exact congr(a ∈ $(Ideal.ker_algebraMap_residueField _))

Premises used: Ideal.ker_algebraMap_residueField
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
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
f₁ : A ≃ₐ[A] HasQuotient.Quotient A (B := Ideal A) (Ideal.span ∅)
⊢ 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

Tactic:
refine Algebra.TensorProduct.congr ?f AlgEquiv.refl

Premises used: Algebra.TensorProduct.congr, AlgEquiv.refl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
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
f₁ : A ≃ₐ[A] HasQuotient.Quotient A (B := Ideal A) ⊥
⊢ A ≃ₐ[A] HasQuotient.Quotient A (B := Ideal A) (Ideal.span ∅)

Tactic:
rw [Ideal.span_empty]

Premises used: Ideal.span_empty
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
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
⊢ A ≃ₐ[A] HasQuotient.Quotient A (B := Ideal A) ⊥

Tactic:
exact { __ := (RingEquiv.quotientBot A).symm, __ := Algebra.ofId _ _ }

Premises used: Algebra.ofId, RingEquiv.symm, RingEquiv.quotientBot
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
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
have :
  ∀
    (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),
    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)
⊢ 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)

Tactic:
have e : A ⊗[R] x.asIdeal.ResidueField ≃ₐ[A]
      (A ⧸ (Ideal.span ∅ : Ideal A)) ⊗[R] x.asIdeal.ResidueField := by
    refine Algebra.TensorProduct.congr ?f AlgEquiv.refl
    rw [Ideal.span_empty]
    exact { __ := (RingEquiv.quotientBot A).symm, __ := Algebra.ofId _ _ }
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
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))
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))ᶜ

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

Premises used: Algebra.lmul, Ideal.Quotient.mk, Polynomial.coeff, Finset.range, HasQuotient.Quotient, Ideal.span, DFunLike.coe, Finset.image, LinearMap.charpoly, Module.finrank
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
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))
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
⊢ 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:
ext x
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
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
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
⊢ 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:
rw [mem_image_comap_zeroLocus_sdiff, IsScalarTower.algebraMap_apply A (A ⧸ Ideal.span s),
    isNilpotent_tensor_residueField_iff]

Premises used: HasQuotient.Quotient, isNilpotent_tensor_residueField_iff, Ideal.span, PrimeSpectrum.mem_image_comap_zeroLocus_sdiff, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
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
⊢ (¬∀ 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:
simp [Set.subset_def]

Premises used: Set.subset_def
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
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
trans₁ :
  Ne (α := x.asIdeal.ResidueField[X]) (map (algebraMap R x.asIdeal.ResidueField) f) 0 ↔ ∃ (i : ℕ), f.coeff i ∉ x.asIdeal
⊢ x ∈ comap C '' (↑(basicOpen f) : Set (PrimeSpectrum R[X])) ↔ ∃ (i : ℕ), f.coeff i ∉ x.asIdeal

Tactic:
trans f.map (algebraMap R x.asIdeal.ResidueField) ≠ 0

Premises used: Algebra.algebraMap, Ideal.ResidueField, Polynomial.map, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
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

Tactic:
(mem_image_comap_basicOpen _ _).trans (not_iff_not.mpr ?_)

Premises used: not_iff_not, Iff.mpr, Polynomial.C, Set.Mem, PrimeSpectrum.mem_image_comap_basicOpen, Iff.trans
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
x : PrimeSpectrum R
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
⊢ x ∈ comap C '' (↑(basicOpen f) : Set (PrimeSpectrum R[X])) ↔
    Ne (α := x.asIdeal.ResidueField[X]) (map (algebraMap R x.asIdeal.ResidueField) f) 0

Tactic:
refine (mem_image_comap_basicOpen _ _).trans (not_iff_not.mpr ?_)

Premises used: not_iff_not, Iff.mpr, PrimeSpectrum.mem_image_comap_basicOpen, Iff.trans
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
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))
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
⊢ 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:
rw [← IsNilpotent.map_iff e.injective, isNilpotent_iff_eq_zero]

Premises used: isNilpotent_iff_eq_zero, IsNilpotent.map_iff, AlgEquiv.injective
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
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))
⊢ 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:
simp [e]
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
x : PrimeSpectrum R
⊢ Ne (α := x.asIdeal.ResidueField[X]) (map (algebraMap R x.asIdeal.ResidueField) f) 0 ↔ ∃ (i : ℕ), f.coeff i ∉ x.asIdeal

Tactic:
simp [Polynomial.ext_iff]

Premises used: Polynomial.ext_iff
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
h :
  ∀ (p : PrimeSpectrum R),
    p ∈ comap C '' (↑(basicOpen f) : Set (PrimeSpectrum R[X])) ↔
      Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (Set.range f.coeff))ᶜ p
⊢ comap C '' (↑(basicOpen f) : Set (PrimeSpectrum R[X])) = (zeroLocus (Set.range f.coeff))ᶜ

Tactic:
ext p
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
p : PrimeSpectrum R
h : (∃ (i : ℕ), f.coeff i ∉ p.asIdeal) ↔ Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (Set.range f.coeff))ᶜ p
⊢ p ∈ comap C '' (↑(basicOpen f) : Set (PrimeSpectrum R[X])) ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (Set.range f.coeff))ᶜ p

Tactic:
rw [mem_image_comap_C_basicOpen]

Premises used: Polynomial.mem_image_comap_C_basicOpen
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
p : PrimeSpectrum R
⊢ (∃ (i : ℕ), f.coeff i ∉ p.asIdeal) ↔ Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (Set.range f.coeff))ᶜ p

Tactic:
simp [Set.range_subset_iff]

Premises used: Set.range_subset_iff
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_1
inst : CommRing R
U : Set (PrimeSpectrum R[X])
hU : IsOpen U
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)
⊢ IsOpen (comap C '' U)

Tactic:
obtain ⟨S, hS, rfl⟩ := isTopologicalBasis_basic_opens.open_eq_sUnion hU

Premises used: TopologicalSpace.IsTopologicalBasis.open_eq_sUnion, PrimeSpectrum.isTopologicalBasis_basic_opens, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
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)
rw : IsOpen (⋃₀ (Set.image (comap C) '' S))
⊢ IsOpen (comap C '' ⋃₀ S)

Tactic:
rw [Set.image_sUnion]

Premises used: Set.image_sUnion
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
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)
h : ∀ t ∈ Set.image (comap C) '' S, IsOpen t
⊢ IsOpen (⋃₀ (Set.image (comap C) '' S))

Tactic:
apply isOpen_sUnion

Premises used: isOpen_sUnion
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
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
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)
⊢ IsOpen (comap C '' t)

Tactic:
obtain ⟨r, rfl⟩ := hS ht

Premises used: rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
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
h : IsOpen (X := PrimeSpectrum R) (zeroLocus (Set.range r.coeff))ᶜ
⊢ IsOpen.{u_1} (X := PrimeSpectrum R) (comap C '' (fun (r : R[X]) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R[X]))) r)

Tactic:
simp only [image_comap_C_basicOpen]

Premises used: Polynomial.image_comap_C_basicOpen
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
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 (X := PrimeSpectrum R) (zeroLocus (Set.range r.coeff))ᶜ

Tactic:
(isClosed_zeroLocus _).isOpen_compl

Premises used: IsClosed.isOpen_compl