-- 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
e :
  A ⊗[R] x.asIdeal.ResidueField ≃ₐ[A]
    TensorProduct.{u_1, u_2, u_1} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span ∅)) x.asIdeal.ResidueField
rw :
  Membership.mem (γ := Set (PrimeSpectrum R)) (comap (algebraMap R A) '' (↑(basicOpen f) : Set (PrimeSpectrum A))) x ↔
    ¬IsNilpotent (R :=
        TensorProduct.{u_1, u_2, u_1} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span ∅)) x.asIdeal.ResidueField)
        ((e : (a : A ⊗[R] x.asIdeal.ResidueField) → (A ⧸ Ideal.span ∅) ⊗[R] x.asIdeal.ResidueField)
            ((algebraMap A (A ⊗[R] x.asIdeal.ResidueField) : (a : A) → A ⊗[R] x.asIdeal.ResidueField) f) :
          TensorProduct.{u_1, u_2, u_1} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span ∅)) x.asIdeal.ResidueField)
rw₁ :
  Membership.mem (γ := Set (PrimeSpectrum R)) (comap (algebraMap R A) '' (↑(basicOpen f) : Set (PrimeSpectrum A))) x ↔
    ¬IsNilpotent (R :=
        TensorProduct.{u_1, u_2, u_1} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span ∅)) x.asIdeal.ResidueField)
        ((algebraMap A
                (TensorProduct.{u_1, u_2, u_1} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span ∅))
                  x.asIdeal.ResidueField) :
              (a : A) → (A ⧸ Ideal.span ∅) ⊗[R] x.asIdeal.ResidueField)
            f :
          TensorProduct.{u_1, u_2, u_1} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span ∅)) x.asIdeal.ResidueField)
rw₂ :
  Membership.mem (γ := Set (PrimeSpectrum R)) (comap (algebraMap R A) '' (↑(basicOpen f) : Set (PrimeSpectrum A))) x ↔
    Membership.mem (γ := Set (PrimeSpectrum R))
      (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (zeroLocus ∅ \ zeroLocus {f})) x
rw₃ :
  Membership.mem (γ := Set (PrimeSpectrum R)) (comap (algebraMap R A) '' (↑(basicOpen f) : Set (PrimeSpectrum A))) x ↔
    Membership.mem (γ := Set (PrimeSpectrum R))
      (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (Set.univ \ zeroLocus {f})) x
rw₄ :
  Membership.mem (γ := Set (PrimeSpectrum R)) (comap (algebraMap R A) '' (↑(basicOpen f) : Set (PrimeSpectrum A))) x ↔
    Membership.mem (γ := Set (PrimeSpectrum R))
      (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (zeroLocus {f})ᶜ) x
rw₅ rw₆ :
  Membership.mem (γ := Set (PrimeSpectrum R))
      (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (zeroLocus {f})ᶜ) x ↔
    Membership.mem (γ := Set (PrimeSpectrum R))
      (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (zeroLocus {f})ᶜ) x
⊢ 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:
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]

Premises used: PrimeSpectrum.zeroLocus_empty, AlgEquiv.commutes, IsNilpotent.map_iff, Set.compl_eq_univ_diff, PrimeSpectrum.basicOpen_eq_zeroLocus_compl, AlgEquiv.injective, EmptyCollection.emptyCollection, PrimeSpectrum.mem_image_comap_zeroLocus_sdiff