-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
@[stacks 00FL]
lemma denseRange_comap_iff_minimalPrimes :
    DenseRange (comap f) ↔ ∀ I (h : I ∈ minimalPrimes R), ⟨I, h.1.1⟩ ∈ Set.range (comap f)

Proof state:
case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ (∀ (I : Ideal R) (h : I ∈ minimalPrimes R), { asIdeal := I, isPrime := ⋯ } ∈ Set.range ⇑(comap f)) →
    DenseRange ⇑(comap f)

Tactic:
intro H p

Result:
case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : ∀ (I : Ideal R) (h : I ∈ minimalPrimes R), { asIdeal := I, isPrime := ⋯ } ∈ Set.range ⇑(comap f)
p : PrimeSpectrum R
⊢ p ∈ closure (Set.range ⇑(comap f))

Proof state:
case h.e'_3.h.a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : RingHom.ker f ≤ nilradical R
I : Ideal R
hI : Minimal (fun q => q.IsPrime ∧ ⊥ ≤ q) I
p : Ideal R
⊢ p.IsPrime ∧ RingHom.ker f ≤ p ↔ p.IsPrime ∧ ⊥ ≤ p

Tactic:
exact ⟨fun h ↦ ⟨h.1, bot_le⟩, fun h ↦ ⟨h.1, H.trans (h.1.radical_le_iff.mpr bot_le)⟩⟩

Result:
no goals

Proof state:
case mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : DenseRange ⇑(comap f)
I : Ideal R
hI : I ∈ minimalPrimes R
⊢ { asIdeal := I, isPrime := ⋯ } ∈ Set.range ⇑(comap f)

Tactic:
have : I ∈ (RingHom.ker f).minimalPrimes := by
  rw [denseRange_comap_iff_ker_le_nilRadical] at H
  simp only [minimalPrimes, Ideal.minimalPrimes, Set.mem_setOf] at hI ⊢
  convert hI using 2 with p
  exact ⟨fun h ↦ ⟨h.1, bot_le⟩, fun h ↦ ⟨h.1, H.trans (h.1.radical_le_iff.mpr bot_le)⟩⟩

Result:
case mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : DenseRange ⇑(comap f)
I : Ideal R
hI : I ∈ minimalPrimes R
this : I ∈ (RingHom.ker f).minimalPrimes
⊢ { asIdeal := I, isPrime := ⋯ } ∈ Set.range ⇑(comap f)

Proof state:
case mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : DenseRange ⇑(comap f)
I : Ideal R
hI : I ∈ minimalPrimes R
this : I ∈ (RingHom.ker f).minimalPrimes
⊢ { asIdeal := I, isPrime := ⋯ } ∈ Set.range ⇑(comap f)

Tactic:
obtain ⟨p, hp, _, rfl⟩ := Ideal.exists_comap_eq_of_mem_minimalPrimes f (I := ⊥) I this

Result:
case mp.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : DenseRange ⇑(comap f)
p : Ideal S
hp : p.IsPrime
left✝ : ⊥ ≤ p
hI : Ideal.comap f p ∈ minimalPrimes R
this : Ideal.comap f p ∈ (RingHom.ker f).minimalPrimes
⊢ { asIdeal := Ideal.comap f p, isPrime := ⋯ } ∈ Set.range ⇑(comap f)

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ DenseRange ⇑(comap f) ↔
    ∀ (I : Ideal R) (h : I ∈ minimalPrimes R), { asIdeal := I, isPrime := ⋯ } ∈ Set.range ⇑(comap f)

Tactic:
constructor

Result:
case mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ DenseRange ⇑(comap f) →
    ∀ (I : Ideal R) (h : I ∈ minimalPrimes R), { asIdeal := I, isPrime := ⋯ } ∈ Set.range ⇑(comap f)

case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ (∀ (I : Ideal R) (h : I ∈ minimalPrimes R), { asIdeal := I, isPrime := ⋯ } ∈ Set.range ⇑(comap f)) →
    DenseRange ⇑(comap f)

