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