awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I) →
    ∀ {x y : R},
      HMul.hMul (α := Ideal R) (Ideal.span {x}) (Ideal.span {y}) ≤ I → Ideal.span {x} ≤ I ∨ Ideal.span {y} ≤ I

Tactic:
fun h x y h' => h _ _ ?_

Premises used: Ideal.span, Singleton.singleton
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsRadical
mp :
  ∀ (h : ∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I) (x y : R)
    (h' : HMul.hMul (α := Ideal R) (Ideal.span {x}) (Ideal.span {y}) ≤ I), Ideal.span {x} ⊓ Ideal.span {y} ≤ I
⊢ (∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I) →
    ∀ {x y : R},
      HMul.hMul (α := Ideal R) (Ideal.span {x}) (Ideal.span {y}) ≤ I → Ideal.span {x} ≤ I ∨ Ideal.span {y} ≤ I

Tactic:
refine fun h x y h' => h _ _ ?_
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsRadical
h : ∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I
x y : R
h' : HMul.hMul (α := Ideal R) (Ideal.span {x}) (Ideal.span {y}) ≤ I
mp :
  ∀ (h' : (HMul.hMul (α := Ideal R) (Ideal.span {x}) (Ideal.span {y})).radical ≤ I),
    Ideal.radical (Ideal.span {x} ⊓ Ideal.span {y}) ≤ I
⊢ Ideal.span {x} ⊓ Ideal.span {y} ≤ I

Tactic:
rw [← hI.radical_le_iff] at h' ⊢

Premises used: Ideal.IsRadical.radical_le_iff
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsRadical
h : ∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I
x y : R
h' : (HMul.hMul (α := Ideal R) (Ideal.span {x}) (Ideal.span {y})).radical ≤ I
⊢ Ideal.radical (Ideal.span {x} ⊓ Ideal.span {y}) ≤ I

Tactic:
simpa only [Ideal.radical_inf, Ideal.radical_mul] using h'

Premises used: Ideal.radical_inf, Ideal.radical_mul
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsRadical
mpr : (∀ {x y : R}, x * y ∈ I → x ∉ I → y ∈ I) → ∀ (x y : Ideal R), x ⊓ y ≤ I → (∃ x_1 ∈ x, x_1 ∉ I) → y ≤ I
⊢ (∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I) → ∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I

Tactic:
simp_rw [or_iff_not_imp_left, SetLike.not_le_iff_exists]

Premises used: Classical.or_iff_not_imp_left, SetLike.not_le_iff_exists
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsRadical
h : ∀ {x y : R}, x * y ∈ I → x ∉ I → y ∈ I
s t : Ideal R
h' : s ⊓ t ≤ I
x : R
hx : x ∈ s
hx' : x ∉ I
y : R
hy : y ∈ t
⊢ y ∈ I

Tactic:
h (h' ⟨Ideal.mul_mem_right _ _ hx, Ideal.mul_mem_left _ _ hy⟩) hx'

Premises used: Set.Mem, Ideal.mul_mem_right, And.intro, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsRadical
h : ∀ {x y : R}, x * y ∈ I → x ∉ I → y ∈ I
s t : Ideal R
h' : s ⊓ t ≤ I
x : R
hx : x ∈ s
hx' : x ∉ I
y : R
hy : y ∈ t
⊢ y ∈ I

Tactic:
exact h (h' ⟨Ideal.mul_mem_right _ _ hx, Ideal.mul_mem_left _ _ hy⟩) hx'

Premises used: Ideal.mul_mem_right, And.intro, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
⊢ IsIrreducible (X := PrimeSpectrum R) Z(↑I) ↔ I.radical.IsPrime

Tactic:
zeroLocus_radical I ▸ isIrreducible_zeroLocus_iff_of_radical _ I.radical_isRadical

Premises used: PrimeSpectrum.isIrreducible_zeroLocus_iff_of_radical, PrimeSpectrum.zeroLocus_radical, Eq.rec, Ideal.radical_isRadical
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
rw : IsIrreducible (closure s) ↔ (vanishingIdeal s).IsPrime
rw₁ : IsIrreducible (X := PrimeSpectrum R) Z(↑(vanishingIdeal s)) ↔ (vanishingIdeal s).IsPrime
rw₂ rw₃ : (vanishingIdeal s).IsPrime ↔ (vanishingIdeal s).IsPrime
⊢ IsIrreducible s ↔ (vanishingIdeal s).IsPrime

Tactic:
rw [← isIrreducible_iff_closure, ← zeroLocus_vanishingIdeal_eq_closure,
    isIrreducible_zeroLocus_iff_of_radical _ (isRadical_vanishingIdeal s)]

Premises used: PrimeSpectrum.isIrreducible_zeroLocus_iff_of_radical, PrimeSpectrum.isRadical_vanishingIdeal, isIrreducible_iff_closure, PrimeSpectrum.zeroLocus_vanishingIdeal_eq_closure
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq.{u + 1} (α := Set (Ideal R)) (vanishingIdeal '' {s : Set (PrimeSpectrum R) | IsIrreducible s})
    {P : Ideal R | P.IsPrime}

Tactic:
Set.ext fun I ↦ ⟨fun ⟨_, hs, e⟩ ↦ e ▸ isIrreducible_iff_vanishingIdeal_isPrime.mp hs,
    fun h ↦ ⟨zeroLocus I, (isIrreducible_zeroLocus_iff_of_radical _ h.isRadical).mpr h,
      (vanishingIdeal_zeroLocus_eq_radical I).trans h.radical⟩⟩

Premises used: Iff.mpr, Set.ext, PrimeSpectrum.zeroLocus, PrimeSpectrum.vanishingIdeal_zeroLocus_eq_radical, _private.0.PrimeSpectrum.vanishingIdeal_isIrreducible.match_1, setOf, PrimeSpectrum.isIrreducible_zeroLocus_iff_of_radical, Membership.mem, Eq.rec, SetLike.coe, And.intro, Ideal.IsPrime.isRadical, Iff.intro, Ideal.IsPrime, Exists.intro, Iff.mp, PrimeSpectrum.isIrreducible_iff_vanishingIdeal_isPrime, Ideal.IsPrime.radical, Eq.trans
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq.{u + 1} (α := Set (Ideal R)) (vanishingIdeal '' {s : Set (PrimeSpectrum R) | IsClosed s ∧ IsIrreducible s})
    {P : Ideal R | P.IsPrime}

Tactic:
(subset_antisymm ?_ ?_).trans vanishingIdeal_isIrreducible

Premises used: subset_antisymm, PrimeSpectrum.vanishingIdeal_isIrreducible, Eq.trans
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
refine_1 :
  Subset.{u} (α := Set (Ideal R)) (vanishingIdeal '' {s : Set (PrimeSpectrum R) | IsClosed s ∧ IsIrreducible s})
    (vanishingIdeal '' {s : Set (PrimeSpectrum R) | IsIrreducible s})
refine_2 :
  Subset.{u} (α := Set (Ideal R)) (vanishingIdeal '' {s : Set (PrimeSpectrum R) | IsIrreducible s})
    (vanishingIdeal '' {s : Set (PrimeSpectrum R) | IsClosed s ∧ IsIrreducible s})
⊢ Eq.{u + 1} (α := Set (Ideal R)) (vanishingIdeal '' {s : Set (PrimeSpectrum R) | IsClosed s ∧ IsIrreducible s})
    {P : Ideal R | P.IsPrime}

Tactic:
refine (subset_antisymm ?_ ?_).trans vanishingIdeal_isIrreducible

Premises used: subset_antisymm, PrimeSpectrum.vanishingIdeal_isIrreducible, Eq.trans
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
⊢ Subset.{u} (α := Set (Ideal R)) (vanishingIdeal '' {s : Set (PrimeSpectrum R) | IsClosed s ∧ IsIrreducible s})
    (vanishingIdeal '' {s : Set (PrimeSpectrum R) | IsIrreducible s})

Tactic:
Set.image_mono fun _ ↦ And.right

Premises used: Set.image_mono, And.right
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
⊢ Subset.{u} (α := Set (Ideal R)) (vanishingIdeal '' {s : Set (PrimeSpectrum R) | IsClosed s ∧ IsIrreducible s})
    (vanishingIdeal '' {s : Set (PrimeSpectrum R) | IsIrreducible s})

Tactic:
exact Set.image_mono fun _ ↦ And.right

Premises used: Set.image_mono, And.right
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
hs : Membership.mem (γ := Set (Set (PrimeSpectrum R))) {s : Set (PrimeSpectrum R) | IsIrreducible s} s
⊢ Membership.mem (γ := Set (Ideal R)) (vanishingIdeal '' {s : Set (PrimeSpectrum R) | IsClosed s ∧ IsIrreducible s})
    (vanishingIdeal s)

Tactic:
⟨closure s, ⟨isClosed_closure, hs.closure⟩, vanishingIdeal_closure s⟩

Premises used: Set.Mem, setOf, IsIrreducible.closure, closure, And.intro, Exists.intro, Set.image, isClosed_closure, PrimeSpectrum.vanishingIdeal_closure
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
hs : Membership.mem (γ := Set (Set (PrimeSpectrum R))) {s : Set (PrimeSpectrum R) | IsIrreducible s} s
⊢ Membership.mem (γ := Set (Ideal R)) (vanishingIdeal '' {s : Set (PrimeSpectrum R) | IsClosed s ∧ IsIrreducible s})
    (vanishingIdeal s)

Tactic:
exact ⟨closure s, ⟨isClosed_closure, hs.closure⟩, vanishingIdeal_closure s⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
⊢ IrreducibleSpace.{u} (PrimeSpectrum R) ↔ Ideal.IsPrime (nilradical R)

Tactic:
simp [irreducibleSpace_def, isIrreducible_iff_vanishingIdeal_isPrime]

Premises used: PrimeSpectrum.isIrreducible_iff_vanishingIdeal_isPrime, irreducibleSpace_def
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : IsDomain R
⊢ IrreducibleSpace.{u} (PrimeSpectrum R)

Tactic:
simpa [irreducibleSpace_iff_isPrime_nilradical] using Ideal.isPrime_bot

Premises used: PrimeSpectrum.irreducibleSpace_iff_isPrime_nilradical, Ideal.isPrime_bot
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S_1 : Type v
inst : CommSemiring R
inst_1 : CommSemiring S_1
S : Set (PrimeSpectrum R)
h₁ : IsIrreducible S
h₂ : IsClosed S
rw : closure {{ asIdeal := vanishingIdeal S, isPrime := ⋯ : PrimeSpectrum R }} = S
rw₁ : Z(↑{ asIdeal := vanishingIdeal S, isPrime := ⋯ : PrimeSpectrum R }.asIdeal) = S
rw₂ : closure S = S
rw₃ rw₄ : S = S
⊢ IsGenericPoint { asIdeal := vanishingIdeal S, isPrime := ⋯ : PrimeSpectrum R } S

Tactic:
rw [IsGenericPoint, closure_singleton, zeroLocus_vanishingIdeal_eq_closure, h₂.closure_eq]

Premises used: IsGenericPoint, IsClosed.closure_eq, PrimeSpectrum.closure_singleton, PrimeSpectrum.zeroLocus_vanishingIdeal_eq_closure
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
I : Set R
⊢ QuasiSober.{u} (↑(zeroLocus I) : Type u)

Tactic:
(isClosed_zeroLocus I).isClosedEmbedding_subtypeVal.quasiSober

Premises used: PrimeSpectrum.isClosed_zeroLocus, Topology.IsClosedEmbedding.quasiSober, IsClosed.isClosedEmbedding_subtypeVal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
⊢ CompactSpace.{u} (PrimeSpectrum R)

Tactic:
compactSpace_of_finite_subfamily_closed fun S S_closed S_empty ↦ ?_

Premises used: compactSpace_of_finite_subfamily_closed
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
refine :
  ∀ {ι : Type u} (S : ι → Set (PrimeSpectrum R)) (S_closed : ∀ (i : ι), IsClosed (S i))
    (S_empty : Eq.{u + 1} (α := Set (PrimeSpectrum R)) (⋂ (i : ι), S i) ∅),
    ∃ (u : Finset ι), Eq.{u + 1} (α := Set (PrimeSpectrum R)) (⋂ i ∈ u, S i) ∅
⊢ CompactSpace.{u} (PrimeSpectrum R)

Tactic:
refine compactSpace_of_finite_subfamily_closed fun S S_closed S_empty ↦ ?_

Premises used: compactSpace_of_finite_subfamily_closed
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S_1 : Type v
inst : CommSemiring R
inst_1 : CommSemiring S_1
ι : Type u
S : ι → Set (PrimeSpectrum R)
S_closed : ∀ (i : ι), IsClosed (S i)
S_empty : Eq.{u + 1} (α := Set (PrimeSpectrum R)) (⋂ (i : ι), S i) ∅
choose :
  ∀ (I : (i : ι) → Ideal R) (hI : ∀ (i : ι), S i = Z(↑(I i))),
    ∃ (u : Finset ι), Eq.{u + 1} (α := Set (PrimeSpectrum R)) (⋂ i ∈ u, S i) ∅
⊢ ∃ (u : Finset ι), Eq.{u + 1} (α := Set (PrimeSpectrum R)) (⋂ i ∈ u, S i) ∅

Tactic:
choose I hI using fun i ↦ (isClosed_iff_zeroLocus_ideal (S i)).mp (S_closed i)

Premises used: PrimeSpectrum.isClosed_iff_zeroLocus_ideal, Iff.mp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S_1 : Type v
inst : CommSemiring R
inst_1 : CommSemiring S_1
ι : Type u
S : ι → Set (PrimeSpectrum R)
S_closed : ∀ (i : ι), IsClosed (S i)
S_empty : Eq.{u + 1} (α := Set (PrimeSpectrum R)) (⋂ (i : ι), S i) ∅
I : (i : ι) → Ideal R
hI : ∀ (i : ι), S i = Z(↑(I i))
simp_rw :
  ∀ (S_empty : LE.le.{u} (α := Ideal R) ⊤ (⨆ (i : ι), I i)), ∃ (u : Finset ι), LE.le.{u} (α := Ideal R) ⊤ (⨆ i ∈ u, I i)
⊢ ∃ (u : Finset ι), Eq.{u + 1} (α := Set (PrimeSpectrum R)) (⋂ i ∈ u, S i) ∅

Tactic:
simp_rw [hI, ← zeroLocus_iSup, zeroLocus_empty_iff_eq_top, ← top_le_iff] at S_empty ⊢

Premises used: PrimeSpectrum.zeroLocus_iSup, top_le_iff, PrimeSpectrum.zeroLocus_empty_iff_eq_top
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S_1 : Type v
inst : CommSemiring R
inst_1 : CommSemiring S_1
ι : Type u
S : ι → Set (PrimeSpectrum R)
S_closed : ∀ (i : ι), IsClosed (S i)
I : (i : ι) → Ideal R
hI : ∀ (i : ι), S i = Z(↑(I i))
S_empty : LE.le.{u} (α := Ideal R) ⊤ (⨆ (i : ι), I i)
⊢ ∃ (u : Finset ι), LE.le.{u} (α := Ideal R) ⊤ (⨆ i ∈ u, I i)

Tactic:
CompleteLattice.IsCompactElement.exists_finset_of_le_iSup _
    Ideal.isCompactElement_top _ S_empty

Premises used: Set.Mem, Ideal.isCompactElement_top, CompleteLattice.IsCompactElement.exists_finset_of_le_iSup
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S_1 : Type v
inst : CommSemiring R
inst_1 : CommSemiring S_1
ι : Type u
S : ι → Set (PrimeSpectrum R)
S_closed : ∀ (i : ι), IsClosed (S i)
I : (i : ι) → Ideal R
hI : ∀ (i : ι), S i = Z(↑(I i))
S_empty : LE.le.{u} (α := Ideal R) ⊤ (⨆ (i : ι), I i)
⊢ ∃ (u : Finset ι), LE.le.{u} (α := Ideal R) ⊤ (⨆ i ∈ u, I i)

Tactic:
exact CompleteLattice.IsCompactElement.exists_finset_of_le_iSup _
    Ideal.isCompactElement_top _ S_empty

Premises used: Ideal.isCompactElement_top, CompleteLattice.IsCompactElement.exists_finset_of_le_iSup
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
⊢ DiscreteTopology.{u} (PrimeSpectrum R) ↔ Finite.{u + 1} (PrimeSpectrum R) ∧ Ring.KrullDimLE 0 R

Tactic:
⟨fun _ ↦ ⟨finite_of_compact_of_discrete, .mk₀ fun I h ↦ isClosed_singleton_iff_isMaximal ⟨I, h⟩
    |>.mp <| discreteTopology_iff_forall_isClosed.mp ‹_› _⟩, fun ⟨_, _⟩ ↦
    .of_finite_of_isClosed_singleton fun p ↦ (isClosed_singleton_iff_isMaximal p).mpr inferInstance⟩

Premises used: _private.0.PrimeSpectrum.discreteTopology_iff_finite_and_krullDimLE_zero.match_1, Iff.mpr, PrimeSpectrum.mk, finite_of_compact_of_discrete, DiscreteTopology, Ring.KrullDimLE.mk₀, inferInstance, PrimeSpectrum.isClosed_singleton_iff_isMaximal, discreteTopology_iff_forall_isClosed, And.intro, DiscreteTopology.of_finite_of_isClosed_singleton, Iff.intro, Iff.mp, PrimeSpectrum, Singleton.singleton
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
rw :
  (Set.Finite.{u} (α := Ideal R) {x : Ideal R | x.IsPrime} ∧ ∀ (I : Ideal R), I.IsPrime → I.IsMaximal) ↔
    Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal} ∧
      LE.le (α := Ideal R) (sInf {I : Ideal R | I.IsMaximal}) (nilradical R)
⊢ DiscreteTopology.{u} (PrimeSpectrum R) ↔
    Finite.{u + 1} (↑{I : Ideal R | I.IsMaximal} : Type u) ∧
      LE.le (α := Ideal R) (sInf {I : Ideal R | I.IsMaximal}) (nilradical R)

Tactic:
rw [discreteTopology_iff_finite_and_krullDimLE_zero, Ring.krullDimLE_zero_iff,
    (equivSubtype R).finite_iff, ← Set.coe_setOf, Set.finite_coe_iff, Set.finite_coe_iff]

Premises used: PrimeSpectrum.discreteTopology_iff_finite_and_krullDimLE_zero, Equiv.finite_iff, Ring.krullDimLE_zero_iff, PrimeSpectrum.equivSubtype, Set.finite_coe_iff, Set.coe_setOf, RelIso.toEquiv
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
⊢ (Set.Finite.{u} (α := Ideal R) {x : Ideal R | x.IsPrime} ∧ ∀ (I : Ideal R), I.IsPrime → I.IsMaximal) ↔
    Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal} ∧
      LE.le (α := Ideal R) (sInf {I : Ideal R | I.IsMaximal}) (nilradical R)

Tactic:
⟨fun h ↦ ⟨h.1.subset fun _ h ↦ h.isPrime, nilradical_eq_sInf R ▸ sInf_le_sInf h.2⟩,
    fun ⟨fin, le⟩ ↦ ?_⟩

Premises used: setOf, sInf_le_sInf, Set.Finite, Eq.rec, Set.Finite.subset, Ideal.IsMaximal.isPrime, And, And.right, And.left, And.intro, Iff.intro, Ideal.IsPrime, _private.0.PrimeSpectrum.discreteTopology_iff_finite_isMaximal_and_sInf_le_nilradical.match_1, nilradical_eq_sInf, Eq.symm
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
refine :
  Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal} ∧
      LE.le (α := Ideal R) (sInf {I : Ideal R | I.IsMaximal}) (nilradical R) →
    ∀ (fin : Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal})
      (le : LE.le (α := Ideal R) (sInf {I : Ideal R | I.IsMaximal}) (nilradical R)),
      Set.Finite.{u} (α := Ideal R) {x : Ideal R | x.IsPrime} ∧ ∀ (I : Ideal R), I.IsPrime → I.IsMaximal
