awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
I : Ideal S
hZ : IsClosed (X := PrimeSpectrum S) (zeroLocus (↑I : Set S))
hf : StableUnderSpecialization (comap f '' zeroLocus (↑I : Set S))
q : PrimeSpectrum S
hq : Membership.mem (γ := Set (PrimeSpectrum S)) (zeroLocus (↑I : Set S)) q
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑(Ideal.comap f I) : Set R)) (comap f q)

Tactic:
Ideal.comap_mono hq

Premises used: PrimeSpectrum.zeroLocus, Set.Mem, setOf, Ideal.comap_mono, Set.Subset
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
I : Ideal S
hZ : IsClosed (X := PrimeSpectrum S) (zeroLocus (↑I : Set S))
hf : StableUnderSpecialization (comap f '' zeroLocus (↑I : Set S))
q : PrimeSpectrum S
hq : Membership.mem (γ := Set (PrimeSpectrum S)) (zeroLocus (↑I : Set S)) q
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑(Ideal.comap f I) : Set R)) (comap f q)

Tactic:
exact Ideal.comap_mono hq

Premises used: Ideal.comap_mono
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
I : Ideal S
hZ : IsClosed (X := PrimeSpectrum S) (zeroLocus (↑I : Set S))
hf : StableUnderSpecialization (comap f '' zeroLocus (↑I : Set S))
p : PrimeSpectrum R
hp : Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑(Ideal.comap f I) : Set R)) p
refine_2 :
  ∀ (q : Ideal S) (hqI : q ≥ I) (hq : q.IsPrime) (hqle : Ideal.comap f q ≤ p.asIdeal),
    p ∈ comap f '' zeroLocus (↑I : Set S)
⊢ p ∈ comap f '' zeroLocus (↑I : Set S)

Tactic:
obtain ⟨q, hqI, hq, hqle⟩ := p.asIdeal.exists_ideal_comap_le_prime I hp

Premises used: Ideal.exists_ideal_comap_le_prime, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
I : Ideal S
hZ : IsClosed (X := PrimeSpectrum S) (zeroLocus (↑I : Set S))
hf : StableUnderSpecialization (comap f '' zeroLocus (↑I : Set S))
p : PrimeSpectrum R
hp : Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑(Ideal.comap f I) : Set R)) p
q : Ideal S
hqI : q ≥ I
hq : q.IsPrime
hqle : Ideal.comap f q ≤ p.asIdeal
⊢ p ∈ comap f '' zeroLocus (↑I : Set S)

Tactic:
hf ((le_iff_specializes ⟨q.comap f, inferInstance⟩ p).mp hqle) ⟨⟨q, hq⟩, hqI, rfl⟩

Premises used: PrimeSpectrum.mk, inferInstance, PrimeSpectrum.le_iff_specializes, And.intro, Ideal.comap, Exists.intro, Iff.mp, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
I : Ideal S
hZ : IsClosed (X := PrimeSpectrum S) (zeroLocus (↑I : Set S))
hf : StableUnderSpecialization (comap f '' zeroLocus (↑I : Set S))
p : PrimeSpectrum R
hp : Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑(Ideal.comap f I) : Set R)) p
q : Ideal S
hqI : q ≥ I
hq : q.IsPrime
hqle : Ideal.comap f q ≤ p.asIdeal
⊢ p ∈ comap f '' zeroLocus (↑I : Set S)

Tactic:
exact hf ((le_iff_specializes ⟨q.comap f, inferInstance⟩ p).mp hqle) ⟨⟨q, hq⟩, hqI, rfl⟩

Premises used: PrimeSpectrum.mk, inferInstance, PrimeSpectrum.le_iff_specializes, And.intro, Ideal.comap, Exists.intro, Iff.mp, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
hf : StableUnderSpecialization (Set.range (comap f))
rw : ∀ (hf : StableUnderSpecialization (comap f '' Set.univ)), IsClosed (comap f '' Set.univ)
⊢ IsClosed (Set.range (comap f))

Tactic:
rw [← Set.image_univ] at hf ⊢

