-- 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))
w : Finset R
h 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))ᶜ
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
h₃ :
  ∀ (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
⊢ ∃ (t : Finset R),
    Eq (α := Set (PrimeSpectrum R))
      (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (zeroLocus s \ zeroLocus {f}))
      (zeroLocus (↑t : Set R))ᶜ

Tactic:
classical
  use (Finset.range (Module.finrank R (A ⧸ Ideal.span s))).image
    (Algebra.lmul R (A ⧸ Ideal.span s) (Ideal.Quotient.mk _ f)).charpoly.coeff
  ext x
  rw [mem_image_comap_zeroLocus_sdiff, IsScalarTower.algebraMap_apply A (A ⧸ Ideal.span s),
    isNilpotent_tensor_residueField_iff]
  simp [Set.subset_def]

Premises used: Set.subset_def, HasQuotient.Quotient, isNilpotent_tensor_residueField_iff, Ideal.span, PrimeSpectrum.mem_image_comap_zeroLocus_sdiff, IsScalarTower.algebraMap_apply