⊢ (Set.Finite.{u} (α := Ideal R) {x : Ideal R | x.IsPrime} ∧ ∀ (I : Ideal R), I.IsPrime → I.IsMaximal) ↔
    Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal} ∧
      LE.le (α := Ideal R) (sInf {I : Ideal R | I.IsMaximal}) (nilradical R)

Tactic:
refine ⟨fun h ↦ ⟨h.1.subset fun _ h ↦ h.isPrime, nilradical_eq_sInf R ▸ sInf_le_sInf h.2⟩,
    fun ⟨fin, le⟩ ↦ ?_⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
h :
  Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal} ∧
    LE.le (α := Ideal R) (sInf {I : Ideal R | I.IsMaximal}) (nilradical R)
fin : Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal}
le : LE.le (α := Ideal R) (sInf {I : Ideal R | I.IsMaximal}) (nilradical R)
I : Ideal R
hI : I.IsPrime
⊢ sInf {I : Ideal R | I.IsMaximal} ≤ I

Tactic:
replace le := le.trans (nilradical_le_prime I)
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
h :
  Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal} ∧
    LE.le (α := Ideal R) (sInf {I : Ideal R | I.IsMaximal}) (nilradical R)
fin : Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal}
I : Ideal R
hI : I.IsPrime
le : sInf {I : Ideal R | I.IsMaximal} ≤ I
⊢ ∃ i ∈ fin.toFinset (s := {I : Ideal R | I.IsMaximal}), id i ≤ I

