awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
Z : Set (PrimeSpectrum R)
⊢ IsClosed Z ↔ ∃ (I : Ideal R), Z = zeroLocus (↑I : Set R)

Tactic:
(isClosed_iff_zeroLocus _).trans
    ⟨fun ⟨s, hs⟩ => ⟨_, (zeroLocus_span s).substr hs⟩, fun ⟨I, hI⟩ => ⟨I, hI⟩⟩

Premises used: PrimeSpectrum.isClosed_iff_zeroLocus, PrimeSpectrum.zeroLocus, PrimeSpectrum.zeroLocus_span, Exists, _private.0.PrimeSpectrum.isClosed_iff_zeroLocus_ideal.match_2, _private.0.PrimeSpectrum.isClosed_iff_zeroLocus_ideal.match_1, SetLike.coe, Iff.intro, Exists.intro, Eq.substr, Iff.trans, Ideal.span, Eq
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
Z : Set (PrimeSpectrum R)
⊢ IsClosed Z ↔ ∃ (I : Ideal R), I.IsRadical ∧ Z = zeroLocus (↑I : Set R)

Tactic:
(isClosed_iff_zeroLocus_ideal _).trans
    ⟨fun ⟨I, hI⟩ => ⟨_, I.radical_isRadical, (zeroLocus_radical I).substr hI⟩, fun ⟨I, _, hI⟩ =>
      ⟨I, hI⟩⟩

Premises used: PrimeSpectrum.zeroLocus, _private.0.PrimeSpectrum.isClosed_iff_zeroLocus_radical_ideal.match_1, PrimeSpectrum.zeroLocus_radical, Exists, _private.0.PrimeSpectrum.isClosed_iff_zeroLocus_ideal.match_2, PrimeSpectrum.isClosed_iff_zeroLocus_ideal, And, SetLike.coe, And.intro, Ideal.IsRadical, Iff.intro, Exists.intro, Eq.substr, Iff.trans, Ideal.radical_isRadical, Eq, Ideal.radical
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set R
rw : ∃ (s_1 : Set R), Eq (α := Set (PrimeSpectrum R)) (zeroLocus s) (zeroLocus s_1)
⊢ IsClosed (X := PrimeSpectrum R) (zeroLocus s)

Tactic:
rw [isClosed_iff_zeroLocus]

Premises used: PrimeSpectrum.isClosed_iff_zeroLocus
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set R
⊢ ∃ (s_1 : Set R), Eq (α := Set (PrimeSpectrum R)) (zeroLocus s) (zeroLocus s_1)

Tactic:
⟨s, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set R
⊢ ∃ (s_1 : Set R), Eq (α := Set (PrimeSpectrum R)) (zeroLocus s) (zeroLocus s_1)

Tactic:
exact ⟨s, rfl⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
t : Set (PrimeSpectrum R)
rcases : ∀ (I : Set R) (hI : closure t = zeroLocus I), zeroLocus (↑(vanishingIdeal t) : Set R) = closure t
⊢ zeroLocus (↑(vanishingIdeal t) : Set R) = closure t

Tactic:
rcases isClosed_iff_zeroLocus (closure t) |>.mp isClosed_closure with ⟨I, hI⟩

Premises used: PrimeSpectrum.isClosed_iff_zeroLocus, closure, Iff.mp, isClosed_closure
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
t : Set (PrimeSpectrum R)
I : Set R
hI : closure t = zeroLocus I
rw : t ⊆ closure t ∧ t ⊆ zeroLocus (↑(vanishingIdeal t) : Set R)
⊢ zeroLocus (↑(vanishingIdeal t) : Set R) = closure t

Tactic:
rw [subset_antisymm_iff, (isClosed_zeroLocus _).closure_subset_iff, hI,
      subset_zeroLocus_iff_subset_vanishingIdeal, (gc R).u_l_u_eq_u,
      ← subset_zeroLocus_iff_subset_vanishingIdeal, ← hI]

Premises used: PrimeSpectrum.isClosed_zeroLocus, PrimeSpectrum.gc, IsClosed.closure_subset_iff, subset_antisymm_iff, PrimeSpectrum.subset_zeroLocus_iff_subset_vanishingIdeal, GaloisConnection.u_l_u_eq_u
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
t : Set (PrimeSpectrum R)
I : Set R
hI : closure t = zeroLocus I
⊢ t ⊆ closure t ∧ t ⊆ zeroLocus (↑(vanishingIdeal t) : Set R)

