-- Mathlib/RingTheory/Spectrum/Prime/Polynomial.lean
/-- Let `A` be an `R`-algebra.
`𝔭 : Spec R` is in the image of `Z(I) ∩ D(f) ⊆ Spec S`
if and only if `f` is not nilpotent on `κ(𝔭) ⊗ A ⧸ I`. -/
lemma mem_image_comap_zeroLocus_sdiff (f : A) (s : Set A) (x) :
    x ∈ comap (algebraMap R A) '' (zeroLocus s \ zeroLocus {f}) ↔
      ¬ IsNilpotent (algebraMap A ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField) f)

Proof state:
case mp
R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
x : PrimeSpectrum R
⊢ x ∈ ⇑(comap (algebraMap R A)) '' (zeroLocus s \ zeroLocus {f}) →
    ¬IsNilpotent ((algebraMap A ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)) f)

Tactic:
rintro ⟨q, ⟨hqg, hqf⟩, rfl⟩ H

Result:
case mp.intro.intro.intro
R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
q : PrimeSpectrum A
hqg : q ∈ zeroLocus s
hqf : q ∉ zeroLocus {f}
H : IsNilpotent ((algebraMap A ((A ⧸ Ideal.span s) ⊗[R] ((comap (algebraMap R A)) q).asIdeal.ResidueField)) f)
⊢ False

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
q : PrimeSpectrum A
H : IsNilpotent ((algebraMap A ((A ⧸ Ideal.span s) ⊗[R] ((comap (algebraMap R A)) q).asIdeal.ResidueField)) f)
hqg : s ⊆ ↑q.asIdeal
hqf : f ∉ q.asIdeal
⊢ Ideal.span s ≤ RingHom.ker (algebraMap A q.asIdeal.ResidueField)

Tactic:
rwa [Ideal.span_le, Ideal.ker_algebraMap_residueField]

Result:
no goals

Proof state:
case mp.intro.intro.intro
R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
q : PrimeSpectrum A
hqg : q ∈ zeroLocus s
hqf : q ∉ zeroLocus {f}
H : IsNilpotent ((algebraMap A ((A ⧸ Ideal.span s) ⊗[R] ((comap (algebraMap R A)) q).asIdeal.ResidueField)) f)
⊢ False

Tactic:
simp only [mem_zeroLocus, Set.singleton_subset_iff, SetLike.mem_coe] at hqg hqf

Result:
case mp.intro.intro.intro
R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
q : PrimeSpectrum A
H : IsNilpotent ((algebraMap A ((A ⧸ Ideal.span s) ⊗[R] ((comap (algebraMap R A)) q).asIdeal.ResidueField)) f)
hqg : s ⊆ ↑q.asIdeal
hqf : f ∉ q.asIdeal
⊢ False

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
x : PrimeSpectrum R
q : Ideal ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)
hq : q.IsPrime
hfq : (Ideal.Quotient.mk (Ideal.span s)) f ⊗ₜ[R] 1 ∉ q
a : A
ha : a ∈ s
⊢ (Ideal.Quotient.mk (Ideal.span s)) a ⊗ₜ[R] 1 ∈ q

Tactic:
simp [Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.subset_span ha)]

Result:
no goals

Proof state:
case mpr.intro.intro.asIdeal.h
R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
x : PrimeSpectrum R
q : Ideal ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)
hq : q.IsPrime
hfq : (Ideal.Quotient.mk (Ideal.span s)) f ⊗ₜ[R] 1 ∉ q
this : ∀ a ∈ s, (Ideal.Quotient.mk (Ideal.span s)) a ⊗ₜ[R] 1 ∈ q
a : R
⊢ a ∈ ((comap (algebraMap R x.asIdeal.ResidueField)) ⊥).asIdeal ↔ a ∈ x.asIdeal

Tactic:
exact congr(a ∈ $(Ideal.ker_algebraMap_residueField _))

Result:
no goals

Proof state:
case mp.intro.intro.intro
R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
q : PrimeSpectrum A
H : IsNilpotent ((algebraMap A ((A ⧸ Ideal.span s) ⊗[R] ((comap (algebraMap R A)) q).asIdeal.ResidueField)) f)
hqg : s ⊆ ↑q.asIdeal
hqf : f ∉ q.asIdeal
hs : Ideal.span s ≤ RingHom.ker (algebraMap A q.asIdeal.ResidueField)
F : (A ⧸ Ideal.span s) ⊗[R] (Ideal.comap (algebraMap R A) q.asIdeal).ResidueField →ₐ[A] q.asIdeal.ResidueField :=
  Algebra.TensorProduct.lift (Ideal.Quotient.liftₐ (Ideal.span s) (Algebra.ofId A q.asIdeal.ResidueField) hs)
    (Ideal.ResidueField.mapₐ (Ideal.comap (algebraMap R A) q.asIdeal) q.asIdeal ⋯) ⋯