Tactic:
rw [← fin.coe_toFinset, ← Finset.inf_id_eq_sInf, hI.inf_le'] at le

Premises used: Finset.inf_id_eq_sInf, Ideal.IsPrime.inf_le', Set.Finite.coe_toFinset
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
h :
  Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal} ∧
    LE.le (α := Ideal R) (sInf {I : Ideal R | I.IsMaximal}) (nilradical R)
fin : Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal}
I : Ideal R
hI : I.IsPrime
le : ∃ i ∈ fin.toFinset (s := {I : Ideal R | I.IsMaximal}), id i ≤ I
have : ∀ (M : Ideal R) (hM : M ∈ fin.toFinset (s := {I : Ideal R | I.IsMaximal})) (hMI : id M ≤ I), I.IsMaximal
⊢ I.IsMaximal

Tactic:
have ⟨M, hM, hMI⟩ := le
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
h :
  Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal} ∧
    LE.le (α := Ideal R) (sInf {I : Ideal R | I.IsMaximal}) (nilradical R)
fin : Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal}
I : Ideal R
hI : I.IsPrime
le : ∃ i ∈ fin.toFinset (s := {I : Ideal R | I.IsMaximal}), id i ≤ I
M : Ideal R
hM : M ∈ fin.toFinset (s := {I : Ideal R | I.IsMaximal})
hMI : id M ≤ I
⊢ Membership.mem (γ := Set (Ideal R)) {I : Ideal R | I.IsMaximal} M