Tactic:
⟨subset_closure, subset_zeroLocus_vanishingIdeal t⟩

Premises used: subset_closure, And.intro, PrimeSpectrum.subset_zeroLocus_vanishingIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
t : Set (PrimeSpectrum R)
I : Set R
hI : closure t = zeroLocus I
⊢ t ⊆ closure t ∧ t ⊆ zeroLocus (↑(vanishingIdeal t) : Set R)

Tactic:
exact ⟨subset_closure, subset_zeroLocus_vanishingIdeal t⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
t : Set (PrimeSpectrum R)
⊢ vanishingIdeal (closure t) = vanishingIdeal t

Tactic:
zeroLocus_vanishingIdeal_eq_closure t ▸ (gc R).u_l_u_eq_u t

Premises used: PrimeSpectrum.gc, Eq.rec, GaloisConnection.u_l_u_eq_u, PrimeSpectrum.zeroLocus_vanishingIdeal_eq_closure
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
x : PrimeSpectrum R
rw : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑(vanishingIdeal {x}) : Set R)) (zeroLocus (↑x.asIdeal : Set R))
rw₁ rw₂ : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑x.asIdeal : Set R)) (zeroLocus (↑x.asIdeal : Set R))
⊢ Eq (α := Set (PrimeSpectrum R)) (closure {x}) (zeroLocus (↑x.asIdeal : Set R))

Tactic:
rw [← zeroLocus_vanishingIdeal_eq_closure, vanishingIdeal_singleton]

Premises used: PrimeSpectrum.vanishingIdeal_singleton, PrimeSpectrum.zeroLocus_vanishingIdeal_eq_closure
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
x : PrimeSpectrum R
rw : Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑x.asIdeal : Set R)) {x} ↔ x.asIdeal.IsMaximal
⊢ IsClosed (X := PrimeSpectrum R) {x} ↔ x.asIdeal.IsMaximal

Tactic:
rw [← closure_subset_iff_isClosed, ← zeroLocus_vanishingIdeal_eq_closure,
      vanishingIdeal_singleton]

Premises used: closure_subset_iff_isClosed, PrimeSpectrum.vanishingIdeal_singleton, PrimeSpectrum.zeroLocus_vanishingIdeal_eq_closure
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
x : PrimeSpectrum R
mp : Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑x.asIdeal : Set R)) {x} → x.asIdeal.IsMaximal
mpr : x.asIdeal.IsMaximal → Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑x.asIdeal : Set R)) {x}
⊢ Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑x.asIdeal : Set R)) {x} ↔ x.asIdeal.IsMaximal

Tactic:
constructor
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
x : PrimeSpectrum R
H : Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑x.asIdeal : Set R)) {x}
mp : ∀ (m : Ideal R) (hm : m.IsMaximal) (hxm : x.asIdeal ≤ m), x.asIdeal.IsMaximal
⊢ x.asIdeal.IsMaximal

Tactic:
rcases x.asIdeal.exists_le_maximal x.2.1 with ⟨m, hm, hxm⟩

Premises used: Ideal.exists_le_maximal, Ideal.IsPrime.ne_top', PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
x : PrimeSpectrum R
H : Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑x.asIdeal : Set R)) {x}
m : Ideal R
hm : m.IsMaximal
hxm : x.asIdeal ≤ m
⊢ x.asIdeal.IsMaximal

Tactic:
(congr_arg asIdeal (@H ⟨m, hm.isPrime⟩ hxm)) ▸ hm

Premises used: Eq.rec, congr_arg, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
x : PrimeSpectrum R
H : Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑x.asIdeal : Set R)) {x}
m : Ideal R
hm : m.IsMaximal
hxm : x.asIdeal ≤ m
⊢ x.asIdeal.IsMaximal

Tactic:
exact (congr_arg asIdeal (@H ⟨m, hm.isPrime⟩ hxm)) ▸ hm
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
x : PrimeSpectrum R
H : x.asIdeal.IsMaximal
⊢ Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑x.asIdeal : Set R)) {x}