Premises used: Set.image_univ
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
hf : StableUnderSpecialization (comap f '' Set.univ)
⊢ IsClosed (comap f '' Set.univ)

Tactic:
isClosed_image_of_stableUnderSpecialization _ _ isClosed_univ hf

Premises used: isClosed_univ, PrimeSpectrum.isClosed_image_of_stableUnderSpecialization
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
hf : StableUnderSpecialization (comap f '' Set.univ)
⊢ IsClosed (comap f '' Set.univ)

Tactic:
exact isClosed_image_of_stableUnderSpecialization _ _ isClosed_univ hf

Premises used: isClosed_univ, PrimeSpectrum.isClosed_image_of_stableUnderSpecialization
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
⊢ StableUnderSpecialization (Set.range (comap f)) ↔ IsClosed (Set.range (comap f))

Tactic:
⟨isClosed_range_of_stableUnderSpecialization f, fun h ↦ h.stableUnderSpecialization⟩

Premises used: PrimeSpectrum.isClosed_range_of_stableUnderSpecialization, IsClosed.stableUnderSpecialization, Iff.intro
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
Z : Set (PrimeSpectrum S)
hZ : IsClosed Z
⊢ StableUnderSpecialization (comap f '' Z) ↔ IsClosed (comap f '' Z)

Tactic:
⟨isClosed_image_of_stableUnderSpecialization f Z hZ, fun h ↦ h.stableUnderSpecialization⟩