Tactic:
rw [fin.mem_toFinset] at hM

Premises used: Set.Finite.mem_toFinset
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
h :
  Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal} ∧
    LE.le (α := Ideal R) (sInf {I : Ideal R | I.IsMaximal}) (nilradical R)
fin : Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal}
I : Ideal R
hI : I.IsPrime
le : ∃ i ∈ fin.toFinset (s := {I : Ideal R | I.IsMaximal}), id i ≤ I
M : Ideal R
hM : M ∈ fin.toFinset (s := {I : Ideal R | I.IsMaximal})
hMI : id M ≤ I
hM₁ : Membership.mem (γ := Set (Ideal R)) {I : Ideal R | I.IsMaximal} M
⊢ id M ≤ I

Tactic:
rw [fin.mem_toFinset] at hM

Premises used: Set.Finite.mem_toFinset
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
h :
  Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal} ∧
    LE.le (α := Ideal R) (sInf {I : Ideal R | I.IsMaximal}) (nilradical R)
fin : Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal}
I : Ideal R
hI : I.IsPrime
le : ∃ i ∈ fin.toFinset (s := {I : Ideal R | I.IsMaximal}), id i ≤ I
M : Ideal R
hM : Membership.mem (γ := Set (Ideal R)) {I : Ideal R | I.IsMaximal} M
hMI : id M ≤ I
rwa rwa₁ rwa₂ rwa₃ : M.IsMaximal
⊢ I.IsMaximal

