-- Mathlib/RingTheory/Spectrum/Prime/Polynomial.lean
/-- Let `A` be an `R`-algebra. If `A ⧸ I` is finite free over `R`,
then the image of `Z(I) ∩ D(f) ⊆ Spec S` in `Spec R` is compact open. -/
lemma exists_image_comap_of_finite_of_free (f : A) (s : Set A)
    [Module.Finite R (A ⧸ Ideal.span s)] [Module.Free R (A ⧸ Ideal.span s)] :
    ∃ t : Finset R, comap (algebraMap R A) '' (zeroLocus s \ zeroLocus {f}) = (zeroLocus t)ᶜ

Proof state:
case h
R : Type u_2
A : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
f : A
s : Set A
inst✝¹ : Module.Finite R (A ⧸ Ideal.span s)
inst✝ : Module.Free R (A ⧸ Ideal.span s)
⊢ ⇑(comap (algebraMap R A)) '' (zeroLocus s \ zeroLocus {f}) =
    (zeroLocus
        ↑(Finset.image
            (LinearMap.charpoly ((Algebra.lmul R (A ⧸ Ideal.span s)) ((Ideal.Quotient.mk (Ideal.span s)) f))).coeff
            (Finset.range (Module.finrank R (A ⧸ Ideal.span s)))))ᶜ

Tactic:
ext x

Result:
case h.h
R : Type u_2
A : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
f : A
s : Set A
inst✝¹ : Module.Finite R (A ⧸ Ideal.span s)
inst✝ : Module.Free R (A ⧸ Ideal.span s)
x : PrimeSpectrum R
⊢ x ∈ ⇑(comap (algebraMap R A)) '' (zeroLocus s \ zeroLocus {f}) ↔
    x ∈
      (zeroLocus
          ↑(Finset.image
              (LinearMap.charpoly ((Algebra.lmul R (A ⧸ Ideal.span s)) ((Ideal.Quotient.mk (Ideal.span s)) f))).coeff
              (Finset.range (Module.finrank R (A ⧸ Ideal.span s)))))ᶜ

Proof state:
R : Type u_2
A : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
f : A
s : Set A
inst✝¹ : Module.Finite R (A ⧸ Ideal.span s)
inst✝ : Module.Free R (A ⧸ Ideal.span s)
⊢ ∃ t, ⇑(comap (algebraMap R A)) '' (zeroLocus s \ zeroLocus {f}) = (zeroLocus ↑t)ᶜ

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]

Result:
no goals

Proof state:
case h.h
R : Type u_2
A : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
f : A
s : Set A
inst✝¹ : Module.Finite R (A ⧸ Ideal.span s)
inst✝ : Module.Free R (A ⧸ Ideal.span s)
x : PrimeSpectrum R
⊢ (¬∀ i < Module.finrank R (A ⧸ Ideal.span s),
        (LinearMap.charpoly ((Algebra.lmul R (A ⧸ Ideal.span s)) ((algebraMap A (A ⧸ Ideal.span s)) f))).coeff i ∈
          x.asIdeal) ↔
    x ∈
      (zeroLocus
          ↑(Finset.image
              (LinearMap.charpoly ((Algebra.lmul R (A ⧸ Ideal.span s)) ((Ideal.Quotient.mk (Ideal.span s)) f))).coeff
              (Finset.range (Module.finrank R (A ⧸ Ideal.span s)))))ᶜ

Tactic:
simp [Set.subset_def]

Result:
no goals

Proof state:
case h.h
R : Type u_2
A : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
f : A
s : Set A
inst✝¹ : Module.Finite R (A ⧸ Ideal.span s)
inst✝ : Module.Free R (A ⧸ Ideal.span s)
x : PrimeSpectrum R
⊢ x ∈ ⇑(comap (algebraMap R A)) '' (zeroLocus s \ zeroLocus {f}) ↔
    x ∈
      (zeroLocus
          ↑(Finset.image
              (LinearMap.charpoly ((Algebra.lmul R (A ⧸ Ideal.span s)) ((Ideal.Quotient.mk (Ideal.span s)) f))).coeff
              (Finset.range (Module.finrank R (A ⧸ Ideal.span s)))))ᶜ

Tactic:
rw [mem_image_comap_zeroLocus_sdiff, IsScalarTower.algebraMap_apply A (A ⧸ Ideal.span s),
  isNilpotent_tensor_residueField_iff]

Result:
case h.h
R : Type u_2
A : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
f : A
s : Set A
inst✝¹ : Module.Finite R (A ⧸ Ideal.span s)
inst✝ : Module.Free R (A ⧸ Ideal.span s)
x : PrimeSpectrum R
⊢ (¬∀ i < Module.finrank R (A ⧸ Ideal.span s),
        (LinearMap.charpoly ((Algebra.lmul R (A ⧸ Ideal.span s)) ((algebraMap A (A ⧸ Ideal.span s)) f))).coeff i ∈
          x.asIdeal) ↔
    x ∈
      (zeroLocus
          ↑(Finset.image
              (LinearMap.charpoly ((Algebra.lmul R (A ⧸ Ideal.span s)) ((Ideal.Quotient.mk (Ideal.span s)) f))).coeff
              (Finset.range (Module.finrank R (A ⧸ Ideal.span s)))))ᶜ

Proof state:
R : Type u_2
A : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
f : A
s : Set A
inst✝¹ : Module.Finite R (A ⧸ Ideal.span s)
inst✝ : Module.Free R (A ⧸ Ideal.span s)
⊢ ∃ t, ⇑(comap (algebraMap R A)) '' (zeroLocus s \ zeroLocus {f}) = (zeroLocus ↑t)ᶜ

Tactic:
use (Finset.range (Module.finrank R (A ⧸ Ideal.span s))).image
  (Algebra.lmul R (A ⧸ Ideal.span s) (Ideal.Quotient.mk _ f)).charpoly.coeff

Result:
case h
R : Type u_2
A : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
f : A
s : Set A
inst✝¹ : Module.Finite R (A ⧸ Ideal.span s)
inst✝ : Module.Free R (A ⧸ Ideal.span s)
⊢ ⇑(comap (algebraMap R A)) '' (zeroLocus s \ zeroLocus {f}) =
    (zeroLocus
        ↑(Finset.image
            (LinearMap.charpoly ((Algebra.lmul R (A ⧸ Ideal.span s)) ((Ideal.Quotient.mk (Ideal.span s)) f))).coeff
            (Finset.range (Module.finrank R (A ⧸ Ideal.span s)))))ᶜ