awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC
Goal:
R : Type u_1
inst : CommRing R
U : Set (PrimeSpectrum R[X])
s : Set R[X]
z : zeroLocus s = Uᶜ
rw : IsOpen.{u_1} (X := PrimeSpectrum R) (⋃ (i : (↑s : Type u_1)), PrimeSpectrum.comap C '' (zeroLocus {(↑i : R[X])})ᶜ)
⊢ IsOpen (PrimeSpectrum.comap C '' U)

Tactic:
rw [← compl_compl U, ← z, ← iUnion_of_singleton_coe s, zeroLocus_iUnion, compl_iInter,
    image_iUnion]

Premises used: Set.compl_iInter, compl_compl, Set.image_iUnion, PrimeSpectrum.zeroLocus_iUnion, Set.iUnion_of_singleton_coe
-- Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC
Goal:
R : Type u_1
inst : CommRing R
U : Set (PrimeSpectrum R[X])
s : Set R[X]
z : zeroLocus s = Uᶜ
simp_rw : IsOpen.{u_1} (X := PrimeSpectrum R) (⋃ (i : (↑s : Type u_1)), imageOfDf (↑i : R[X]))
⊢ IsOpen.{u_1} (X := PrimeSpectrum R) (⋃ (i : (↑s : Type u_1)), PrimeSpectrum.comap C '' (zeroLocus {(↑i : R[X])})ᶜ)

Tactic:
simp_rw [← imageOfDf_eq_comap_C_compl_zeroLocus]

Premises used: AlgebraicGeometry.Polynomial.imageOfDf_eq_comap_C_compl_zeroLocus
-- Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC
Goal:
R : Type u_1
inst : CommRing R
U : Set (PrimeSpectrum R[X])
s : Set R[X]
z : zeroLocus s = Uᶜ
⊢ IsOpen.{u_1} (X := PrimeSpectrum R) (⋃ (i : (↑s : Type u_1)), imageOfDf (↑i : R[X]))

Tactic:
isOpen_iUnion fun f => isOpen_imageOfDf

Premises used: isOpen_iUnion, AlgebraicGeometry.Polynomial.isOpen_imageOfDf
-- Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC
Goal:
R : Type u_1
inst : CommRing R
U : Set (PrimeSpectrum R[X])
s : Set R[X]
z : zeroLocus s = Uᶜ
⊢ IsOpen.{u_1} (X := PrimeSpectrum R) (⋃ (i : (↑s : Type u_1)), imageOfDf (↑i : R[X]))

Tactic:
exact isOpen_iUnion fun f => isOpen_imageOfDf

Premises used: isOpen_iUnion, AlgebraicGeometry.Polynomial.isOpen_imageOfDf
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
simp_rw : ∃ x ∈ s, x.asIdeal.IsMaximal
⊢ ∃ x ∈ s, IsClosed (X := PrimeSpectrum R) {x}

Tactic:
simp_rw [isClosed_singleton_iff_isMaximal]