Tactic:
fun p hp ↦ PrimeSpectrum.ext (H.eq_of_le p.2.1 hp).symm

Premises used: PrimeSpectrum.ext, Set.Mem, setOf, Set.Subset, Ideal.IsMaximal.eq_of_le, Set.singleton, Ideal.IsPrime.ne_top', Eq.symm
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
x : PrimeSpectrum R
H : x.asIdeal.IsMaximal
⊢ Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑x.asIdeal : Set R)) {x}

Tactic:
exact fun p hp ↦ PrimeSpectrum.ext (H.eq_of_le p.2.1 hp).symm

Premises used: PrimeSpectrum.ext, Ideal.IsMaximal.eq_of_le, Eq.symm
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
rw : (vanishingIdeal s).radical.IsRadical
⊢ (vanishingIdeal s).IsRadical

Tactic:
rw [← vanishingIdeal_closure, ← zeroLocus_vanishingIdeal_eq_closure,
    vanishingIdeal_zeroLocus_eq_radical]

Premises used: PrimeSpectrum.vanishingIdeal_zeroLocus_eq_radical, PrimeSpectrum.vanishingIdeal_closure, PrimeSpectrum.zeroLocus_vanishingIdeal_eq_closure
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ (vanishingIdeal s).radical.IsRadical

Tactic:
apply Ideal.radical_isRadical

Premises used: Ideal.radical_isRadical
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
mp : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus (↑J : Set R)) → I.radical = J.radical
mpr : I.radical = J.radical → Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus (↑J : Set R))
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus (↑J : Set R)) ↔ I.radical = J.radical

Tactic:
constructor
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
h : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus (↑J : Set R))
mp : Eq (α := Ideal R) (vanishingIdeal (zeroLocus (↑I : Set R))) (vanishingIdeal (zeroLocus (↑J : Set R)))
⊢ I.radical = J.radical

Tactic:
simp_rw [← vanishingIdeal_zeroLocus_eq_radical, h]

Premises used: PrimeSpectrum.vanishingIdeal_zeroLocus_eq_radical
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
h : I.radical = J.radical
mpr : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I.radical : Set R)) (zeroLocus (↑J : Set R))
mpr₁ : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑J.radical : Set R)) (zeroLocus (↑J : Set R))
mpr₂ mpr₃ : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑J : Set R)) (zeroLocus (↑J : Set R))
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus (↑J : Set R))

Tactic:
rw [← zeroLocus_radical, h, zeroLocus_radical]

Premises used: PrimeSpectrum.zeroLocus_radical
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s t : Set (PrimeSpectrum R)
ht : IsClosed t
h : vanishingIdeal t ≤ vanishingIdeal s
rw : closure s ⊆ closure t
⊢ s ⊆ t

Tactic:
rw [← ht.closure_subset_iff, ← ht.closure_eq]

Premises used: IsClosed.closure_eq, IsClosed.closure_subset_iff
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s t : Set (PrimeSpectrum R)
ht : IsClosed t
h : vanishingIdeal t ≤ vanishingIdeal s
⊢ Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑(vanishingIdeal s) : Set R))
    (zeroLocus (↑(vanishingIdeal t) : Set R))

Tactic:
zeroLocus_anti_mono_ideal h

Premises used: PrimeSpectrum.zeroLocus_anti_mono_ideal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s t : Set (PrimeSpectrum R)
ht : IsClosed t
h : vanishingIdeal t ≤ vanishingIdeal s
h₁ : zeroLocus (↑(vanishingIdeal s) : Set R) = closure s
h₂ : zeroLocus (↑(vanishingIdeal t) : Set R) = closure t
⊢ closure s ⊆ closure t

Tactic:
convert! ← zeroLocus_anti_mono_ideal h

Premises used: PrimeSpectrum.zeroLocus_anti_mono_ideal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s t : Set (PrimeSpectrum R)
ht : IsClosed t
h : vanishingIdeal t ≤ vanishingIdeal s
⊢ zeroLocus (↑(vanishingIdeal s) : Set R) = closure s

Tactic:
apply zeroLocus_vanishingIdeal_eq_closure

