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
mp :
  Membership.mem (γ := Set (PrimeSpectrum R))
      (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (zeroLocus s \ zeroLocus {f})) x →
    ¬IsNilpotent (R :=
        TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField)
        ((algebraMap A
                (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
                  x.asIdeal.ResidueField) :
              (a : A) → (A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)
            f :
          TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField)
mpr :
  ¬IsNilpotent (R :=
        TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField)
        ((algebraMap A
                (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
                  x.asIdeal.ResidueField) :
              (a : A) → (A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)
            f :
          TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
            x.asIdeal.ResidueField) →
    Membership.mem (γ := Set (PrimeSpectrum R))
      (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (zeroLocus s \ zeroLocus {f})) x
⊢ Membership.mem (γ := Set (PrimeSpectrum R))
      (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (zeroLocus s \ zeroLocus {f})) x ↔
    ¬IsNilpotent (R :=
        TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField)
        ((algebraMap A
                (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
                  x.asIdeal.ResidueField) :
              (a : A) → (A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)
            f :
          TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField)

Tactic:
constructor
-- 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
q : PrimeSpectrum A
hqg : Membership.mem (γ := Set (PrimeSpectrum A)) (zeroLocus s) q
hqf : q ∉ zeroLocus {f}
H :
  IsNilpotent (R :=
    TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
      (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q))))
    ((algebraMap A
            (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
              (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q)))) :
          (a : A) → (A ⧸ Ideal.span s) ⊗[R] (comap (algebraMap R A) q).asIdeal.ResidueField)
        f :
      TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
        (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q))))
⊢ s ⊆ (↑q.asIdeal : Set A)

Tactic:
simp only [mem_zeroLocus, Set.singleton_subset_iff, SetLike.mem_coe] at hqg hqf

Premises used: Set.singleton_subset_iff, PrimeSpectrum.mem_zeroLocus, SetLike.mem_coe
-- 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
q : PrimeSpectrum A
hqg : Membership.mem (γ := Set (PrimeSpectrum A)) (zeroLocus s) q
hqf : q ∉ zeroLocus {f}
H :
  IsNilpotent (R :=
    TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
      (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q))))
    ((algebraMap A
            (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
              (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q)))) :
          (a : A) → (A ⧸ Ideal.span s) ⊗[R] (comap (algebraMap R A) q).asIdeal.ResidueField)
        f :
      TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
        (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q))))
hqg₁ : s ⊆ (↑q.asIdeal : Set A)
⊢ f ∉ q.asIdeal

Tactic:
simp only [mem_zeroLocus, Set.singleton_subset_iff, SetLike.mem_coe] at hqg hqf

Premises used: Set.singleton_subset_iff, PrimeSpectrum.mem_zeroLocus, SetLike.mem_coe
-- 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
q : PrimeSpectrum A
H :
  IsNilpotent (R :=
    TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
      (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q))))
    ((algebraMap A
            (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
              (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q)))) :
          (a : A) → (A ⧸ Ideal.span s) ⊗[R] (comap (algebraMap R A) q).asIdeal.ResidueField)
        f :
      TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
        (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q))))
hqg : s ⊆ (↑q.asIdeal : Set A)
hqf : f ∉ q.asIdeal
rwa : s ⊆ (↑(RingHom.ker (F := A →+* q.asIdeal.ResidueField) (algebraMap A q.asIdeal.ResidueField)) : Set A)
rwa₁ rwa₂ rwa₃ rwa₄ : s ⊆ (↑q.asIdeal : Set A)
⊢ LE.le (α := Ideal A) (Ideal.span s)
    (RingHom.ker (F := A →+* q.asIdeal.ResidueField) (algebraMap A q.asIdeal.ResidueField))

Tactic:
rwa [Ideal.span_le, Ideal.ker_algebraMap_residueField]

Premises used: Ideal.span_le, Ideal.ker_algebraMap_residueField
-- 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
q : PrimeSpectrum A
H :
  IsNilpotent (R :=
    TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
      (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q))))
    ((algebraMap A
            (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
              (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q)))) :
          (a : A) → (A ⧸ Ideal.span s) ⊗[R] (comap (algebraMap R A) q).asIdeal.ResidueField)
        f :
      TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
        (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q))))