Premises used: IsClosed.stableUnderSpecialization, Iff.intro, PrimeSpectrum.isClosed_image_of_stableUnderSpecialization
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
h₁ : Function.Surjective (comap f)
h₂ : SpecializingMap (comap f)
rw : Function.Surjective (comap f) ∧ ∀ (s : Set (PrimeSpectrum R)), IsClosed s ↔ IsClosed (comap f ⁻¹' s)
⊢ IsQuotientMap (comap f)

Tactic:
rw [Topology.isQuotientMap_iff_isClosed]

Premises used: Topology.isQuotientMap_iff_isClosed
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
h₁ : Function.Surjective (comap f)
h₂ : SpecializingMap (comap f)
⊢ Function.Surjective (comap f) ∧ ∀ (s : Set (PrimeSpectrum R)), IsClosed s ↔ IsClosed (comap f ⁻¹' s)

Tactic:
⟨h₁, fun s ↦ ⟨fun hs ↦ hs.preimage (continuous_comap f),
    fun hsc ↦ Set.image_preimage_eq s h₁ ▸ isClosed_image_of_stableUnderSpecialization _ _ hsc
      (h₂.stableUnderSpecialization_image hsc.stableUnderSpecialization)⟩⟩

Premises used: Eq.rec, PrimeSpectrum.continuous_comap, Set.image_preimage_eq, IsClosed.stableUnderSpecialization, Set.preimage, And.intro, Iff.intro, IsClosed.preimage, PrimeSpectrum.comap, PrimeSpectrum.isClosed_image_of_stableUnderSpecialization, SpecializingMap.stableUnderSpecialization_image
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
h₁ : Function.Surjective (comap f)
h₂ : SpecializingMap (comap f)
⊢ Function.Surjective (comap f) ∧ ∀ (s : Set (PrimeSpectrum R)), IsClosed s ↔ IsClosed (comap f ⁻¹' s)

Tactic:
exact ⟨h₁, fun s ↦ ⟨fun hs ↦ hs.preimage (continuous_comap f),
    fun hsc ↦ Set.image_preimage_eq s h₁ ▸ isClosed_image_of_stableUnderSpecialization _ _ hsc
      (h₂.stableUnderSpecialization_image hsc.stableUnderSpecialization)⟩⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
h₁ : Function.Surjective (comap f)
h₂ : GeneralizingMap (comap f)
rw : Function.Surjective (comap f) ∧ ∀ (s : Set (PrimeSpectrum R)), IsClosed s ↔ IsClosed (comap f ⁻¹' s)
⊢ IsQuotientMap (comap f)

Tactic:
rw [Topology.isQuotientMap_iff_isClosed]

Premises used: Topology.isQuotientMap_iff_isClosed
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
h₁ : Function.Surjective (comap f)
h₂ : GeneralizingMap (comap f)
⊢ Function.Surjective (comap f) ∧ ∀ (s : Set (PrimeSpectrum R)), IsClosed s ↔ IsClosed (comap f ⁻¹' s)

Tactic:
⟨h₁, fun s ↦ ⟨fun hs ↦ hs.preimage (continuous_comap f),
    fun hsc ↦ Set.image_preimage_eq s h₁ ▸ ?_⟩⟩

Premises used: Eq.rec, PrimeSpectrum.continuous_comap, Set.image_preimage_eq, And.intro, Iff.intro, IsClosed.preimage
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
h₁ : Function.Surjective (comap f)
h₂ : GeneralizingMap (comap f)
refine : ∀ (s : Set (PrimeSpectrum R)) (hsc : IsClosed (comap f ⁻¹' s)), IsClosed (comap f '' comap f ⁻¹' s)
⊢ Function.Surjective (comap f) ∧ ∀ (s : Set (PrimeSpectrum R)), IsClosed s ↔ IsClosed (comap f ⁻¹' s)

Tactic:
refine ⟨h₁, fun s ↦ ⟨fun hs ↦ hs.preimage (continuous_comap f),
    fun hsc ↦ Set.image_preimage_eq s h₁ ▸ ?_⟩⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
h₁ : Function.Surjective (comap f)
h₂ : GeneralizingMap (comap f)
s : Set (PrimeSpectrum R)
hsc : IsClosed (comap f ⁻¹' s)
apply : StableUnderSpecialization (comap f '' comap f ⁻¹' s)
⊢ IsClosed (comap f '' comap f ⁻¹' s)

Tactic:
apply isClosed_image_of_stableUnderSpecialization _ _ hsc

Premises used: PrimeSpectrum.isClosed_image_of_stableUnderSpecialization
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
h₁ : Function.Surjective (comap f)
h₂ : GeneralizingMap (comap f)
s : Set (PrimeSpectrum R)
hsc : IsClosed (comap f ⁻¹' s)
rw : StableUnderGeneralization sᶜ
⊢ StableUnderSpecialization (comap f '' comap f ⁻¹' s)

Tactic:
rw [Set.image_preimage_eq s h₁, ← stableUnderGeneralization_compl_iff]

Premises used: Set.image_preimage_eq, stableUnderGeneralization_compl_iff
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
h₁ : Function.Surjective (comap f)
h₂ : GeneralizingMap (comap f)
s : Set (PrimeSpectrum R)
hsc : IsClosed (comap f ⁻¹' s)
⊢ StableUnderGeneralization (comap f '' (comap f ⁻¹' s)ᶜ)

Tactic:
h₂.stableUnderGeneralization_image hsc.isOpen_compl.stableUnderGeneralization

Premises used: IsClosed.isOpen_compl, GeneralizingMap.stableUnderGeneralization_image, IsOpen.stableUnderGeneralization
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
h₁ : Function.Surjective (comap f)
h₂ : GeneralizingMap (comap f)
s : Set (PrimeSpectrum R)
hsc : IsClosed (comap f ⁻¹' s)
h : sᶜ = comap f '' (comap f ⁻¹' s)ᶜ
⊢ StableUnderGeneralization sᶜ

Tactic:
convert! h₂.stableUnderGeneralization_image hsc.isOpen_compl.stableUnderGeneralization

Premises used: IsClosed.isOpen_compl, GeneralizingMap.stableUnderGeneralization_image, IsOpen.stableUnderGeneralization
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
h₁ : Function.Surjective (comap f)
h₂ : GeneralizingMap (comap f)
s : Set (PrimeSpectrum R)
hsc : IsClosed (comap f ⁻¹' s)
h : sᶜ = comap f '' comap f ⁻¹' sᶜ
h₃ h₄ : sᶜ = sᶜ
⊢ sᶜ = comap f '' (comap f ⁻¹' s)ᶜ

Tactic:
rw [← Set.preimage_compl, Set.image_preimage_eq _ h₁]

Premises used: Set.image_preimage_eq, Set.preimage_compl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
h :
  ∀ (x : R), x ∈ vanishingIdeal (Set.range (comap f)) ↔ Membership.mem (γ := Ideal R) (Ideal.radical (RingHom.ker f)) x
⊢ vanishingIdeal (Set.range (comap f)) = Ideal.radical (RingHom.ker f)

Tactic:
ext x
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
x : R
h :
  x ∈ vanishingIdeal (Set.range (comap f)) ↔
    Membership.mem (γ := Ideal R) (Ideal.comap f (sInf {J : Ideal S | ⊥ ≤ J ∧ J.IsPrime})) x
⊢ x ∈ vanishingIdeal (Set.range (comap f)) ↔ Membership.mem (γ := Ideal R) (Ideal.radical (RingHom.ker f)) x

Tactic:
rw [RingHom.ker_eq_comap_bot, ← Ideal.comap_radical, Ideal.radical_eq_sInf]

Premises used: Ideal.radical_eq_sInf, RingHom.ker_eq_comap_bot, Ideal.comap_radical
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
x : R
h :
  (∀ (a : PrimeSpectrum S), Membership.mem (α := S) a.asIdeal ((f : (a : R) → S) x : S)) ↔
    ∀ (p : Submodule S S), Ideal.IsPrime p → Membership.mem (α := S) p ((f : (a : R) → S) x : S)
⊢ x ∈ vanishingIdeal (Set.range (comap f)) ↔
    Membership.mem (γ := Ideal R) (Ideal.comap f (sInf {J : Ideal S | ⊥ ≤ J ∧ J.IsPrime})) x

Tactic:
simp only [mem_vanishingIdeal, Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff,
    comap_asIdeal, Ideal.mem_comap, bot_le, true_and, Submodule.mem_sInf, Set.mem_setOf_eq]

Premises used: Set.mem_range, forall_exists_index, Set.mem_setOf_eq, Submodule.mem_sInf, PrimeSpectrum.comap_asIdeal, PrimeSpectrum.mem_vanishingIdeal, Ideal.mem_comap, forall_apply_eq_imp_iff, bot_le, true_and
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
x : R
⊢ (∀ (a : PrimeSpectrum S), Membership.mem (α := S) a.asIdeal ((f : (a : R) → S) x : S)) ↔
    ∀ (p : Submodule S S), Ideal.IsPrime p → Membership.mem (α := S) p ((f : (a : R) → S) x : S)

Tactic:
⟨fun H I hI ↦ H ⟨I, hI⟩, fun H I ↦ H I.1 I.2⟩

Premises used: PrimeSpectrum.mk, PrimeSpectrum.isPrime, Iff.intro, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
x : R
⊢ (∀ (a : PrimeSpectrum S), Membership.mem (α := S) a.asIdeal ((f : (a : R) → S) x : S)) ↔
    ∀ (p : Submodule S S), Ideal.IsPrime p → Membership.mem (α := S) p ((f : (a : R) → S) x : S)

Tactic:
exact ⟨fun H I hI ↦ H ⟨I, hI⟩, fun H I ↦ H I.1 I.2⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
rw :
  Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑(vanishingIdeal (Set.range (comap f))) : Set R))
    (zeroLocus (↑(RingHom.ker f) : Set R))
rw₁ :
  Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑(Ideal.radical (RingHom.ker f)) : Set R))
    (zeroLocus (↑(RingHom.ker f) : Set R))
rw₂ rw₃ : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑(RingHom.ker f) : Set R)) (zeroLocus (↑(RingHom.ker f) : Set R))
⊢ closure (Set.range (comap f)) = zeroLocus (↑(RingHom.ker f) : Set R)

Tactic:
rw [← zeroLocus_vanishingIdeal_eq_closure, vanishingIdeal_range_comap, zeroLocus_radical]

Premises used: PrimeSpectrum.vanishingIdeal_range_comap, PrimeSpectrum.zeroLocus_radical, PrimeSpectrum.zeroLocus_vanishingIdeal_eq_closure
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
rw : closure (Set.range (comap f)) = Set.univ ↔ LE.le (α := Ideal R) (RingHom.ker f) (nilradical R)
rw₁ :
  Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑(RingHom.ker f) : Set R)) Set.univ ↔
    LE.le (α := Ideal R) (RingHom.ker f) (nilradical R)
rw₂ : (↑(RingHom.ker f) : Set R) ⊆ (↑(nilradical R) : Set R) ↔ LE.le (α := Ideal R) (RingHom.ker f) (nilradical R)
rw₃ rw₄ : LE.le (α := Ideal R) (RingHom.ker f) (nilradical R) ↔ LE.le (α := Ideal R) (RingHom.ker f) (nilradical R)
⊢ DenseRange (comap f) ↔ LE.le (α := Ideal R) (RingHom.ker f) (nilradical R)

Tactic:
rw [denseRange_iff_closure_range, closure_range_comap, zeroLocus_eq_univ_iff,
    SetLike.coe_subset_coe]

Premises used: PrimeSpectrum.closure_range_comap, PrimeSpectrum.zeroLocus_eq_univ_iff, SetLike.coe_subset_coe, denseRange_iff_closure_range
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
mp :
  DenseRange (comap f) →
    ∀ (I : Ideal R) (h : Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) I),
      { asIdeal := I, isPrime := ⋯ : PrimeSpectrum R } ∈ Set.range (comap f)
mpr :
  (∀ (I : Ideal R) (h : Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) I),
      { asIdeal := I, isPrime := ⋯ : PrimeSpectrum R } ∈ Set.range (comap f)) →
    DenseRange (comap f)
⊢ DenseRange (comap f) ↔
    ∀ (I : Ideal R) (h : Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) I),
      { asIdeal := I, isPrime := ⋯ : PrimeSpectrum R } ∈ Set.range (comap f)

Tactic:
constructor
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
H : DenseRange (comap f)
I : Ideal R
hI : Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) I
rw :
  ∀ (H : LE.le (α := Ideal R) (RingHom.ker f) (nilradical R)) (I : Ideal R)
    (hI : Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) I),
    Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (RingHom.ker f)) I
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (RingHom.ker f)) I

Tactic:
rw [denseRange_comap_iff_ker_le_nilRadical] at H

Premises used: PrimeSpectrum.denseRange_comap_iff_ker_le_nilRadical
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
H : LE.le (α := Ideal R) (RingHom.ker f) (nilradical R)
I : Ideal R
hI : Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) I
⊢ Minimal (fun (q : Ideal R) ↦ q.IsPrime ∧ ⊥ ≤ q) I

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

Premises used: Set.mem_setOf, Ideal.IsMinimalPrime
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
H : LE.le (α := Ideal R) (RingHom.ker f) (nilradical R)
I : Ideal R
hI : Minimal (fun (q : Ideal R) ↦ q.IsPrime ∧ ⊥ ≤ q) I
⊢ Minimal (fun (q : Ideal R) ↦ q.IsPrime ∧ ⊥ ≤ q) I

Tactic:
hI
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
H : LE.le (α := Ideal R) (RingHom.ker f) (nilradical R)
I : Ideal R
hI : Minimal (fun (q : Ideal R) ↦ q.IsPrime ∧ ⊥ ≤ q) I
h : ∀ (p : Ideal R), p.IsPrime ∧ RingHom.ker f ≤ p ↔ p.IsPrime ∧ ⊥ ≤ p
⊢ Minimal (fun (q : Ideal R) ↦ q.IsPrime ∧ RingHom.ker f ≤ q) I

Tactic:
convert! hI using 2 with p
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
H : LE.le (α := Ideal R) (RingHom.ker f) (nilradical R)
I : Ideal R
hI : Minimal (fun (q : Ideal R) ↦ q.IsPrime ∧ ⊥ ≤ q) I
p : Ideal R
⊢ p.IsPrime ∧ RingHom.ker f ≤ p ↔ p.IsPrime ∧ ⊥ ≤ p

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

Premises used: Iff.mpr, And.left, And.intro, Iff.intro, LE.le.trans, Ideal.IsPrime.radical_le_iff, bot_le
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
H : LE.le (α := Ideal R) (RingHom.ker f) (nilradical R)
I : Ideal R
hI : Minimal (fun (q : Ideal R) ↦ 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)⟩⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
H : DenseRange (comap f)
I : Ideal R
hI : Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) I
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (RingHom.ker f)) I

Tactic:
have : I ∈ (RingHom.ker f).minimalPrimes := by
      rw [denseRange_comap_iff_ker_le_nilRadical] at H
      simp only [Set.mem_setOf, Ideal.IsMinimalPrime] 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)⟩⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