this : f ∈ q.asIdeal
⊢ False

Tactic:
exact hqf this

Result:
no goals

Proof state:
case mpr
R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
x : PrimeSpectrum R
H :
  ¬∀ ⦃I : Ideal ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)⦄,
      I ∈ {J | J.IsPrime} → (algebraMap A ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)) f ∈ I
⊢ x ∈ ⇑(comap (algebraMap R A)) '' (zeroLocus s \ zeroLocus {f})

Tactic:
simp only [Set.mem_setOf_eq, Algebra.TensorProduct.algebraMap_apply,
  Ideal.Quotient.algebraMap_eq, not_forall, Classical.not_imp] at H

Result:
case mpr
R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
x : PrimeSpectrum R
H : ∃ x_1, ∃ (_ : x_1.IsPrime), (Ideal.Quotient.mk (Ideal.span s)) f ⊗ₜ[R] 1 ∉ x_1
⊢ x ∈ ⇑(comap (algebraMap R A)) '' (zeroLocus s \ zeroLocus {f})

Proof state:
case mpr.intro.intro
R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
x : PrimeSpectrum R
q : Ideal ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)
hq : q.IsPrime
hfq : (Ideal.Quotient.mk (Ideal.span s)) f ⊗ₜ[R] 1 ∉ q
this : ∀ a ∈ s, (Ideal.Quotient.mk (Ideal.span s)) a ⊗ₜ[R] 1 ∈ q
⊢ (comap (algebraMap R x.asIdeal.ResidueField)) ⊥ = x

Tactic:
ext a

Result:
case mpr.intro.intro.asIdeal.h
R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
x : PrimeSpectrum R
q : Ideal ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)
hq : q.IsPrime
hfq : (Ideal.Quotient.mk (Ideal.span s)) f ⊗ₜ[R] 1 ∉ q
this : ∀ a ∈ s, (Ideal.Quotient.mk (Ideal.span s)) a ⊗ₜ[R] 1 ∈ q
a : R
⊢ a ∈ ((comap (algebraMap R x.asIdeal.ResidueField)) ⊥).asIdeal ↔ a ∈ x.asIdeal

Proof state:
case mp.intro.intro.intro
R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
q : PrimeSpectrum A
H : IsNilpotent ((algebraMap A ((A ⧸ Ideal.span s) ⊗[R] ((comap (algebraMap R A)) q).asIdeal.ResidueField)) f)
hqg : s ⊆ ↑q.asIdeal
hqf : f ∉ q.asIdeal
hs : Ideal.span s ≤ RingHom.ker (algebraMap A q.asIdeal.ResidueField)
F : (A ⧸ Ideal.span s) ⊗[R] (Ideal.comap (algebraMap R A) q.asIdeal).ResidueField →ₐ[A] q.asIdeal.ResidueField :=
  Algebra.TensorProduct.lift (Ideal.Quotient.liftₐ (Ideal.span s) (Algebra.ofId A q.asIdeal.ResidueField) hs)
    (Ideal.ResidueField.mapₐ (Ideal.comap (algebraMap R A) q.asIdeal) q.asIdeal ⋯) ⋯
this : IsNilpotent (F ((algebraMap A ((A ⧸ Ideal.span s) ⊗[R] ((comap (algebraMap R A)) q).asIdeal.ResidueField)) f))
⊢ False

Tactic:
rw [AlgHom.commutes, isNilpotent_iff_eq_zero, ← RingHom.mem_ker,
  Ideal.ker_algebraMap_residueField] at this

Result:
case mp.intro.intro.intro
R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
q : PrimeSpectrum A
H : IsNilpotent ((algebraMap A ((A ⧸ Ideal.span s) ⊗[R] ((comap (algebraMap R A)) q).asIdeal.ResidueField)) f)
hqg : s ⊆ ↑q.asIdeal
hqf : f ∉ q.asIdeal
hs : Ideal.span s ≤ RingHom.ker (algebraMap A q.asIdeal.ResidueField)
F : (A ⧸ Ideal.span s) ⊗[R] (Ideal.comap (algebraMap R A) q.asIdeal).ResidueField →ₐ[A] q.asIdeal.ResidueField :=
  Algebra.TensorProduct.lift (Ideal.Quotient.liftₐ (Ideal.span s) (Algebra.ofId A q.asIdeal.ResidueField) hs)
    (Ideal.ResidueField.mapₐ (Ideal.comap (algebraMap R A) q.asIdeal) q.asIdeal ⋯) ⋯
this : f ∈ q.asIdeal
⊢ False