awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact (isClosed_zeroLocus _).isOpen_compl

Premises used: IsClosed.isOpen_compl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_1
inst : CommRing R
x : PrimeSpectrum R
⊢ ∃ (a : PrimeSpectrum R[X]), comap C a = x

Tactic:
⟨comap (evalRingHom 0) x, ?_⟩

Premises used: Exists.intro, Polynomial.evalRingHom, PrimeSpectrum.comap, OfNat.ofNat
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_1
inst : CommRing R
x : PrimeSpectrum R
refine : comap C (comap (evalRingHom 0) x) = x
⊢ ∃ (a : PrimeSpectrum R[X]), comap C a = x

Tactic:
refine ⟨comap (evalRingHom 0) x, ?_⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_1
inst : CommRing R
x : PrimeSpectrum R
a : ∀ (x : R), Eq (α := R) ((RingHom.comp (evalRingHom 0) C : (a : R) → R) x : R) ((RingHom.id R : (a : R) → R) x : R)
⊢ Eq (α := R →+* R) (RingHom.comp (evalRingHom 0) C) (RingHom.id R)

Tactic:
ext
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_1
inst : CommRing R
x : PrimeSpectrum R
x_1 : R
⊢ Eq (α := R) ((RingHom.comp (evalRingHom 0) C : (a : R) → R) x_1 : R) ((RingHom.id R : (a : R) → R) x_1 : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
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
rw₂ rw₃ : (fun (x : PrimeSpectrum R) ↦ x) x = x
⊢ comap C (comap (evalRingHom 0) x) = x

Tactic:
rw [← comap_comp_apply, (show (evalRingHom 0).comp C = .id R by ext; simp),
    comap_id]

Premises used: PrimeSpectrum.comap_comp_apply, PrimeSpectrum.comap_id
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
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}))
inst₁ : Module.Free 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))ᶜ

Tactic:
apply +allowSynthFailures exists_image_comap_of_finite_of_free

Premises used: PrimeSpectrum.exists_image_comap_of_finite_of_free
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hg : g.Monic
⊢ Module.Finite R (HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.span {g}))

Tactic:
.of_basis (AdjoinRoot.powerBasis' hg).basis

Premises used: PowerBasis.basis, Module.Finite.of_basis, AdjoinRoot.powerBasis'
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hg : g.Monic
⊢ Module.Finite R (HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.span {g}))

Tactic:
exact .of_basis (AdjoinRoot.powerBasis' hg).basis
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hg : g.Monic
⊢ Module.Free R (HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.span {g}))

Tactic:
.of_basis (AdjoinRoot.powerBasis' hg).basis

Premises used: PowerBasis.basis, Module.Free.of_basis, AdjoinRoot.powerBasis'
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hg : g.Monic
⊢ Module.Free R (HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.span {g}))

Tactic:
exact .of_basis (AdjoinRoot.powerBasis' hg).basis
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hg : g.Monic
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}))
⊢ IsCompact (X := PrimeSpectrum R) (comap C '' (zeroLocus {g} \ zeroLocus {f}))

Tactic:
obtain ⟨t, ht⟩ := exists_image_comap_of_monic f g hg

Premises used: Polynomial.exists_image_comap_of_monic
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
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))ᶜ
rw : IsCompact.{u_1} (X := PrimeSpectrum R) (⋃ (i : (↑(↑t : Set R) : Type u_1)), (zeroLocus {(↑i : R)})ᶜ)
⊢ IsCompact (X := PrimeSpectrum R) (comap C '' (zeroLocus {g} \ zeroLocus {f}))

Tactic:
rw [ht, ← (t : Set R).iUnion_of_singleton_coe, zeroLocus_iUnion, Set.compl_iInter]

Premises used: Set.compl_iInter, PrimeSpectrum.zeroLocus_iUnion, SetLike.coe, Set.iUnion_of_singleton_coe
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
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))ᶜ
h : ∀ (i : (↑(↑t : Set R) : Type u_1)), IsCompact (X := PrimeSpectrum R) (zeroLocus {(↑i : R)})ᶜ
⊢ IsCompact.{u_1} (X := PrimeSpectrum R) (⋃ (i : (↑(↑t : Set R) : Type u_1)), (zeroLocus {(↑i : R)})ᶜ)

Tactic:
apply isCompact_iUnion

Premises used: isCompact_iUnion
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
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))ᶜ
x : (↑(↑t : Set R) : Type u_1)
⊢ IsCompact (X := PrimeSpectrum R) (zeroLocus {(↑x : R)})ᶜ

Tactic:
simpa using isCompact_basicOpen _

Premises used: PrimeSpectrum.isCompact_basicOpen
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
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))ᶜ
⊢ ∀ (i : (↑(↑t : Set R) : Type u_1)), IsCompact (X := PrimeSpectrum R) (zeroLocus {(↑i : R)})ᶜ