Premises used: PrimeSpectrum.zeroLocus_vanishingIdeal_eq_closure
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s t : Set (PrimeSpectrum R)
ht : IsClosed t
h : vanishingIdeal t ≤ vanishingIdeal s
⊢ zeroLocus (↑(vanishingIdeal t) : Set R) = closure t

Tactic:
apply zeroLocus_vanishingIdeal_eq_closure

Premises used: PrimeSpectrum.zeroLocus_vanishingIdeal_eq_closure
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s t : Set (PrimeSpectrum R)
hs : IsClosed s
ht : IsClosed t
rw : s ⊆ t ∧ ¬t ⊆ s ↔ vanishingIdeal t < vanishingIdeal s
rw₁ : s ⊆ t ∧ ¬vanishingIdeal s ≤ vanishingIdeal t ↔ vanishingIdeal t < vanishingIdeal s
rw₂ : vanishingIdeal t ≤ vanishingIdeal s ∧ ¬vanishingIdeal s ≤ vanishingIdeal t ↔ vanishingIdeal t < vanishingIdeal s
rw₃ rw₄ :
  vanishingIdeal t ≤ vanishingIdeal s ∧ ¬vanishingIdeal s ≤ vanishingIdeal t ↔
    vanishingIdeal t ≤ vanishingIdeal s ∧ ¬vanishingIdeal s ≤ vanishingIdeal t
⊢ s ⊂ t ↔ vanishingIdeal t < vanishingIdeal s

Tactic:
rw [Set.ssubset_def, vanishingIdeal_anti_mono_iff hs, vanishingIdeal_anti_mono_iff ht,
    lt_iff_le_not_ge]

Premises used: Set.ssubset_def, PrimeSpectrum.vanishingIdeal_anti_mono_iff, lt_iff_le_not_ge
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsDomain R
⊢ T1Space.{u} (PrimeSpectrum R) ↔ IsField R

Tactic:
⟨?_, fun h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsDomain R
refine_1 : T1Space.{u} (PrimeSpectrum R) → IsField R
refine_2 : ∀ (h : IsField R), T1Space.{u} (PrimeSpectrum R)
⊢ T1Space.{u} (PrimeSpectrum R) ↔ IsField R

Tactic:
refine ⟨?_, fun h => ?_⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsDomain R
h : T1Space.{u} (PrimeSpectrum R)
⊢ ¬Ne.{u + 1} (α := Ideal R) (asIdeal { asIdeal := ⊥, isPrime := ⋯ }) ⊥

Tactic:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsDomain R
h : T1Space.{u} (PrimeSpectrum R)
⊢ IsField R

Tactic:
exact
      Classical.not_not.1
        (mt
          (Ring.ne_bot_of_isMaximal_of_not_isField <|
            (isClosed_singleton_iff_isMaximal _).1 (T1Space.t1 ⟨⊥, inferInstance⟩))
          (by simp))

Premises used: Classical.not_not, Ring.ne_bot_of_isMaximal_of_not_isField, T1Space.t1, mt, PrimeSpectrum.isClosed_singleton_iff_isMaximal, Iff.mp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsDomain R
h : IsField R
⊢ T1Space.{u} (PrimeSpectrum R)

Tactic:
⟨fun x => (isClosed_singleton_iff_isMaximal x).2 ?_⟩

Premises used: Iff.mpr, PrimeSpectrum.isClosed_singleton_iff_isMaximal, T1Space.mk
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsDomain R
h : IsField R
refine_2 : ∀ (x : PrimeSpectrum R), x.asIdeal.IsMaximal
⊢ T1Space.{u} (PrimeSpectrum R)

Tactic:
refine ⟨fun x => (isClosed_singleton_iff_isMaximal x).2 ?_⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsDomain R
h : IsField R
x : PrimeSpectrum R
pos : ∀ (hx : x.asIdeal = ⊥), x.asIdeal.IsMaximal
neg : ∀ (hx : ¬x.asIdeal = ⊥), x.asIdeal.IsMaximal
⊢ x.asIdeal.IsMaximal

Tactic:
by_cases hx : x.asIdeal = ⊥

Premises used: PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsDomain R
h : IsField R
x : PrimeSpectrum R
hx : x.asIdeal = ⊥
this : Semifield R := h.toSemifield
⊢ x.asIdeal.IsMaximal