H : DenseRange (comap f)
I : Ideal R
hI : Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) I
this : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (RingHom.ker f)) I
mp :
  ∀ (p : Ideal S) (hp : p.IsPrime),
    ⊥ ≤ p →
      ∀ (hI : Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) (Ideal.comap f p))
        (this : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (RingHom.ker f)) (Ideal.comap f p)),
        { asIdeal := Ideal.comap f p, isPrime := ⋯ : PrimeSpectrum R } ∈ Set.range (comap f)
⊢ { asIdeal := I, isPrime := ⋯ : PrimeSpectrum R } ∈ Set.range (comap f)

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

Premises used: Ideal.exists_comap_eq_of_mem_minimalPrimes, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
H : DenseRange (comap f)
p : Ideal S
hp : p.IsPrime
left : ⊥ ≤ p
hI : Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) (Ideal.comap f p)
this : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (RingHom.ker f)) (Ideal.comap f p)
⊢ { asIdeal := Ideal.comap f p, isPrime := ⋯ : PrimeSpectrum R } ∈ Set.range (comap f)

Tactic:
⟨⟨p, hp⟩, rfl⟩

Premises used: PrimeSpectrum.mk, Set.Mem, setOf, Exists.intro, Set.range, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
H : DenseRange (comap f)
p : Ideal S
hp : p.IsPrime
left : ⊥ ≤ p
hI : Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) (Ideal.comap f p)
this : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (RingHom.ker f)) (Ideal.comap f p)
⊢ { asIdeal := Ideal.comap f p, isPrime := ⋯ : PrimeSpectrum R } ∈ Set.range (comap f)