Premises used: PrimeSpectrum.isClosed_singleton_iff_isMaximal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
obtain : ∀ (I : Ideal R) (hI' : sᶜ = zeroLocus (↑I : Set R)), ∃ x ∈ s, x.asIdeal.IsMaximal
⊢ ∃ x ∈ s, x.asIdeal.IsMaximal

Tactic:
obtain ⟨I, hI'⟩ := (isClosed_iff_zeroLocus_ideal _).mp hs.isClosed_compl

Premises used: PrimeSpectrum.isClosed_iff_zeroLocus_ideal, IsOpen.isClosed_compl, Iff.mp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
I : Ideal R
hI' : sᶜ = zeroLocus (↑I : Set R)
simp_rw : ∃ (x : PrimeSpectrum R), ¬(↑I : Set R) ⊆ (↑x.asIdeal : Set R) ∧ x.asIdeal.IsMaximal
⊢ ∃ x ∈ s, x.asIdeal.IsMaximal

Tactic:
simp_rw [← @Set.notMem_compl_iff _ s, hI', mem_zeroLocus]

Premises used: PrimeSpectrum.mem_zeroLocus, Set.notMem_compl_iff
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
I : Ideal R
hI' : sᶜ = zeroLocus (↑I : Set R)
⊢ s ≠ ∅

Tactic:
have := hs'.ne_empty
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
I : Ideal R
hI' : sᶜ = zeroLocus (↑I : Set R)
this : s ≠ ∅
contrapose! : ∀ (this : ∀ (x : PrimeSpectrum R) (_ : ¬(↑I : Set R) ⊆ (↑x.asIdeal : Set R)), ¬x.asIdeal.IsMaximal), s = ∅
⊢ ∃ (x : PrimeSpectrum R), ¬(↑I : Set R) ⊆ (↑x.asIdeal : Set R) ∧ x.asIdeal.IsMaximal

Tactic:
contrapose! this
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
I : Ideal R
hI' : sᶜ = zeroLocus (↑I : Set R)
this : ∀ (x : PrimeSpectrum R) (_ : ¬(↑I : Set R) ⊆ (↑x.asIdeal : Set R)), ¬x.asIdeal.IsMaximal
⊢ ∀ (x : PrimeSpectrum R), x.asIdeal.IsMaximal → (↑I : Set R) ⊆ (↑x.asIdeal : Set R)

Tactic:
simp_rw [not_imp_not] at this

Premises used: not_imp_not
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
I : Ideal R
hI' : sᶜ = zeroLocus (↑I : Set R)
this : ∀ (x : PrimeSpectrum R), x.asIdeal.IsMaximal → (↑I : Set R) ⊆ (↑x.asIdeal : Set R)
rw : I.jacobson = jacobson ⊥
⊢ s = ∅

Tactic:
rw [← Set.compl_univ, eq_compl_comm, hI', eq_comm, ← zeroLocus_bot,
    zeroLocus_eq_iff, Ideal.radical_eq_jacobson, Ideal.radical_eq_jacobson]

Premises used: Ideal.radical_eq_jacobson, PrimeSpectrum.zeroLocus_eq_iff, Set.compl_univ, eq_comm, PrimeSpectrum.zeroLocus_bot, eq_compl_comm
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
I : Ideal R
hI' : sᶜ = zeroLocus (↑I : Set R)
this : ∀ (x : PrimeSpectrum R), x.asIdeal.IsMaximal → (↑I : Set R) ⊆ (↑x.asIdeal : Set R)
⊢ I.jacobson = jacobson ⊥

Tactic:
le_antisymm (le_sInf ?_) (Ideal.jacobson_mono bot_le)

Premises used: le_antisymm, Ideal.jacobson_mono, le_sInf, bot_le
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
I : Ideal R
hI' : sᶜ = zeroLocus (↑I : Set R)
this : ∀ (x : PrimeSpectrum R), x.asIdeal.IsMaximal → (↑I : Set R) ⊆ (↑x.asIdeal : Set R)
refine : ∀ (b : Ideal R), Membership.mem (γ := Set (Ideal R)) {J : Ideal R | ⊥ ≤ J ∧ J.IsMaximal} b → I.jacobson ≤ b
⊢ I.jacobson = jacobson ⊥

Tactic:
refine le_antisymm (le_sInf ?_) (Ideal.jacobson_mono bot_le)

Premises used: le_antisymm, Ideal.jacobson_mono, le_sInf, bot_le
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
I : Ideal R
hI' : sᶜ = zeroLocus (↑I : Set R)
this : ∀ (x : PrimeSpectrum R), x.asIdeal.IsMaximal → (↑I : Set R) ⊆ (↑x.asIdeal : Set R)
x : Ideal R
hx : x.IsMaximal
⊢ I.jacobson ≤ x

Tactic:
sInf_le ⟨this ⟨x, hx.isPrime⟩ hx, hx⟩

Premises used: PrimeSpectrum.mk, Set.Mem, Ideal.IsMaximal.isPrime, sInf_le, And.intro
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
I : Ideal R
hI' : sᶜ = zeroLocus (↑I : Set R)
this : ∀ (x : PrimeSpectrum R), x.asIdeal.IsMaximal → (↑I : Set R) ⊆ (↑x.asIdeal : Set R)
x : Ideal R
hx : x.IsMaximal
⊢ I.jacobson ≤ x

Tactic:
exact sInf_le ⟨this ⟨x, hx.isPrime⟩ hx, hx⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
rw : ∀ (Z : Set (PrimeSpectrum R)), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints (PrimeSpectrum R)).Nonempty
⊢ JacobsonSpace.{u_1} (PrimeSpectrum R)

Tactic:
rw [jacobsonSpace_iff_locallyClosed]

Premises used: jacobsonSpace_iff_locallyClosed
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
U Z : Set (PrimeSpectrum R)
hU : IsOpen U
hZ : IsClosed Z
hS : (U ∩ Z).Nonempty
⊢ ∃ (I : Ideal R), (zeroLocus (↑I : Set R))ᶜ = U

Tactic:
simp only [← isClosed_compl_iff, isClosed_iff_zeroLocus_ideal, @compl_eq_comm _ U] at hU hZ

Premises used: PrimeSpectrum.isClosed_iff_zeroLocus_ideal, compl_eq_comm, isClosed_compl_iff
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
U Z : Set (PrimeSpectrum R)
hU : IsOpen U
hZ : IsClosed Z
hS : (U ∩ Z).Nonempty
hU₁ : ∃ (I : Ideal R), (zeroLocus (↑I : Set R))ᶜ = U
⊢ ∃ (I : Ideal R), Z = zeroLocus (↑I : Set R)

Tactic:
simp only [← isClosed_compl_iff, isClosed_iff_zeroLocus_ideal, @compl_eq_comm _ U] at hU hZ

Premises used: PrimeSpectrum.isClosed_iff_zeroLocus_ideal, compl_eq_comm, isClosed_compl_iff
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
U Z : Set (PrimeSpectrum R)
hS : (U ∩ Z).Nonempty
hU : ∃ (I : Ideal R), (zeroLocus (↑I : Set R))ᶜ = U
hZ : ∃ (I : Ideal R), Z = zeroLocus (↑I : Set R)
obtain :
  ∀ (I : Ideal R)
    (hU : ∃ (I_1 : Ideal R), Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I_1 : Set R))ᶜ (zeroLocus (↑I : Set R))ᶜ)
    (J : Ideal R)
    (hZ : ∃ (I : Ideal R), Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑J : Set R)) (zeroLocus (↑I : Set R)))
    (hS : Set.Nonempty (α := PrimeSpectrum R) ((zeroLocus (↑I : Set R))ᶜ ∩ zeroLocus (↑J : Set R))),
    Set.Nonempty (α := PrimeSpectrum R)
      ((zeroLocus (↑I : Set R))ᶜ ∩ zeroLocus (↑J : Set R) ∩ closedPoints (PrimeSpectrum R))