Tactic:
hx.symm ▸ Ideal.bot_isMaximal

Premises used: Eq.rec, Ideal.bot_isMaximal, Eq.symm
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsDomain R
h : IsField R
x : PrimeSpectrum R
hx : x.asIdeal = ⊥
this : Semifield R := h.toSemifield
⊢ x.asIdeal.IsMaximal

Tactic:
exact hx.symm ▸ Ideal.bot_isMaximal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsDomain R
h : IsField R
x : PrimeSpectrum R
hx : ¬x.asIdeal = ⊥
⊢ x.asIdeal.IsMaximal

Tactic:
absurd h (Ring.not_isField_iff_exists_prime.2 ⟨x.asIdeal, ⟨hx, x.2⟩⟩)

Premises used: Iff.mpr, PrimeSpectrum.isPrime, absurd, Ring.not_isField_iff_exists_prime, And.intro, Exists.intro, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsDomain R
h : IsField R
x : PrimeSpectrum R
hx : ¬x.asIdeal = ⊥
⊢ x.asIdeal.IsMaximal

Tactic:
exact absurd h (Ring.not_isField_iff_exists_prime.2 ⟨x.asIdeal, ⟨hx, x.2⟩⟩)

Premises used: Iff.mpr, PrimeSpectrum.isPrime, absurd, Ring.not_isField_iff_exists_prime, And.intro, Exists.intro, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsRadical
rw :
  Set.Nonempty (α := PrimeSpectrum R) Z(↑I) ∧ IsPreirreducible (X := PrimeSpectrum R) Z(↑I) ↔
    I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
⊢ IsIrreducible (X := PrimeSpectrum R) Z(↑I) ↔ I.IsPrime

Tactic:
rw [Ideal.isPrime_iff, IsIrreducible]

Premises used: IsIrreducible, Ideal.isPrime_iff
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsRadical
h₁ : Set.Nonempty (α := PrimeSpectrum R) Z(↑I) ↔ I ≠ ⊤
h₂ : IsPreirreducible (X := PrimeSpectrum R) Z(↑I) ↔ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
⊢ Set.Nonempty (α := PrimeSpectrum R) Z(↑I) ∧ IsPreirreducible (X := PrimeSpectrum R) Z(↑I) ↔
    I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I

Tactic:
apply and_congr

Premises used: and_congr
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsRadical
h₁ : Ne (α := Set (PrimeSpectrum R)) Z(↑I) ∅ ↔ I ≠ ⊤
h₂ : ¬Eq (α := Set (PrimeSpectrum R)) Z(↑I) ∅ ↔ I ≠ ⊤
h₃ h₄ : ¬I = ⊤ ↔ I ≠ ⊤
⊢ Set.Nonempty (α := PrimeSpectrum R) Z(↑I) ↔ I ≠ ⊤

Tactic:
rw [Set.nonempty_iff_ne_empty, Ne, zeroLocus_empty_iff_eq_top]

Premises used: Ne, Set.nonempty_iff_ne_empty, PrimeSpectrum.zeroLocus_empty_iff_eq_top
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsRadical
trans :
  IsPreirreducible (X := PrimeSpectrum R) Z(↑I) ↔
    ∀ (x y : Ideal R),
      Subset (α := Set (PrimeSpectrum R)) Z(↑I) (Z(↑x) ∪ Z(↑y)) →
        Subset (α := Set (PrimeSpectrum R)) Z(↑I) Z(↑x) ∨ Subset (α := Set (PrimeSpectrum R)) Z(↑I) Z(↑y)
trans₁ :
  (∀ (x y : Ideal R),
      Subset (α := Set (PrimeSpectrum R)) Z(↑I) (Z(↑x) ∪ Z(↑y)) →
        Subset (α := Set (PrimeSpectrum R)) Z(↑I) Z(↑x) ∨ Subset (α := Set (PrimeSpectrum R)) Z(↑I) Z(↑y)) ↔
    ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
⊢ IsPreirreducible (X := PrimeSpectrum R) Z(↑I) ↔ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I