Tactic:
exact fun _ ↦ by simpa using isCompact_basicOpen _
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hg : g.Monic
obtain :
  ∀ (t : Finset R)
    (ht : Eq (α := Set (PrimeSpectrum R)) (comap C '' (zeroLocus {g} \ zeroLocus {f})) (zeroLocus (↑t : Set R))ᶜ),
    IsOpen (X := PrimeSpectrum R) (comap C '' (zeroLocus {g} \ zeroLocus {f}))
⊢ IsOpen (X := PrimeSpectrum R) (comap C '' (zeroLocus {g} \ zeroLocus {f}))

Tactic:
obtain ⟨t, ht⟩ := exists_image_comap_of_monic f g hg

Premises used: Polynomial.exists_image_comap_of_monic
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
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))ᶜ
rw : IsOpen (X := PrimeSpectrum R) (zeroLocus (↑t : Set R))ᶜ
⊢ IsOpen (X := PrimeSpectrum R) (comap C '' (zeroLocus {g} \ zeroLocus {f}))

Tactic:
rw [ht]
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
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))ᶜ
⊢ IsOpen (X := PrimeSpectrum R) (zeroLocus (↑t : Set R))ᶜ

Tactic:
(isClosed_zeroLocus (R := R) t).isOpen_compl

Premises used: IsClosed.isOpen_compl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
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))ᶜ
⊢ IsOpen (X := PrimeSpectrum R) (zeroLocus (↑t : Set R))ᶜ

Tactic:
exact (isClosed_zeroLocus (R := R) t).isOpen_compl

