-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
lemma isClosed_range_of_stableUnderSpecialization
    (hf : StableUnderSpecialization (Set.range (comap f))) :
    IsClosed (Set.range (comap f))

Proof state:
case refine_1.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : StableUnderSpecialization (Set.range ⇑(comap f))
q : PrimeSpectrum S
⊢ (comap f) q ∈ zeroLocus ↑(RingHom.ker f)

Tactic:
exact Ideal.comap_mono bot_le

Result:
no goals

Proof state:
case refine_2.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : StableUnderSpecialization (Set.range ⇑(comap f))
p : PrimeSpectrum R
hp : p ∈ zeroLocus ↑(RingHom.ker f)
q : Ideal R
hq : q ∈ (RingHom.ker f).minimalPrimes
hqle : q ≤ p.asIdeal
⊢ p ∈ Set.range ⇑(comap f)

Tactic:
obtain ⟨q', hq', hq'c⟩ := Ideal.exists_minimalPrimes_comap_eq f q hq

Result:
case refine_2.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : StableUnderSpecialization (Set.range ⇑(comap f))
p : PrimeSpectrum R
hp : p ∈ zeroLocus ↑(RingHom.ker f)
q : Ideal R
hq : q ∈ (RingHom.ker f).minimalPrimes
hqle : q ≤ p.asIdeal
q' : Ideal S
hq' : q' ∈ ⊥.minimalPrimes
hq'c : Ideal.comap f q' = q
⊢ p ∈ Set.range ⇑(comap f)

Proof state:
case refine_2.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : StableUnderSpecialization (Set.range ⇑(comap f))
p : PrimeSpectrum R
hp : p ∈ zeroLocus ↑(RingHom.ker f)
q : Ideal R
hq : q ∈ (RingHom.ker f).minimalPrimes
hqle : q ≤ p.asIdeal
q' : Ideal S
hq' : q' ∈ ⊥.minimalPrimes
hq'c : Ideal.comap f q' = q
⊢ p ∈ Set.range ⇑(comap f)

Tactic:
exact hf ((le_iff_specializes ⟨q, hq.1.1⟩ p).mp hqle) ⟨⟨q', hq'.1.1⟩, PrimeSpectrum.ext hq'c⟩

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : StableUnderSpecialization (Set.range ⇑(comap f))
⊢ IsClosed (Set.range ⇑(comap f))

Tactic:
refine (isClosed_iff_zeroLocus _).mpr ⟨RingHom.ker f, le_antisymm ?_ ?_⟩

Result:
case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : StableUnderSpecialization (Set.range ⇑(comap f))
⊢ Set.range ⇑(comap f) ≤ zeroLocus ↑(RingHom.ker f)

case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : StableUnderSpecialization (Set.range ⇑(comap f))
⊢ zeroLocus ↑(RingHom.ker f) ≤ Set.range ⇑(comap f)

Proof state:
case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : StableUnderSpecialization (Set.range ⇑(comap f))
⊢ zeroLocus ↑(RingHom.ker f) ≤ Set.range ⇑(comap f)

Tactic:
intro p hp

Result:
case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : StableUnderSpecialization (Set.range ⇑(comap f))
p : PrimeSpectrum R
hp : p ∈ zeroLocus ↑(RingHom.ker f)
⊢ p ∈ Set.range ⇑(comap f)

Proof state:
case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : StableUnderSpecialization (Set.range ⇑(comap f))
p : PrimeSpectrum R
hp : p ∈ zeroLocus ↑(RingHom.ker f)
⊢ p ∈ Set.range ⇑(comap f)

Tactic:
obtain ⟨q, hq, hqle⟩ := Ideal.exists_minimalPrimes_le hp

Result:
case refine_2.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : StableUnderSpecialization (Set.range ⇑(comap f))
p : PrimeSpectrum R
hp : p ∈ zeroLocus ↑(RingHom.ker f)
q : Ideal R
hq : q ∈ (RingHom.ker f).minimalPrimes
hqle : q ≤ p.asIdeal
⊢ p ∈ Set.range ⇑(comap f)

Proof state:
case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : StableUnderSpecialization (Set.range ⇑(comap f))
⊢ Set.range ⇑(comap f) ≤ zeroLocus ↑(RingHom.ker f)

Tactic:
rintro _ ⟨q, rfl⟩

Result:
case refine_1.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : StableUnderSpecialization (Set.range ⇑(comap f))
q : PrimeSpectrum S
⊢ (comap f) q ∈ zeroLocus ↑(RingHom.ker f)