Tactic:
trans ∀ x y : Ideal R, Z(I) ⊆ Z(x) ∪ Z(y) → Z(I) ⊆ Z(x) ∨ Z(I) ⊆ Z(y)
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsRadical
simp_rw :
  (∀ (z₁ z₂ : Set (PrimeSpectrum R)),
      (∃ (I : Ideal R), z₁ = Z(↑I)) → (∃ (I : Ideal R), z₂ = Z(↑I)) → Z(↑I) ⊆ z₁ ∪ z₂ → Z(↑I) ⊆ z₁ ∨ Z(↑I) ⊆ z₂) ↔
    ∀ (x y : Ideal R),
      Subset (α := Set (PrimeSpectrum R)) Z(↑I) (Z(↑x) ∪ Z(↑y)) →
        Subset (α := Set (PrimeSpectrum R)) Z(↑I) Z(↑x) ∨ Subset (α := Set (PrimeSpectrum R)) Z(↑I) Z(↑y)
⊢ IsPreirreducible (X := PrimeSpectrum R) Z(↑I) ↔
    ∀ (x y : Ideal R),
      Subset (α := Set (PrimeSpectrum R)) Z(↑I) (Z(↑x) ∪ Z(↑y)) →
        Subset (α := Set (PrimeSpectrum R)) Z(↑I) Z(↑x) ∨ Subset (α := Set (PrimeSpectrum R)) Z(↑I) Z(↑y)

Tactic:
simp_rw [isPreirreducible_iff_isClosed_union_isClosed, isClosed_iff_zeroLocus_ideal]

Premises used: isPreirreducible_iff_isClosed_union_isClosed, PrimeSpectrum.isClosed_iff_zeroLocus_ideal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsRadical
mp :
  (∀ (z₁ z₂ : Set (PrimeSpectrum R)),
      (∃ (I : Ideal R), z₁ = Z(↑I)) → (∃ (I : Ideal R), z₂ = Z(↑I)) → Z(↑I) ⊆ z₁ ∪ z₂ → Z(↑I) ⊆ z₁ ∨ Z(↑I) ⊆ z₂) →
    ∀ (x y : Ideal R),
      Subset (α := Set (PrimeSpectrum R)) Z(↑I) (Z(↑x) ∪ Z(↑y)) →
        Subset (α := Set (PrimeSpectrum R)) Z(↑I) Z(↑x) ∨ Subset (α := Set (PrimeSpectrum R)) Z(↑I) Z(↑y)
mpr :
  (∀ (x y : Ideal R),
      Subset (α := Set (PrimeSpectrum R)) Z(↑I) (Z(↑x) ∪ Z(↑y)) →
        Subset (α := Set (PrimeSpectrum R)) Z(↑I) Z(↑x) ∨ Subset (α := Set (PrimeSpectrum R)) Z(↑I) Z(↑y)) →
    ∀ (z₁ z₂ : Set (PrimeSpectrum R)),
      (∃ (I : Ideal R), z₁ = Z(↑I)) → (∃ (I : Ideal R), z₂ = Z(↑I)) → Z(↑I) ⊆ z₁ ∪ z₂ → Z(↑I) ⊆ z₁ ∨ Z(↑I) ⊆ z₂
⊢ (∀ (z₁ z₂ : Set (PrimeSpectrum R)),
      (∃ (I : Ideal R), z₁ = Z(↑I)) → (∃ (I : Ideal R), z₂ = Z(↑I)) → Z(↑I) ⊆ z₁ ∪ z₂ → Z(↑I) ⊆ z₁ ∨ Z(↑I) ⊆ z₂) ↔
    ∀ (x y : Ideal R),
      Subset (α := Set (PrimeSpectrum R)) Z(↑I) (Z(↑x) ∪ Z(↑y)) →
        Subset (α := Set (PrimeSpectrum R)) Z(↑I) Z(↑x) ∨ Subset (α := Set (PrimeSpectrum R)) Z(↑I) Z(↑y)

Tactic:
constructor
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsRadical
h :
  ∀ (z₁ z₂ : Set (PrimeSpectrum R)),
    (∃ (I : Ideal R), z₁ = Z(↑I)) → (∃ (I : Ideal R), z₂ = Z(↑I)) → Z(↑I) ⊆ z₁ ∪ z₂ → Z(↑I) ⊆ z₁ ∨ Z(↑I) ⊆ z₂