hqg : s ⊆ (↑q.asIdeal : Set A)
hqf : f ∉ q.asIdeal
⊢ LE.le (α := Ideal A) (Ideal.span s)
    (RingHom.ker (F := A →+* q.asIdeal.ResidueField) (algebraMap A q.asIdeal.ResidueField))

Tactic:
have hs : Ideal.span s ≤ RingHom.ker (algebraMap A q.asIdeal.ResidueField) := by
      rwa [Ideal.span_le, Ideal.ker_algebraMap_residueField]
-- 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
q : PrimeSpectrum A
H :
  IsNilpotent (R :=
    TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
      (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q))))
    ((algebraMap A
            (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
              (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q)))) :
          (a : A) → (A ⧸ Ideal.span s) ⊗[R] (comap (algebraMap R A) q).asIdeal.ResidueField)
        f :
      TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
        (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q))))
hqg : s ⊆ (↑q.asIdeal : Set A)
hqf : f ∉ q.asIdeal
hs :
  LE.le (α := Ideal A) (Ideal.span s)
    (RingHom.ker (F := A →+* q.asIdeal.ResidueField) (algebraMap A q.asIdeal.ResidueField))
F : TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
    (Ideal.ResidueField (Ideal.comap (F := R →+* A) (algebraMap R A) q.asIdeal)) →ₐ[A]
  q.asIdeal.ResidueField :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this :
  IsNilpotent.{u_1} (R := q.asIdeal.ResidueField)
    ((F : (a : (A ⧸ Ideal.span s) ⊗[R] (comap (algebraMap R A) q).asIdeal.ResidueField) → q.asIdeal.ResidueField)
        ((algebraMap A
              (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
                (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q)))) :
            (a : A) → (A ⧸ Ideal.span s) ⊗[R] (comap (algebraMap R A) q).asIdeal.ResidueField)
          f) :
      q.asIdeal.ResidueField)
⊢ f ∈ q.asIdeal

Tactic:
rw [AlgHom.commutes, isNilpotent_iff_eq_zero, ← RingHom.mem_ker,
      Ideal.ker_algebraMap_residueField] at this

Premises used: Ideal.ker_algebraMap_residueField, RingHom.mem_ker, isNilpotent_iff_eq_zero, AlgHom.commutes
-- 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
q : PrimeSpectrum A
H :
  IsNilpotent (R :=
    TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
      (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q))))
    ((algebraMap A
            (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
              (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q)))) :
          (a : A) → (A ⧸ Ideal.span s) ⊗[R] (comap (algebraMap R A) q).asIdeal.ResidueField)
        f :
      TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
        (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q))))
hqg : s ⊆ (↑q.asIdeal : Set A)
hqf : f ∉ q.asIdeal
hs :
  LE.le (α := Ideal A) (Ideal.span s)
    (RingHom.ker (F := A →+* q.asIdeal.ResidueField) (algebraMap A q.asIdeal.ResidueField))
F : TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
    (Ideal.ResidueField (Ideal.comap (F := R →+* A) (algebraMap R A) q.asIdeal)) →ₐ[A]
  q.asIdeal.ResidueField :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : f ∈ q.asIdeal
⊢ False

Tactic:
hqf this
-- 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
q : PrimeSpectrum A
H :
  IsNilpotent (R :=
    TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
      (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q))))
    ((algebraMap A
            (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
              (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q)))) :
          (a : A) → (A ⧸ Ideal.span s) ⊗[R] (comap (algebraMap R A) q).asIdeal.ResidueField)
        f :
      TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
        (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q))))
hqg : s ⊆ (↑q.asIdeal : Set A)
hqf : f ∉ q.asIdeal
hs :
  LE.le (α := Ideal A) (Ideal.span s)
    (RingHom.ker (F := A →+* q.asIdeal.ResidueField) (algebraMap A q.asIdeal.ResidueField))
F : TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
    (Ideal.ResidueField (Ideal.comap (F := R →+* A) (algebraMap R A) q.asIdeal)) →ₐ[A]
  q.asIdeal.ResidueField :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : f ∈ q.asIdeal
⊢ False

Tactic:
exact hqf this
-- 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
H :
  ¬IsNilpotent (R :=
      TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField)
      ((algebraMap A
              (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
                x.asIdeal.ResidueField) :
            (a : A) → (A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)
          f :
        TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField)
⊢ ¬∀
      ⦃I :
        Ideal
          (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
            x.asIdeal.ResidueField)⦄,
      Membership.mem (γ :=
          Set
            (Ideal
              (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
                x.asIdeal.ResidueField)))
          {J :
            Ideal
              (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
                x.asIdeal.ResidueField) |
            J.IsPrime}
          I →
        Membership.mem (α :=
          TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField)
          I
          ((algebraMap A
                  (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
                    x.asIdeal.ResidueField) :
                (a : A) → (A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)
              f :
            TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
              x.asIdeal.ResidueField)

Tactic:
rw [← mem_nilradical, nilradical_eq_sInf, Ideal.mem_sInf] at H

Premises used: Ideal.mem_sInf, nilradical_eq_sInf, mem_nilradical
-- 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
H :
  ¬∀
      ⦃I :
        Ideal
          (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
            x.asIdeal.ResidueField)⦄,
      Membership.mem (γ :=
          Set
            (Ideal
              (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
                x.asIdeal.ResidueField)))
          {J :
            Ideal
              (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
                x.asIdeal.ResidueField) |
            J.IsPrime}
          I →
        Membership.mem (α :=
          TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField)
          I
          ((algebraMap A
                  (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
                    x.asIdeal.ResidueField) :
                (a : A) → (A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)
              f :
            TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
              x.asIdeal.ResidueField)
⊢ ∃ (x_1 :
    Ideal
      (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField))
    (_ : x_1.IsPrime),
    ((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) ∉
      x_1

Tactic:
simp only [Set.mem_setOf_eq, Algebra.TensorProduct.algebraMap_apply,
      Ideal.Quotient.algebraMap_eq, not_forall] at H

Premises used: Algebra.TensorProduct.algebraMap_apply, Ideal.Quotient.algebraMap_eq, Set.mem_setOf_eq, Classical.not_forall
-- 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
H :
  ∃ (x_1 :
    Ideal
      (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField))
    (_ : x_1.IsPrime),
    ((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) ∉
      x_1
mpr :
  ∀
    (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),
    Membership.mem (γ := Set (PrimeSpectrum R))
      (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (zeroLocus s \ zeroLocus {f})) x
⊢ Membership.mem (γ := Set (PrimeSpectrum R))
    (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (zeroLocus s \ zeroLocus {f})) x

Tactic:
obtain ⟨q, hq, hfq⟩ := H
-- 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
a : A
ha : 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)

Tactic:
simp [Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.subset_span ha)]

Premises used: Iff.mpr, Ideal.subset_span, Ideal.Quotient.eq_zero_iff_mem
-- 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
⊢ ∀ 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)

Tactic:
have : ∀ a ∈ s, Ideal.Quotient.mk (Ideal.span s) a ⊗ₜ[R] 1 ∈ q := fun a ha ↦ by
      simp [Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.subset_span ha)]
-- 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)
⊢ Membership.mem (γ := Set (PrimeSpectrum A)) (zeroLocus s)
    (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) })

Tactic:
simpa [Set.subset_def]

Premises used: Set.subset_def
-- 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)
⊢ 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) } ∉
    zeroLocus {f}

Tactic:
simpa
-- 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 (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
⊢ Membership.mem (γ := Set (PrimeSpectrum R))
    (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (zeroLocus s \ zeroLocus {f})) x

Tactic:
refine ⟨comap (algebraMap A _) ⟨q, hq⟩, ⟨by simpa [Set.subset_def], by simpa⟩, ?_⟩