-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
lemma closure_image_comap_zeroLocus (I : Ideal S) :
    closure (comap f '' zeroLocus I) = zeroLocus (I.comap f)

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
x : PrimeSpectrum R
hx : Ideal.comap f I ≤ x.asIdeal
p' : Ideal S
hp' : p'.IsPrime
hp'' : I ≤ p'
hq₁ : Ideal.comap f p' ∈ (Ideal.comap f I).minimalPrimes
hq₂ : Ideal.comap f p' ≤ x.asIdeal
p'' : PrimeSpectrum S := { asIdeal := p', isPrime := hp' }
⊢ (comap f) { asIdeal := p', isPrime := hp' } ∈ ⇑(comap f) '' zeroLocus ↑I

Tactic:
exact ⟨_, hp'', rfl⟩

Result:
no goals

Proof state:
case a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
⊢ zeroLocus ↑(Ideal.comap f I) ⊆ closure (⇑(comap f) '' zeroLocus ↑I)

Tactic:
rintro x (hx : I.comap f ≤ x.asIdeal)

Result:
case a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
x : PrimeSpectrum R
hx : Ideal.comap f I ≤ x.asIdeal
⊢ x ∈ closure (⇑(comap f) '' zeroLocus ↑I)

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
⊢ closure (⇑(comap f) '' zeroLocus ↑I) = zeroLocus ↑(Ideal.comap f I)

Tactic:
apply subset_antisymm

Result:
case a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
⊢ closure (⇑(comap f) '' zeroLocus ↑I) ⊆ zeroLocus ↑(Ideal.comap f I)

case a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
⊢ zeroLocus ↑(Ideal.comap f I) ⊆ closure (⇑(comap f) '' zeroLocus ↑I)

Proof state:
case a.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
x : PrimeSpectrum R
hx : Ideal.comap f I ≤ x.asIdeal
q : Ideal R
hq₁ : q ∈ (Ideal.comap f I).minimalPrimes
hq₂ : q ≤ x.asIdeal
⊢ x ∈ closure (⇑(comap f) '' zeroLocus ↑I)

Tactic:
obtain ⟨p', hp', hp'', rfl⟩ := Ideal.exists_comap_eq_of_mem_minimalPrimes f _ hq₁

Result:
case a.intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
x : PrimeSpectrum R
hx : Ideal.comap f I ≤ x.asIdeal
p' : Ideal S
hp' : p'.IsPrime
hp'' : I ≤ p'
hq₁ : Ideal.comap f p' ∈ (Ideal.comap f I).minimalPrimes
hq₂ : Ideal.comap f p' ≤ x.asIdeal
⊢ x ∈ closure (⇑(comap f) '' zeroLocus ↑I)

Proof state:
case a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
⊢ zeroLocus ↑I ⊆ zeroLocus (⇑f '' ↑(Ideal.comap f I))

Tactic:
exact zeroLocus_anti_mono (Set.image_preimage_subset _ _)

Result:
no goals

Proof state:
case a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
⊢ closure (⇑(comap f) '' zeroLocus ↑I) ⊆ zeroLocus ↑(Ideal.comap f I)

Tactic:
rw [(isClosed_zeroLocus _).closure_subset_iff, Set.image_subset_iff, preimage_comap_zeroLocus]

Result:
case a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
⊢ zeroLocus ↑I ⊆ zeroLocus (⇑f '' ↑(Ideal.comap f I))

Proof state:
case a.intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
x : PrimeSpectrum R
hx : Ideal.comap f I ≤ x.asIdeal
p' : Ideal S
hp' : p'.IsPrime
hp'' : I ≤ p'
hq₁ : Ideal.comap f p' ∈ (Ideal.comap f I).minimalPrimes
hq₂ : Ideal.comap f p' ≤ x.asIdeal
p'' : PrimeSpectrum S := { asIdeal := p', isPrime := hp' }
⊢ x ∈ closure (⇑(comap f) '' zeroLocus ↑I)

Tactic:
apply isClosed_closure.stableUnderSpecialization ((le_iff_specializes
  (comap f ⟨p', hp'⟩) x).mp hq₂) (subset_closure (by exact ⟨_, hp'', rfl⟩))

Result:
no goals

Proof state:
case a.intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
x : PrimeSpectrum R
hx : Ideal.comap f I ≤ x.asIdeal
p' : Ideal S
hp' : p'.IsPrime
hp'' : I ≤ p'
hq₁ : Ideal.comap f p' ∈ (Ideal.comap f I).minimalPrimes
hq₂ : Ideal.comap f p' ≤ x.asIdeal
⊢ x ∈ closure (⇑(comap f) '' zeroLocus ↑I)

Tactic:
let p'' : PrimeSpectrum S := ⟨p', hp'⟩

Result:
case a.intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
x : PrimeSpectrum R
hx : Ideal.comap f I ≤ x.asIdeal
p' : Ideal S
hp' : p'.IsPrime
hp'' : I ≤ p'
hq₁ : Ideal.comap f p' ∈ (Ideal.comap f I).minimalPrimes
hq₂ : Ideal.comap f p' ≤ x.asIdeal
p'' : PrimeSpectrum S := { asIdeal := p', isPrime := hp' }
⊢ x ∈ closure (⇑(comap f) '' zeroLocus ↑I)

Proof state:
case a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
x : PrimeSpectrum R
hx : Ideal.comap f I ≤ x.asIdeal
⊢ x ∈ closure (⇑(comap f) '' zeroLocus ↑I)

Tactic:
obtain ⟨q, hq₁, hq₂⟩ := Ideal.exists_minimalPrimes_le hx

Result:
case a.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
x : PrimeSpectrum R
hx : Ideal.comap f I ≤ x.asIdeal
q : Ideal R
hq₁ : q ∈ (Ideal.comap f I).minimalPrimes
hq₂ : q ≤ x.asIdeal
⊢ x ∈ closure (⇑(comap f) '' zeroLocus ↑I)