Tactic:
exact ⟨⟨p, hp⟩, rfl⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
H :
  ∀ (I : Ideal R) (h : Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) I),
    { asIdeal := I, isPrime := ⋯ : PrimeSpectrum R } ∈ Set.range (comap f)
p : PrimeSpectrum R
mpr :
  ∀ (q : Ideal R) (hq : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊥) q) (hq' : q ≤ p.asIdeal),
    p ∈ closure (Set.range (comap f))
⊢ p ∈ closure (Set.range (comap f))

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

Premises used: Ideal.exists_minimalPrimes_le, bot_le
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
H :
  ∀ (I : Ideal R) (h : Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) I),
    { asIdeal := I, isPrime := ⋯ : PrimeSpectrum R } ∈ Set.range (comap f)
p : PrimeSpectrum R
q : Ideal R
hq : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊥) q
hq' : q ≤ p.asIdeal
⊢ p ∈ closure (Set.range (comap f))

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

Premises used: PrimeSpectrum.mk, subset_closure, PrimeSpectrum.le_iff_specializes, And.left, Iff.mp, isClosed_closure, Specializes.mem_closed
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
H :
  ∀ (I : Ideal R) (h : Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) I),
    { asIdeal := I, isPrime := ⋯ : PrimeSpectrum R } ∈ Set.range (comap f)
p : PrimeSpectrum R
q : Ideal R
hq : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊥) q
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))

Premises used: PrimeSpectrum.mk, subset_closure, PrimeSpectrum.le_iff_specializes, And.left, Iff.mp, isClosed_closure, Specializes.mem_closed