Proof state:
case mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ DenseRange ⇑(comap f) →
    ∀ (I : Ideal R) (h : I ∈ minimalPrimes R), { asIdeal := I, isPrime := ⋯ } ∈ Set.range ⇑(comap f)

Tactic:
intro H I hI

Result:
case mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : DenseRange ⇑(comap f)
I : Ideal R
hI : I ∈ minimalPrimes R
⊢ { asIdeal := I, isPrime := ⋯ } ∈ Set.range ⇑(comap f)

Proof state:
case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : ∀ (I : Ideal R) (h : I ∈ minimalPrimes R), { asIdeal := I, isPrime := ⋯ } ∈ Set.range ⇑(comap f)
p : PrimeSpectrum R
⊢ p ∈ closure (Set.range ⇑(comap f))

Tactic:
obtain ⟨q, hq, hq'⟩ := Ideal.exists_minimalPrimes_le (J := p.asIdeal) bot_le

Result:
case mpr.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : ∀ (I : Ideal R) (h : I ∈ minimalPrimes R), { asIdeal := I, isPrime := ⋯ } ∈ Set.range ⇑(comap f)
p : PrimeSpectrum R
q : Ideal R
hq : q ∈ ⊥.minimalPrimes
hq' : q ≤ p.asIdeal
⊢ p ∈ closure (Set.range ⇑(comap f))

Proof state:
case mp.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : DenseRange ⇑(comap f)
p : Ideal S
hp : p.IsPrime
left✝ : ⊥ ≤ p
hI : Ideal.comap f p ∈ minimalPrimes R
this : Ideal.comap f p ∈ (RingHom.ker f).minimalPrimes
⊢ { asIdeal := Ideal.comap f p, isPrime := ⋯ } ∈ Set.range ⇑(comap f)

Tactic:
exact ⟨⟨p, hp⟩, rfl⟩

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : DenseRange ⇑(comap f)
I : Ideal R
hI : I ∈ minimalPrimes R
⊢ I ∈ (RingHom.ker f).minimalPrimes

Tactic:
rw [denseRange_comap_iff_ker_le_nilRadical] at H

Result:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : RingHom.ker f ≤ nilradical R
I : Ideal R
hI : I ∈ minimalPrimes R
⊢ I ∈ (RingHom.ker f).minimalPrimes

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : RingHom.ker f ≤ nilradical R
I : Ideal R
hI : I ∈ minimalPrimes R
⊢ I ∈ (RingHom.ker f).minimalPrimes

Tactic:
simp only [minimalPrimes, Ideal.minimalPrimes, Set.mem_setOf] at hI ⊢

Result:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : RingHom.ker f ≤ nilradical R
I : Ideal R
hI : Minimal (fun q => q.IsPrime ∧ ⊥ ≤ q) I
⊢ Minimal (fun q => q.IsPrime ∧ RingHom.ker f ≤ q) I

Proof state:
case mpr.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : ∀ (I : Ideal R) (h : I ∈ minimalPrimes R), { asIdeal := I, isPrime := ⋯ } ∈ Set.range ⇑(comap f)
p : PrimeSpectrum R
q : Ideal R
hq : q ∈ ⊥.minimalPrimes
hq' : q ≤ p.asIdeal
⊢ p ∈ closure (Set.range ⇑(comap f))

Tactic:
exact ((le_iff_specializes ⟨q, hq.1.1⟩ p).mp hq').mem_closed isClosed_closure
  (subset_closure (H q hq))

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : RingHom.ker f ≤ nilradical R
I : Ideal R
hI : Minimal (fun q => q.IsPrime ∧ ⊥ ≤ q) I
⊢ Minimal (fun q => q.IsPrime ∧ RingHom.ker f ≤ q) I

Tactic:
convert hI using 2 with p

Result:
case h.e'_3.h.a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : RingHom.ker f ≤ nilradical R
I : Ideal R
hI : Minimal (fun q => q.IsPrime ∧ ⊥ ≤ q) I
p : Ideal R
⊢ p.IsPrime ∧ RingHom.ker f ≤ p ↔ p.IsPrime ∧ ⊥ ≤ p