Tactic:
rwa [← hM.eq_of_le hI.1 hMI]

Premises used: Ideal.IsMaximal.eq_of_le, Ideal.IsPrime.ne_top'
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
h :
  Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal} ∧
    LE.le (α := Ideal R) (sInf {I : Ideal R | I.IsMaximal}) (nilradical R)
fin : Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal}
le : LE.le (α := Ideal R) (sInf {I : Ideal R | I.IsMaximal}) (nilradical R)
⊢ ∀ (I : Ideal R) (hI : I.IsPrime), I.IsMaximal

Tactic:
have hpm (I : Ideal R) (hI : I.IsPrime) : I.IsMaximal := by
    replace le := le.trans (nilradical_le_prime I)
    rw [← fin.coe_toFinset, ← Finset.inf_id_eq_sInf, hI.inf_le'] at le
    have ⟨M, hM, hMI⟩ := le
    rw [fin.mem_toFinset] at hM
    rwa [← hM.eq_of_le hI.1 hMI]
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
h :
  Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal} ∧
    LE.le (α := Ideal R) (sInf {I : Ideal R | I.IsMaximal}) (nilradical R)
fin : Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal}
le : LE.le (α := Ideal R) (sInf {I : Ideal R | I.IsMaximal}) (nilradical R)
hpm : ∀ (I : Ideal R) (hI : I.IsPrime), I.IsMaximal
⊢ Set.Finite.{u} (α := Ideal R) {x : Ideal R | x.IsPrime} ∧ ∀ (I : Ideal R), I.IsPrime → I.IsMaximal

