awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (hypothesis)
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)
⊢ Membership.mem (γ := Set (PrimeSpectrum R))
    (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (zeroLocus s \ zeroLocus {f})) x
have 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
Tactic: simp only [Set.mem_setOf_eq, Algebra.TensorProduct.algebraMap_apply,
      Ideal.Quotient.algebraMap_eq, not_forall] at H
Cleared hypotheses: H
-- 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
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
⊢ Membership.mem (γ := Set (PrimeSpectrum R))
    (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (zeroLocus s \ zeroLocus {f})) x
have 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
Tactic: obtain ⟨q, hq, hfq⟩ := H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (hypothesis)
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
⊢ Membership.mem (γ := Set (PrimeSpectrum R))
    (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (zeroLocus s \ zeroLocus {f})) x
have 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)
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)]
-- 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
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 R))
    (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (zeroLocus s \ zeroLocus {f})) x
have 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
Tactic: refine ⟨comap (algebraMap A _) ⟨q, hq⟩, ⟨by simpa [Set.subset_def], by simpa⟩, ?_⟩
-- 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
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 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
have mpr : comap (S := x.asIdeal.ResidueField) (algebraMap R 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 _ _) ⊥]
-- 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
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 (S := x.asIdeal.ResidueField) (algebraMap R x.asIdeal.ResidueField) ⊥ = x
have mpr : ∀ (a : R),
  Membership.mem (γ := Ideal R) (asIdeal (comap (S := x.asIdeal.ResidueField) (algebraMap R x.asIdeal.ResidueField) ⊥))
      a ↔
    a ∈ x.asIdeal
Tactic: ext a
-- 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
⊢ 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
have f₁ : A ≃ₐ[A] HasQuotient.Quotient A (B := Ideal A) (Ideal.span ∅)
Tactic: refine Algebra.TensorProduct.congr ?f AlgEquiv.refl
-- 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
⊢ A ≃ₐ[A] HasQuotient.Quotient A (B := Ideal A) (Ideal.span ∅)
have f₁ : A ≃ₐ[A] HasQuotient.Quotient A (B := Ideal A) ⊥
Tactic: rw [Ideal.span_empty]
-- 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
⊢ 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 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)
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 _ _ }
-- 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
⊢ 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)) (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)
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_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)
⊢ 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)) (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)
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_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)
⊢ 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)) (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
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_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
⊢ 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)) (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
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_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
⊢ 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)) (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
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]