Premises used: IsClosed.isOpen_compl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
trans :
  x ∈ comap C '' (↑(basicOpen f) : Set (PrimeSpectrum (MvPolynomial σ R))) ↔
    Ne (α := MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      ((map (algebraMap R x.asIdeal.ResidueField) : (a : MvPolynomial σ R) → MvPolynomial σ x.asIdeal.ResidueField) f :
        MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      (0 : MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
trans₁ :
  Ne (α := MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      ((map (algebraMap R x.asIdeal.ResidueField) : (a : MvPolynomial σ R) → MvPolynomial σ x.asIdeal.ResidueField) f :
        MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      (0 : MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField) ↔
    ∃ (i : σ →₀ ℕ), coeff i f ∉ x.asIdeal
⊢ x ∈ comap C '' (↑(basicOpen f) : Set (PrimeSpectrum (MvPolynomial σ R))) ↔ ∃ (i : σ →₀ ℕ), coeff i f ∉ x.asIdeal

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

Premises used: Algebra.algebraMap, Ideal.ResidueField, MvPolynomial.map, DFunLike.coe, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
⊢ x ∈ comap C '' (↑(basicOpen f) : Set (PrimeSpectrum (MvPolynomial σ R))) ↔
    Ne (α := MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      ((map (algebraMap R x.asIdeal.ResidueField) : (a : MvPolynomial σ R) → MvPolynomial σ x.asIdeal.ResidueField) f :
        MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      (0 : MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)

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

Premises used: not_iff_not, Iff.mpr, Set.Mem, PrimeSpectrum.mem_image_comap_basicOpen, Iff.trans, MvPolynomial.C
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
refine :
  IsNilpotent (R := MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)
      ((algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField) :
            (a : MvPolynomial σ R) → MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)
          f :
        MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField) ↔
    Eq (α := MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      ((map (algebraMap R x.asIdeal.ResidueField) : (a : MvPolynomial σ R) → MvPolynomial σ x.asIdeal.ResidueField) f :
        MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      (0 : MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
⊢ x ∈ comap C '' (↑(basicOpen f) : Set (PrimeSpectrum (MvPolynomial σ R))) ↔
    Ne (α := MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      ((map (algebraMap R x.asIdeal.ResidueField) : (a : MvPolynomial σ R) → MvPolynomial σ x.asIdeal.ResidueField) f :
        MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      (0 : MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)

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_2
inst : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField :=
  scalarRTensorAlgEquiv
rw :
  Eq (α := MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      ((e : (a : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField) → MvPolynomial σ x.asIdeal.ResidueField)
          ((algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField) :
              (a : MvPolynomial σ R) → MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)
            f) :
        MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      (0 : MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField) ↔
    Eq (α := MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      ((map (algebraMap R x.asIdeal.ResidueField) : (a : MvPolynomial σ R) → MvPolynomial σ x.asIdeal.ResidueField) f :
        MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      (0 : MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
⊢ IsNilpotent (R := MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)
      ((algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField) :
            (a : MvPolynomial σ R) → MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)
          f :
        MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField) ↔
    Eq (α := MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      ((map (algebraMap R x.asIdeal.ResidueField) : (a : MvPolynomial σ R) → MvPolynomial σ x.asIdeal.ResidueField) f :
        MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      (0 : MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)

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_2
inst : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField :=
  scalarRTensorAlgEquiv
change :
  Eq (α := MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      (((↑e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField →ₐ[R] MvPolynomial σ x.asIdeal.ResidueField).comp
              (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)) :
            (a : MvPolynomial σ R) → MvPolynomial σ x.asIdeal.ResidueField)
          f :
        MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      (0 : MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField) ↔
    Eq (α := MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      ((map (algebraMap R x.asIdeal.ResidueField) : (a : MvPolynomial σ R) → MvPolynomial σ x.asIdeal.ResidueField) f :
        MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      (0 : MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
⊢ Eq (α := MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      ((e : (a : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField) → MvPolynomial σ x.asIdeal.ResidueField)
          ((algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField) :
              (a : MvPolynomial σ R) → MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)
            f) :
        MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      (0 : MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField) ↔
    Eq (α := MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      ((map (algebraMap R x.asIdeal.ResidueField) : (a : MvPolynomial σ R) → MvPolynomial σ x.asIdeal.ResidueField) f :
        MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      (0 : MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)

Tactic:
change (e.toAlgHom.toRingHom).comp (algebraMap _ _) f = 0 ↔ MvPolynomial.map _ f = 0

Premises used: AlgEquiv.toAlgHom, Algebra.algebraMap, RingHom.comp, AlgHom.toRingHom, MvPolynomial.map, DFunLike.coe
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField :=
  scalarRTensorAlgEquiv
a :
  Eq (α := MvPolynomial σ R →+* MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
    ((↑e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField →ₐ[R] MvPolynomial σ x.asIdeal.ResidueField).comp
      (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)))
    (map (algebraMap R x.asIdeal.ResidueField))
⊢ Eq (α := MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      (((↑e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField →ₐ[R] MvPolynomial σ x.asIdeal.ResidueField).comp
              (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)) :
            (a : MvPolynomial σ R) → MvPolynomial σ x.asIdeal.ResidueField)
          f :
        MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      (0 : MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField) ↔
    Eq (α := MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      ((map (algebraMap R x.asIdeal.ResidueField) : (a : MvPolynomial σ R) → MvPolynomial σ x.asIdeal.ResidueField) f :
        MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      (0 : MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)

Tactic:
congr!
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField :=
  scalarRTensorAlgEquiv
a :
  ∀ (x_1 : R) (m : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := x.asIdeal.ResidueField)
      (coeff m
        ((RingHom.comp (β := MvPolynomial σ R)
              ((↑e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField →ₐ[R] MvPolynomial σ x.asIdeal.ResidueField).comp
                (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)))
              C :
            (a : R) → MvPolynomial σ x.asIdeal.ResidueField)
          x_1))
      (coeff m
        ((RingHom.comp (map (algebraMap R x.asIdeal.ResidueField)) C : (a : R) → MvPolynomial σ x.asIdeal.ResidueField)
          x_1))
a₁ :
  ∀ (i : σ) (m : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := x.asIdeal.ResidueField)
      (coeff m
        (((↑e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField →ₐ[R] MvPolynomial σ x.asIdeal.ResidueField).comp
              (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)) :
            (a : MvPolynomial σ R) → MvPolynomial σ x.asIdeal.ResidueField)
          (X i)))
      (coeff m
        ((map (algebraMap R x.asIdeal.ResidueField) : (a : MvPolynomial σ R) → MvPolynomial σ x.asIdeal.ResidueField)
          (X i)))
⊢ Eq (α := MvPolynomial σ R →+* MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
    ((↑e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField →ₐ[R] MvPolynomial σ x.asIdeal.ResidueField).comp
      (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)))
    (map (algebraMap R x.asIdeal.ResidueField))

Tactic:
ext
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField :=
  scalarRTensorAlgEquiv
x_1 : R
m : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := x.asIdeal.ResidueField)
    (coeff m
      ((RingHom.comp (β := MvPolynomial σ R)
            ((↑e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField →ₐ[R] MvPolynomial σ x.asIdeal.ResidueField).comp
              (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)))
            C :
          (a : R) → MvPolynomial σ x.asIdeal.ResidueField)
        x_1))
    (coeff m
      ((RingHom.comp (map (algebraMap R x.asIdeal.ResidueField)) C : (a : R) → MvPolynomial σ x.asIdeal.ResidueField)
        x_1))

Tactic:
simp [scalarRTensorAlgEquiv, e, coeff_map,
        Algebra.smul_def, apply_ite (f := algebraMap _ _)]

Premises used: Algebra.algebraMap, apply_ite, MvPolynomial.coeff_map, MvPolynomial.scalarRTensorAlgEquiv, Algebra.smul_def, DFunLike.coe
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField :=
  scalarRTensorAlgEquiv
i : σ
m : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := x.asIdeal.ResidueField)
    (coeff m
      (((↑e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField →ₐ[R] MvPolynomial σ x.asIdeal.ResidueField).comp
            (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)) :
          (a : MvPolynomial σ R) → MvPolynomial σ x.asIdeal.ResidueField)
        (X i)))
    (coeff m
      ((map (algebraMap R x.asIdeal.ResidueField) : (a : MvPolynomial σ R) → MvPolynomial σ x.asIdeal.ResidueField)
        (X i)))

Tactic:
simp [e, scalarRTensorAlgEquiv, coeff_map, coeff_X']

Premises used: MvPolynomial.coeff_map, MvPolynomial.coeff_X', MvPolynomial.scalarRTensorAlgEquiv
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
⊢ Ne (α := MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      ((map (algebraMap R x.asIdeal.ResidueField) : (a : MvPolynomial σ R) → MvPolynomial σ x.asIdeal.ResidueField) f :
        MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      (0 : MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField) ↔
    ∃ (i : σ →₀ ℕ), coeff i f ∉ x.asIdeal

Tactic:
simp [MvPolynomial.ext_iff, coeff_map]

Premises used: MvPolynomial.ext_iff, MvPolynomial.coeff_map
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
trans :
  x ∈ comap C '' (↑(basicOpen f) : Set (PrimeSpectrum (MvPolynomial σ R))) ↔
    Ne (α := MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      ((map (algebraMap R x.asIdeal.ResidueField) : (a : MvPolynomial σ R) → MvPolynomial σ x.asIdeal.ResidueField) f :
        MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      (0 : MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
trans₁ trans₂ :
  Ne (α := MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      ((map (algebraMap R x.asIdeal.ResidueField) : (a : MvPolynomial σ R) → MvPolynomial σ x.asIdeal.ResidueField) f :
        MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      (0 : MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField) ↔
    ∃ (i : σ →₀ ℕ), coeff i f ∉ x.asIdeal
⊢ x ∈ comap C '' (↑(basicOpen f) : Set (PrimeSpectrum (MvPolynomial σ R))) ↔ ∃ (i : σ →₀ ℕ), coeff i f ∉ x.asIdeal

Tactic:
classical
  trans f.map (algebraMap R x.asIdeal.ResidueField) ≠ 0
  · refine (mem_image_comap_basicOpen _ _).trans (not_iff_not.mpr ?_)
    let e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField ≃ₐ[R]
        MvPolynomial σ x.asIdeal.ResidueField := scalarRTensorAlgEquiv
    rw [← IsNilpotent.map_iff e.injective, isNilpotent_iff_eq_zero]
    change (e.toAlgHom.toRingHom).comp (algebraMap _ _) f = 0 ↔ MvPolynomial.map _ f = 0
    congr!
    ext
    · simp [scalarRTensorAlgEquiv, e, coeff_map,
        Algebra.smul_def, apply_ite (f := algebraMap _ _)]
    · simp [e, scalarRTensorAlgEquiv, coeff_map, coeff_X']
  · simp [MvPolynomial.ext_iff, coeff_map]

Premises used: not_iff_not, Iff.mpr, Algebra.algebraMap, PrimeSpectrum.mem_image_comap_basicOpen, Ideal.ResidueField, MvPolynomial.ext_iff, apply_ite, isNilpotent_iff_eq_zero, MvPolynomial.coeff_map, MvPolynomial.coeff_X', MvPolynomial.scalarRTensorAlgEquiv, Iff.trans, MvPolynomial.map, Algebra.smul_def, DFunLike.coe, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
f : MvPolynomial σ R
h :
  ∀ (p : PrimeSpectrum R),
    p ∈ comap C '' (↑(basicOpen f) : Set (PrimeSpectrum (MvPolynomial σ R))) ↔
      Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (Set.range fun (m : σ →₀ ℕ) ↦ coeff m f))ᶜ p
⊢ comap C '' (↑(basicOpen f) : Set (PrimeSpectrum (MvPolynomial σ R))) =
    (zeroLocus (Set.range fun (m : σ →₀ ℕ) ↦ coeff m f))ᶜ

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

Tactic:
rw [mem_image_comap_C_basicOpen]

Premises used: MvPolynomial.mem_image_comap_C_basicOpen
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
f : MvPolynomial σ R
p : PrimeSpectrum R
⊢ (∃ (i : σ →₀ ℕ), coeff i f ∉ p.asIdeal) ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (Set.range fun (m : σ →₀ ℕ) ↦ coeff m f))ᶜ p

Tactic:
simp [Set.range_subset_iff]

Premises used: Set.range_subset_iff