Tactic:
⟨fin.subset hpm, hpm⟩

Premises used: Set.Finite.subset, And.intro
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
h :
  Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal} ∧
    LE.le (α := Ideal R) (sInf {I : Ideal R | I.IsMaximal}) (nilradical R)
fin : Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal}
le : LE.le (α := Ideal R) (sInf {I : Ideal R | I.IsMaximal}) (nilradical R)
hpm : ∀ (I : Ideal R) (hI : I.IsPrime), I.IsMaximal
⊢ Set.Finite.{u} (α := Ideal R) {x : Ideal R | x.IsPrime} ∧ ∀ (I : Ideal R), I.IsPrime → I.IsMaximal

Tactic:
exact ⟨fin.subset hpm, hpm⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
surj : Function.Surjective (α := R) (β := PiLocalization R) (⇑(toPiLocalization R) : (a : R) → PiLocalization R)
⊢ DiscreteTopology.{u} (PrimeSpectrum R)

Tactic:
discreteTopology_iff_finite_and_krullDimLE_zero.mpr ⟨finite_of_toPiLocalization_surjective
    surj, .mk₀ fun I prime ↦ isMaximal_of_toPiLocalization_surjective surj ⟨I, prime⟩⟩

Premises used: Iff.mpr, PrimeSpectrum.discreteTopology_iff_finite_and_krullDimLE_zero, PrimeSpectrum.mk, PrimeSpectrum.finite_of_toPiLocalization_surjective, Ring.KrullDimLE.mk₀, And.intro, PrimeSpectrum.isMaximal_of_toPiLocalization_surjective
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
simp :
  ∀ (s : Set (PrimeSpectrum R)), (∃ (s_1 : Set R), s = zeroLocus s_1) → ∃ (s_1 : Set S), comap f ⁻¹' s = zeroLocus s_1
⊢ Continuous (comap f)

Tactic:
simp only [continuous_iff_isClosed, isClosed_iff_zeroLocus]

Premises used: PrimeSpectrum.isClosed_iff_zeroLocus, continuous_iff_isClosed
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
s : Set R
⊢ ∃ (s_1 : Set S), comap f ⁻¹' zeroLocus s = zeroLocus s_1

Tactic:
⟨_, preimage_comap_zeroLocus_aux f s⟩

Premises used: PrimeSpectrum.preimage_comap_zeroLocus_aux, Exists.intro
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
s : Set R
⊢ ∃ (s_1 : Set S), comap f ⁻¹' zeroLocus s = zeroLocus s_1

Tactic:
exact ⟨_, preimage_comap_zeroLocus_aux f s⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
x : PrimeSpectrum S
⊢ comap f x = comap f x

Tactic:
rfl

Premises used: rfl