⊢ (U ∩ Z ∩ closedPoints (PrimeSpectrum R)).Nonempty

Tactic:
obtain ⟨⟨I, rfl⟩, ⟨J, rfl⟩⟩ := And.intro hU hZ

Premises used: And.intro, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
I : Ideal R
hU : ∃ (I_1 : Ideal R), Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I_1 : Set R))ᶜ (zeroLocus (↑I : Set R))ᶜ
J : Ideal R
hZ : ∃ (I : Ideal R), Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑J : Set R)) (zeroLocus (↑I : Set R))
hS : Set.Nonempty (α := PrimeSpectrum R) ((zeroLocus (↑I : Set R))ᶜ ∩ zeroLocus (↑J : Set R))
simp :
  ∀ (hS : ¬∀ (b : Ideal R), Membership.mem (γ := Set (Ideal R)) {J_1 : Ideal R | J ≤ J_1 ∧ J_1.IsMaximal} b → I ≤ b),
    ¬Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑J : Set R) ∩ closedPoints (PrimeSpectrum R))
        (zeroLocus (↑I : Set R))
⊢ Set.Nonempty (α := PrimeSpectrum R)
    ((zeroLocus (↑I : Set R))ᶜ ∩ zeroLocus (↑J : Set R) ∩ closedPoints (PrimeSpectrum R))