x y : Ideal R
⊢ Subset (α := Set (PrimeSpectrum R)) Z(↑I) (Z(↑x) ∪ Z(↑y)) →
    Subset (α := Set (PrimeSpectrum R)) Z(↑I) Z(↑x) ∨ Subset (α := Set (PrimeSpectrum R)) Z(↑I) Z(↑y)

Tactic:
h _ _ ⟨x, rfl⟩ ⟨y, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsRadical
h :
  ∀ (z₁ z₂ : Set (PrimeSpectrum R)),
    (∃ (I : Ideal R), z₁ = Z(↑I)) → (∃ (I : Ideal R), z₂ = Z(↑I)) → Z(↑I) ⊆ z₁ ∪ z₂ → Z(↑I) ⊆ z₁ ∨ Z(↑I) ⊆ z₂
x y : Ideal R
⊢ Subset (α := Set (PrimeSpectrum R)) Z(↑I) (Z(↑x) ∪ Z(↑y)) →
    Subset (α := Set (PrimeSpectrum R)) Z(↑I) Z(↑x) ∨ Subset (α := Set (PrimeSpectrum R)) Z(↑I) Z(↑y)

Tactic:
exact h _ _ ⟨x, rfl⟩ ⟨y, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsRadical
h :
  ∀ (x y : Ideal R),
    Subset (α := Set (PrimeSpectrum R)) Z(↑I) (Z(↑x) ∪ Z(↑y)) →
      Subset (α := Set (PrimeSpectrum R)) Z(↑I) Z(↑x) ∨ Subset (α := Set (PrimeSpectrum R)) Z(↑I) Z(↑y)
x y : Ideal R
⊢ Subset (α := Set (PrimeSpectrum R)) Z(↑I) (Z(↑x) ∪ Z(↑y)) →
    Subset (α := Set (PrimeSpectrum R)) Z(↑I) Z(↑x) ∨ Subset (α := Set (PrimeSpectrum R)) Z(↑I) Z(↑y)

Tactic:
h x y
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsRadical
h :
  ∀ (x y : Ideal R),
    Subset (α := Set (PrimeSpectrum R)) Z(↑I) (Z(↑x) ∪ Z(↑y)) →
      Subset (α := Set (PrimeSpectrum R)) Z(↑I) Z(↑x) ∨ Subset (α := Set (PrimeSpectrum R)) Z(↑I) Z(↑y)
x y : Ideal R
⊢ Subset (α := Set (PrimeSpectrum R)) Z(↑I) (Z(↑x) ∪ Z(↑y)) →
    Subset (α := Set (PrimeSpectrum R)) Z(↑I) Z(↑x) ∨ Subset (α := Set (PrimeSpectrum R)) Z(↑I) Z(↑y)

Tactic:
exact h x y
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsRadical
simp_rw : (∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I) ↔ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
⊢ (∀ (x y : Ideal R),
      Subset (α := Set (PrimeSpectrum R)) Z(↑I) (Z(↑x) ∪ Z(↑y)) →
        Subset (α := Set (PrimeSpectrum R)) Z(↑I) Z(↑x) ∨ Subset (α := Set (PrimeSpectrum R)) Z(↑I) Z(↑y)) ↔
    ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I

Tactic:
simp_rw [← zeroLocus_inf, subset_zeroLocus_iff_le_vanishingIdeal,
        vanishingIdeal_zeroLocus_eq_radical, hI.radical]

Premises used: PrimeSpectrum.vanishingIdeal_zeroLocus_eq_radical, PrimeSpectrum.subset_zeroLocus_iff_le_vanishingIdeal, PrimeSpectrum.zeroLocus_inf, Ideal.IsRadical.radical
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsRadical
mp : (∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I) → ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
mpr : (∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I) → ∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I
⊢ (∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I) ↔ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I

Tactic:
constructor
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsRadical
mp :
  (∀ (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
⊢ (∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I) → ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I

Tactic:
simp_rw [← SetLike.mem_coe, ← Set.singleton_subset_iff, ← Ideal.span_le, ←
          Ideal.span_singleton_mul_span_singleton]

Premises used: Ideal.span_le, Set.singleton_subset_iff, Ideal.span_singleton_mul_span_singleton, SetLike.mem_coe