Tactic:
simp only [Set.nonempty_iff_ne_empty, ne_eq, Set.inter_assoc,
    ← Set.disjoint_iff_inter_eq_empty, Set.disjoint_compl_left_iff_subset,
    zeroLocus_subset_zeroLocus_iff, Ideal.radical_eq_jacobson, Ideal.jacobson, le_sInf_iff] at hS ⊢

Premises used: Set.disjoint_compl_left_iff_subset, le_sInf_iff, PrimeSpectrum.zeroLocus_subset_zeroLocus_iff, Ideal.jacobson, Ideal.radical_eq_jacobson, ne_eq, Set.disjoint_iff_inter_eq_empty, Set.nonempty_iff_ne_empty, Set.inter_assoc
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
I : Ideal R
hU : ∃ (I_1 : Ideal R), Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I_1 : Set R))ᶜ (zeroLocus (↑I : Set R))ᶜ
J : Ideal R
hZ : ∃ (I : Ideal R), Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑J : Set R)) (zeroLocus (↑I : Set R))
hS : ¬∀ (b : Ideal R), Membership.mem (γ := Set (Ideal R)) {J_1 : Ideal R | J ≤ J_1 ∧ J_1.IsMaximal} b → I ≤ b
contrapose :
  ∀
    (hS :
      Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑J : Set R) ∩ closedPoints (PrimeSpectrum R))
        (zeroLocus (↑I : Set R)))
    (b : Ideal R), Membership.mem (γ := Set (Ideal R)) {J_1 : Ideal R | J ≤ J_1 ∧ J_1.IsMaximal} b → I ≤ b
⊢ ¬Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑J : Set R) ∩ closedPoints (PrimeSpectrum R))
      (zeroLocus (↑I : Set R))

Tactic:
contrapose hS
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
I : Ideal R
hU : ∃ (I_1 : Ideal R), Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I_1 : Set R))ᶜ (zeroLocus (↑I : Set R))ᶜ
J : Ideal R
hZ : ∃ (I : Ideal R), Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑J : Set R)) (zeroLocus (↑I : Set R))
hS :
  Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑J : Set R) ∩ closedPoints (PrimeSpectrum R)) (zeroLocus (↑I : Set R))
x : Ideal R
hJx : J ≤ x
hx : x.IsMaximal
⊢ I ≤ x

Tactic:
@hS ⟨x, hx.isPrime⟩ ⟨hJx, (isClosed_singleton_iff_isMaximal _).mpr hx⟩

Premises used: Iff.mpr, PrimeSpectrum.zeroLocus, Set.Mem, setOf, PrimeSpectrum.isClosed_singleton_iff_isMaximal, Set.Subset, And.intro
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
I : Ideal R
hU : ∃ (I_1 : Ideal R), Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I_1 : Set R))ᶜ (zeroLocus (↑I : Set R))ᶜ
J : Ideal R
hZ : ∃ (I : Ideal R), Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑J : Set R)) (zeroLocus (↑I : Set R))
hS :
  Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑J : Set R) ∩ closedPoints (PrimeSpectrum R)) (zeroLocus (↑I : Set R))
x : Ideal R
hJx : J ≤ x
hx : x.IsMaximal
⊢ I ≤ x

Tactic:
exact @hS ⟨x, hx.isPrime⟩ ⟨hJx, (isClosed_singleton_iff_isMaximal _).mpr hx⟩

Premises used: Iff.mpr, PrimeSpectrum.isClosed_singleton_iff_isMaximal, And.intro
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
⊢ IsJacobsonRing R ↔ JacobsonSpace.{u_1} (PrimeSpectrum R)

Tactic:
⟨fun _ ↦ inferInstance, fun H ↦ ⟨fun I hI ↦ le_antisymm ?_ Ideal.le_jacobson⟩⟩

Premises used: inferInstance, le_antisymm, Iff.intro, IsJacobsonRing.mk, Ideal.le_jacobson
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
refine : ∀ (H : JacobsonSpace.{u_1} (PrimeSpectrum R)) (I : Ideal R) (hI : I.IsRadical), I.jacobson ≤ I
⊢ IsJacobsonRing R ↔ JacobsonSpace.{u_1} (PrimeSpectrum R)

Tactic:
refine ⟨fun _ ↦ inferInstance, fun H ↦ ⟨fun I hI ↦ le_antisymm ?_ Ideal.le_jacobson⟩⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
H : JacobsonSpace.{u_1} (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
rw : I.jacobson.radical ≤ I
⊢ I.jacobson ≤ I

Tactic:
rw [← I.isRadical_jacobson.radical]

Premises used: Ideal.isRadical_jacobson, Ideal.IsRadical.radical
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
H : JacobsonSpace.{u_1} (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
rw : I.radical
| I

Tactic:
rw [← hI.radical]

Premises used: Ideal.IsRadical.radical
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
H : JacobsonSpace.{u_1} (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
conv_rhs : I.jacobson.radical ≤ I.radical
⊢ I.jacobson.radical ≤ I

Tactic:
conv_rhs => rw [← hI.radical]

Premises used: Ideal.IsRadical.radical
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
H : JacobsonSpace.{u_1} (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
simp_rw :
  LE.le (α := Ideal R) (vanishingIdeal (zeroLocus (↑I.jacobson : Set R)) : Ideal R)
    (vanishingIdeal (zeroLocus (↑I : Set R)))
⊢ I.jacobson.radical ≤ I.radical

Tactic:
simp_rw [← vanishingIdeal_zeroLocus_eq_radical]

Premises used: PrimeSpectrum.vanishingIdeal_zeroLocus_eq_radical
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
H : JacobsonSpace.{u_1} (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
h : Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus (↑I.jacobson : Set R))
⊢ LE.le (α := Ideal R) (vanishingIdeal (zeroLocus (↑I.jacobson : Set R)) : Ideal R)
    (vanishingIdeal (zeroLocus (↑I : Set R)))

Tactic:
apply vanishingIdeal_anti_mono

Premises used: PrimeSpectrum.vanishingIdeal_anti_mono
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
H : JacobsonSpace.{u_1} (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
h :
  Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R) ∩ closedPoints (PrimeSpectrum R))
    (zeroLocus (↑I.jacobson : Set R))
⊢ Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus (↑I.jacobson : Set R))

Tactic:
rw [← H.1 (isClosed_zeroLocus I), (isClosed_zeroLocus _).closure_subset_iff]

Premises used: PrimeSpectrum.isClosed_zeroLocus, JacobsonSpace.closure_inter_closedPoints, IsClosed.closure_subset_iff
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
H : JacobsonSpace.{u_1} (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
x : PrimeSpectrum R
hx : I ≤ x.asIdeal
hx' : Membership.mem (γ := Set (PrimeSpectrum R)) (closedPoints (PrimeSpectrum R)) x
h : I.jacobson ≤ x.asIdeal
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I.jacobson : Set R)) x

Tactic:
change jacobson I ≤ x.asIdeal

Premises used: Ideal.jacobson, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
H : JacobsonSpace.{u_1} (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
x : PrimeSpectrum R
hx : I ≤ x.asIdeal
hx' : Membership.mem (γ := Set (PrimeSpectrum R)) (closedPoints (PrimeSpectrum R)) x
⊢ I.jacobson ≤ x.asIdeal

Tactic:
sInf_le ⟨hx, (isClosed_singleton_iff_isMaximal _).mp hx'⟩

Premises used: Set.Mem, PrimeSpectrum.isClosed_singleton_iff_isMaximal, sInf_le, And.intro, Iff.mp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
H : JacobsonSpace.{u_1} (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
x : PrimeSpectrum R
hx : I ≤ x.asIdeal
hx' : Membership.mem (γ := Set (PrimeSpectrum R)) (closedPoints (PrimeSpectrum R)) x
⊢ I.jacobson ≤ x.asIdeal

Tactic:
exact sInf_le ⟨hx, (isClosed_singleton_iff_isMaximal _).mp hx'⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsJacobsonRing R
x : PrimeSpectrum R
⊢ IsOpen (X := PrimeSpectrum R) {x}

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsJacobsonRing R
x : PrimeSpectrum R
⊢ IsClopen (X := PrimeSpectrum R) {x}

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsJacobsonRing R
x : PrimeSpectrum R
⊢ ∀ (a : IsOpen (X := PrimeSpectrum R) {x}), IsClopen (X := PrimeSpectrum R) {x}

Tactic:
1 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsJacobsonRing R
x : PrimeSpectrum R
h_1 : IsOpen (X := PrimeSpectrum R) {x}
h : IsOpen (X := PrimeSpectrum R) {x} := h_1
obtain :
  ∀ (y : PrimeSpectrum R) (h' : IsClosed (X := PrimeSpectrum R) {y}),
    IsOpen (X := PrimeSpectrum R) {y} → IsClopen (X := PrimeSpectrum R) {y}
⊢ IsClopen (X := PrimeSpectrum R) {x}

Tactic:
obtain ⟨y, rfl : y = x, h'⟩ := exists_isClosed_singleton_of_isJacobsonRing _ h
      ⟨x, Set.mem_singleton x⟩

Premises used: Set.mem_singleton, PrimeSpectrum.exists_isClosed_singleton_of_isJacobsonRing, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsJacobsonRing R
y : PrimeSpectrum R
h' : IsClosed (X := PrimeSpectrum R) {y}
h_1 : IsOpen (X := PrimeSpectrum R) {y}
h : IsOpen (X := PrimeSpectrum R) {y} := h_1
⊢ IsClopen (X := PrimeSpectrum R) {y}

Tactic:
⟨h', h⟩

Premises used: And.intro, IsClopen
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsJacobsonRing R
y : PrimeSpectrum R
h' : IsClosed (X := PrimeSpectrum R) {y}
h_1 : IsOpen (X := PrimeSpectrum R) {y}
h : IsOpen (X := PrimeSpectrum R) {y} := h_1
⊢ IsClopen (X := PrimeSpectrum R) {y}

Tactic:
exact ⟨h', h⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsJacobsonRing R
x : PrimeSpectrum R
⊢ ∀ (a : IsOpen (X := PrimeSpectrum R) {x}), IsClopen (X := PrimeSpectrum R) {x}

Tactic:
tfae_have 1 → 2
  | h => by
    obtain ⟨y, rfl : y = x, h'⟩ := exists_isClosed_singleton_of_isJacobsonRing _ h
      ⟨x, Set.mem_singleton x⟩
    exact ⟨h', h⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsJacobsonRing R
x : PrimeSpectrum R
tfae_1_to_2 : ∀ (a : IsOpen (X := PrimeSpectrum R) {x}), IsClopen (X := PrimeSpectrum R) {x}
⊢ IsClopen (X := PrimeSpectrum R) {x}

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsJacobsonRing R
x : PrimeSpectrum R
tfae_1_to_2 : ∀ (a : IsOpen (X := PrimeSpectrum R) {x}), IsClopen (X := PrimeSpectrum R) {x}
⊢ IsClosed (X := PrimeSpectrum R) {x} ∧ StableUnderGeneralization (X := PrimeSpectrum R) {x}

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsJacobsonRing R
x : PrimeSpectrum R
tfae_1_to_2 : ∀ (a : IsOpen (X := PrimeSpectrum R) {x}), IsClopen (X := PrimeSpectrum R) {x}
⊢ ∀ (a : IsClopen (X := PrimeSpectrum R) {x}),
    IsClosed (X := PrimeSpectrum R) {x} ∧ StableUnderGeneralization (X := PrimeSpectrum R) {x}

Tactic:
2 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsJacobsonRing R
x : PrimeSpectrum R
tfae_1_to_2 : ∀ (a : IsOpen (X := PrimeSpectrum R) {x}), IsClopen (X := PrimeSpectrum R) {x}
⊢ ∀ (a : IsClopen (X := PrimeSpectrum R) {x}),
    IsClosed (X := PrimeSpectrum R) {x} ∧ StableUnderGeneralization (X := PrimeSpectrum R) {x}

Tactic:
tfae_have 2 → 3
  | h => ⟨h.isClosed, h.isOpen.stableUnderGeneralization⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsJacobsonRing R
x : PrimeSpectrum R
tfae_1_to_2 : ∀ (a : IsOpen (X := PrimeSpectrum R) {x}), IsClopen (X := PrimeSpectrum R) {x}
tfae_2_to_3 :
  ∀ (a : IsClopen (X := PrimeSpectrum R) {x}),
    IsClosed (X := PrimeSpectrum R) {x} ∧ StableUnderGeneralization (X := PrimeSpectrum R) {x}
⊢ IsClosed (X := PrimeSpectrum R) {x} ∧ StableUnderGeneralization (X := PrimeSpectrum R) {x}

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsJacobsonRing R
x : PrimeSpectrum R
tfae_1_to_2 : ∀ (a : IsOpen (X := PrimeSpectrum R) {x}), IsClopen (X := PrimeSpectrum R) {x}
tfae_2_to_3 :
  ∀ (a : IsClopen (X := PrimeSpectrum R) {x}),
    IsClosed (X := PrimeSpectrum R) {x} ∧ StableUnderGeneralization (X := PrimeSpectrum R) {x}
⊢ IsOpen (X := PrimeSpectrum R) {x}

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsJacobsonRing R
x : PrimeSpectrum R
tfae_1_to_2 : ∀ (a : IsOpen (X := PrimeSpectrum R) {x}), IsClopen (X := PrimeSpectrum R) {x}
tfae_2_to_3 :
  ∀ (a : IsClopen (X := PrimeSpectrum R) {x}),
    IsClosed (X := PrimeSpectrum R) {x} ∧ StableUnderGeneralization (X := PrimeSpectrum R) {x}
⊢ ∀ (a : IsClosed (X := PrimeSpectrum R) {x} ∧ StableUnderGeneralization (X := PrimeSpectrum R) {x}),
    IsOpen (X := PrimeSpectrum R) {x}

Tactic:
3 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsJacobsonRing R
x : PrimeSpectrum R
tfae_1_to_2 : ∀ (a : IsOpen (X := PrimeSpectrum R) {x}), IsClopen (X := PrimeSpectrum R) {x}
tfae_2_to_3 :
  ∀ (a : IsClopen (X := PrimeSpectrum R) {x}),
    IsClosed (X := PrimeSpectrum R) {x} ∧ StableUnderGeneralization (X := PrimeSpectrum R) {x}
h₁ : IsClosed (X := PrimeSpectrum R) {x}
h₂ : StableUnderGeneralization (X := PrimeSpectrum R) {x}
⊢ IsMax x

Tactic:
rw [isClosed_singleton_iff_isMaximal, ← isMax_iff] at h₁

Premises used: PrimeSpectrum.isMax_iff, PrimeSpectrum.isClosed_singleton_iff_isMaximal