awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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}
h₃ : IsMax x
⊢ StableUnderGeneralization (X := PrimeSpectrum R) {x}

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

Premises used: PrimeSpectrum.isMax_iff, PrimeSpectrum.isClosed_singleton_iff_isMaximal
-- 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₁ : IsMax x
h₂ : StableUnderGeneralization (X := PrimeSpectrum R) {x}
this :
  Eq (α := Set (PrimeSpectrum R)) {x}
    (⋃ (p : PrimeSpectrum R),
        ⋃ (_ : Membership.mem (γ := Set (PrimeSpectrum R)) {p : PrimeSpectrum R | IsMin p ∧ p ≠ x} p), closure {p})ᶜ
rw :
  IsClosed.{u_1} (X := PrimeSpectrum R)
    (⋃ (p : PrimeSpectrum R),
      ⋃ (_ : Membership.mem (γ := Set (PrimeSpectrum R)) {p : PrimeSpectrum R | IsMin p ∧ p ≠ x} p), closure {p})
⊢ IsOpen (X := PrimeSpectrum R) {x}

Tactic:
rw [this, isOpen_compl_iff]

Premises used: isOpen_compl_iff
-- 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₁ : IsMax x
h₂ : StableUnderGeneralization (X := PrimeSpectrum R) {x}
this :
  Eq (α := Set (PrimeSpectrum R)) {x}
    (⋃ (p : PrimeSpectrum R),
        ⋃ (_ : Membership.mem (γ := Set (PrimeSpectrum R)) {p : PrimeSpectrum R | IsMin p ∧ p ≠ x} p), closure {p})ᶜ
⊢ IsClosed.{u_1} (X := PrimeSpectrum R)
    (⋃ (p : PrimeSpectrum R),
      ⋃ (_ : Membership.mem (γ := Set (PrimeSpectrum R)) {p : PrimeSpectrum R | IsMin p ∧ p ≠ x} p), closure {p})

Tactic:
Set.Finite.isClosed_biUnion ?_ (fun _ _ ↦ isClosed_closure)

Premises used: isClosed_closure, Set.Finite.isClosed_biUnion
-- 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₁ : IsMax x
h₂ : StableUnderGeneralization (X := PrimeSpectrum R) {x}
this :
  Eq (α := Set (PrimeSpectrum R)) {x}
    (⋃ (p : PrimeSpectrum R),
        ⋃ (_ : Membership.mem (γ := Set (PrimeSpectrum R)) {p : PrimeSpectrum R | IsMin p ∧ p ≠ x} p), closure {p})ᶜ
refine : Set.Finite.{u_1} (α := PrimeSpectrum R) {p : PrimeSpectrum R | IsMin p ∧ p ≠ x}
⊢ IsClosed.{u_1} (X := PrimeSpectrum R)
    (⋃ (p : PrimeSpectrum R),
      ⋃ (_ : Membership.mem (γ := Set (PrimeSpectrum R)) {p : PrimeSpectrum R | IsMin p ∧ p ≠ x} p), closure {p})

Tactic:
refine Set.Finite.isClosed_biUnion ?_ (fun _ _ ↦ isClosed_closure)

Premises used: isClosed_closure, Set.Finite.isClosed_biUnion
-- 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₁ : IsMax x
h₂ : StableUnderGeneralization (X := PrimeSpectrum R) {x}
this :
  Eq (α := Set (PrimeSpectrum R)) {x}
    (⋃ (p : PrimeSpectrum R),
        ⋃ (_ : Membership.mem (γ := Set (PrimeSpectrum R)) {p : PrimeSpectrum R | IsMin p ∧ p ≠ x} p), closure {p})ᶜ
⊢ Set.Finite.{u_1} (α := PrimeSpectrum R) {p : PrimeSpectrum R | IsMin p ∧ p ≠ x}

Tactic:
(finite_setOf_isMin R).subset fun x h ↦ h.1

Premises used: Set.Finite.subset, PrimeSpectrum.finite_setOf_isMin, And.left
-- 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₁ : IsMax x
h₂ : StableUnderGeneralization (X := PrimeSpectrum R) {x}
this :
  Eq (α := Set (PrimeSpectrum R)) {x}
    (⋃ (p : PrimeSpectrum R),
        ⋃ (_ : Membership.mem (γ := Set (PrimeSpectrum R)) {p : PrimeSpectrum R | IsMin p ∧ p ≠ x} p), closure {p})ᶜ
⊢ Set.Finite.{u_1} (α := PrimeSpectrum R) {p : PrimeSpectrum R | IsMin p ∧ p ≠ x}

Tactic:
exact (finite_setOf_isMin R).subset fun x h ↦ h.1

Premises used: Set.Finite.subset, PrimeSpectrum.finite_setOf_isMin
-- 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₁ : IsMax x
h₂ : StableUnderGeneralization (X := PrimeSpectrum R) {x}
suffices :
  Eq (α := Set (PrimeSpectrum R)) {x}
    (⋃ (p : PrimeSpectrum R),
        ⋃ (_ : Membership.mem (γ := Set (PrimeSpectrum R)) {p : PrimeSpectrum R | IsMin p ∧ p ≠ x} p), closure {p})ᶜ
⊢ IsOpen (X := PrimeSpectrum R) {x}

Tactic:
suffices {x} = (⋃ p ∈ { p : PrimeSpectrum R | IsMin p ∧ p ≠ x }, closure {p})ᶜ by
      rw [this, isOpen_compl_iff]
      refine Set.Finite.isClosed_biUnion ?_ (fun _ _ ↦ isClosed_closure)
      exact (finite_setOf_isMin R).subset fun x h ↦ h.1
-- 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₁ : IsMax x
h₂ : StableUnderGeneralization (X := PrimeSpectrum R) {x}
h :
  ∀ (p : PrimeSpectrum R),
    Membership.mem (γ := Set (PrimeSpectrum R)) {x} p ↔
      Membership.mem (γ := Set (PrimeSpectrum R))
        (⋃ (p : PrimeSpectrum R),
            ⋃ (_ : Membership.mem (γ := Set (PrimeSpectrum R)) {p : PrimeSpectrum R | IsMin p ∧ p ≠ x} p), closure {p})ᶜ
        p
⊢ Eq (α := Set (PrimeSpectrum R)) {x}
    (⋃ (p : PrimeSpectrum R),
        ⋃ (_ : Membership.mem (γ := Set (PrimeSpectrum R)) {p : PrimeSpectrum R | IsMin p ∧ p ≠ x} p), closure {p})ᶜ

Tactic:
ext p
-- 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₁ : IsMax x
h₂ : StableUnderGeneralization (X := PrimeSpectrum R) {x}
p : PrimeSpectrum R
h : p = x ↔ ∀ (i : PrimeSpectrum R), IsMin i → i ≤ p → i = x
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) {x} p ↔
    Membership.mem (γ := Set (PrimeSpectrum R))
      (⋃ (p : PrimeSpectrum R),
          ⋃ (_ : Membership.mem (γ := Set (PrimeSpectrum R)) {p : PrimeSpectrum R | IsMin p ∧ p ≠ x} p), closure {p})ᶜ
      p

Tactic:
simp only [Set.mem_singleton_iff, ne_eq, Set.mem_setOf_eq, Set.compl_iUnion, Set.mem_iInter,
      Set.mem_compl_iff, and_imp, ← specializes_iff_mem_closure, ← le_iff_specializes,
      not_imp_not]

Premises used: and_imp, specializes_iff_mem_closure, Set.mem_setOf_eq, Set.mem_iInter, ne_eq, Set.compl_iUnion, Set.mem_singleton_iff, PrimeSpectrum.le_iff_specializes, Set.mem_compl_iff, not_imp_not
-- 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₁ : IsMax x
h₂ : StableUnderGeneralization (X := PrimeSpectrum R) {x}
p : PrimeSpectrum R
h : p = x → ∀ (i : PrimeSpectrum R), IsMin i → i ≤ p → i = x
h₃ : (∀ (i : PrimeSpectrum R), IsMin i → i ≤ p → i = x) → p = x
⊢ p = x ↔ ∀ (i : PrimeSpectrum R), IsMin i → i ≤ p → i = x

Tactic:
constructor
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsJacobsonRing R
p : PrimeSpectrum R
tfae_1_to_2 : ∀ (a : IsOpen (X := PrimeSpectrum R) {p}), IsClopen (X := PrimeSpectrum R) {p}
tfae_2_to_3 :
  ∀ (a : IsClopen (X := PrimeSpectrum R) {p}),
    IsClosed (X := PrimeSpectrum R) {p} ∧ StableUnderGeneralization (X := PrimeSpectrum R) {p}
h₁ : IsMax p
h₂ : StableUnderGeneralization (X := PrimeSpectrum R) {p}
i : PrimeSpectrum R
h_1 : IsMin i
h : ∀ (h₂ : IsMin p) (i : PrimeSpectrum R), IsMin i → i ≤ p → i = p
⊢ i ≤ p → i = p

Tactic:
rw [stableUnderGeneralization_singleton, ← isMin_iff] at h₂

Premises used: PrimeSpectrum.isMin_iff, PrimeSpectrum.stableUnderGeneralization_singleton
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsJacobsonRing R
p : PrimeSpectrum R
tfae_1_to_2 : ∀ (a : IsOpen (X := PrimeSpectrum R) {p}), IsClopen (X := PrimeSpectrum R) {p}
tfae_2_to_3 :
  ∀ (a : IsClopen (X := PrimeSpectrum R) {p}),
    IsClosed (X := PrimeSpectrum R) {p} ∧ StableUnderGeneralization (X := PrimeSpectrum R) {p}
h₁ : IsMax p
h₂ : IsMin p
i : PrimeSpectrum R
h : IsMin i
⊢ i ≤ p → i = p

Tactic:
h₂.eq_of_le

Premises used: IsMin.eq_of_le
-- Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsJacobsonRing R
p : PrimeSpectrum R
tfae_1_to_2 : ∀ (a : IsOpen (X := PrimeSpectrum R) {p}), IsClopen (X := PrimeSpectrum R) {p}
tfae_2_to_3 :
  ∀ (a : IsClopen (X := PrimeSpectrum R) {p}),
    IsClosed (X := PrimeSpectrum R) {p} ∧ StableUnderGeneralization (X := PrimeSpectrum R) {p}
h₁ : IsMax p
h₂ : IsMin p
i : PrimeSpectrum R
h : IsMin i
⊢ i ≤ p → i = p

Tactic:
exact h₂.eq_of_le

Premises used: IsMin.eq_of_le
-- 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₁ : IsMax x
h₂ : StableUnderGeneralization (X := PrimeSpectrum R) {x}
p : PrimeSpectrum R
hp : ∀ (i : PrimeSpectrum R), IsMin i → i ≤ p → i = x
h : x ≤ p
⊢ p = x

Tactic:
apply h₁.eq_of_ge

Premises used: IsMax.eq_of_ge
-- 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₁ : IsMax x
h₂ : StableUnderGeneralization (X := PrimeSpectrum R) {x}
p : PrimeSpectrum R
hp : ∀ (i : PrimeSpectrum R), IsMin i → i ≤ p → i = x
h : ∀ (q : Ideal R) (hq : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊥) q) (hq' : q ≤ p.asIdeal), x ≤ p
⊢ x ≤ p

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.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₁ : IsMax x
h₂ : StableUnderGeneralization (X := PrimeSpectrum R) {x}
p : PrimeSpectrum R
hp : ∀ (i : PrimeSpectrum R), IsMin i → i ≤ p → i = x
q : Ideal R
hq : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊥) q
hq' : q ≤ p.asIdeal
⊢ x ≤ p

Tactic:
(hp ⟨q, hq.1.1⟩ (isMin_iff.mpr hq) hq').ge.trans hq'

Premises used: Iff.mpr, PrimeSpectrum.mk, Eq.ge, PrimeSpectrum.isMin_iff, And.left, LE.le.trans
-- 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₁ : IsMax x
h₂ : StableUnderGeneralization (X := PrimeSpectrum R) {x}
p : PrimeSpectrum R
hp : ∀ (i : PrimeSpectrum R), IsMin i → i ≤ p → i = x
q : Ideal R
hq : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊥) q
hq' : q ≤ p.asIdeal
⊢ x ≤ p

Tactic:
exact (hp ⟨q, hq.1.1⟩ (isMin_iff.mpr hq) hq').ge.trans hq'

Premises used: Iff.mpr, PrimeSpectrum.mk, Eq.ge, PrimeSpectrum.isMin_iff, And.left, LE.le.trans
-- 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:
tfae_have 3 → 1
  | ⟨h₁, h₂⟩ => by
    rw [isClosed_singleton_iff_isMaximal, ← isMax_iff] at h₁
    suffices {x} = (⋃ p ∈ { p : PrimeSpectrum R | IsMin p ∧ p ≠ x }, closure {p})ᶜ by
      rw [this, isOpen_compl_iff]
      refine Set.Finite.isClosed_biUnion ?_ (fun _ _ ↦ isClosed_closure)
      exact (finite_setOf_isMin R).subset fun x h ↦ h.1
    ext p
    simp only [Set.mem_singleton_iff, ne_eq, Set.mem_setOf_eq, Set.compl_iUnion, Set.mem_iInter,
      Set.mem_compl_iff, and_imp, ← specializes_iff_mem_closure, ← le_iff_specializes,
      not_imp_not]
    constructor
    · rintro rfl _ _
      rw [stableUnderGeneralization_singleton, ← isMin_iff] at h₂
      exact h₂.eq_of_le
    · intro hp
      apply h₁.eq_of_ge
      obtain ⟨q, hq, hq'⟩ := Ideal.exists_minimalPrimes_le (J := p.asIdeal) bot_le
      exact (hp ⟨q, hq.1.1⟩ (isMin_iff.mpr hq) hq').ge.trans hq'
-- 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}
tfae_3_to_1 :
  ∀ (a : IsClosed (X := PrimeSpectrum R) {x} ∧ StableUnderGeneralization (X := PrimeSpectrum R) {x}),
    IsOpen (X := PrimeSpectrum R) {x}
⊢ [IsOpen (X := PrimeSpectrum R) {x}, IsClopen (X := PrimeSpectrum R) {x},
      IsClosed (X := PrimeSpectrum R) {x} ∧ StableUnderGeneralization (X := PrimeSpectrum R) {x}].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : Membership.mem (γ := Ideal R) 𝔪 x
pos : ∀ (hn : x ∈ p₀.asIdeal), ∃ (q : PrimeSpectrum R), x ∈ q.asIdeal ∧ p₀ < q ∧ q.asIdeal < 𝔪
neg : ∀ (hn : x ∉ p₀.asIdeal), ∃ (q : PrimeSpectrum R), x ∈ q.asIdeal ∧ p₀ < q ∧ q.asIdeal < 𝔪
⊢ ∃ (q : PrimeSpectrum R), x ∈ q.asIdeal ∧ p₀ < q ∧ q.asIdeal < 𝔪

Tactic:
by_cases hn : x ∈ p₀.1

Premises used: PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : Membership.mem (γ := Ideal R) 𝔪 x
hn : x ∈ p₀.asIdeal
⊢ ∃ (q : PrimeSpectrum R), x ∈ q.asIdeal ∧ p₀ < q ∧ q.asIdeal < 𝔪

Tactic:
⟨p₁, h₀.le hn, h₀, h₁⟩

Premises used: LT.lt.le, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : Membership.mem (γ := Ideal R) 𝔪 x
hn : x ∈ p₀.asIdeal
⊢ ∃ (q : PrimeSpectrum R), x ∈ q.asIdeal ∧ p₀ < q ∧ q.asIdeal < 𝔪

Tactic:
exact ⟨p₁, h₀.le hn, h₀, h₁⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : Membership.mem (γ := Ideal R) 𝔪 x
hn : x ∉ p₀.asIdeal
e : (↑(zeroLocus (↑p₀.asIdeal : Set R)) : Type u_1) ≃o PrimeSpectrum (R ⧸ p₀.asIdeal) :=
  p₀.asIdeal.primeSpectrumQuotientOrderIsoZeroLocus.symm
neg :
  ∀ (q : Ideal R) (hq : q ∈ (p₀.asIdeal + span {x}).minimalPrimes),
    ∃ (q : PrimeSpectrum R), x ∈ q.asIdeal ∧ p₀ < q ∧ q.asIdeal < 𝔪
⊢ ∃ (q : PrimeSpectrum R), x ∈ q.asIdeal ∧ p₀ < q ∧ q.asIdeal < 𝔪

Tactic:
obtain ⟨q, hq⟩ := (p₀.1 + span {x}).nonempty_minimalPrimes <|
    sup_le (IsLocalRing.le_maximalIdeal_of_isPrime p₀.1) ((span_singleton_le_iff_mem 𝔪).mpr hx)
      |>.trans_lt (IsMaximal.isPrime' 𝔪).1.lt_top |>.ne

Premises used: Ideal.nonempty_minimalPrimes
-- Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : Membership.mem (γ := Ideal R) 𝔪 x
hn : x ∉ p₀.asIdeal
e : (↑(zeroLocus (↑p₀.asIdeal : Set R)) : Type u_1) ≃o PrimeSpectrum (R ⧸ p₀.asIdeal) :=
  p₀.asIdeal.primeSpectrumQuotientOrderIsoZeroLocus.symm
q_1 : Ideal R
hq : q_1 ∈ (p₀.asIdeal + span {x}).minimalPrimes
q : PrimeSpectrum R := { asIdeal := q_1, isPrime := ⋯ }
⊢ q.asIdeal.IsPrime

Tactic:
have : q.1.IsPrime := q.2
-- Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : Membership.mem (γ := Ideal R) 𝔪 x
hn : x ∉ p₀.asIdeal
e : (↑(zeroLocus (↑p₀.asIdeal : Set R)) : Type u_1) ≃o PrimeSpectrum (R ⧸ p₀.asIdeal) :=
  p₀.asIdeal.primeSpectrumQuotientOrderIsoZeroLocus.symm
q_1 : Ideal R
hq : q_1 ∈ (p₀.asIdeal + span {x}).minimalPrimes
q : PrimeSpectrum R := { asIdeal := q_1, isPrime := ⋯ }
this : q.asIdeal.IsPrime
⊢ x ∈ q.asIdeal

Tactic:
have hxq : x ∈ q.1 := le_sup_right.trans hq.1.2 (mem_span_singleton_self x)
-- Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : Membership.mem (γ := Ideal R) 𝔪 x
hn : x ∉ p₀.asIdeal
e : (↑(zeroLocus (↑p₀.asIdeal : Set R)) : Type u_1) ≃o PrimeSpectrum (R ⧸ p₀.asIdeal) :=
  p₀.asIdeal.primeSpectrumQuotientOrderIsoZeroLocus.symm
q_1 : Ideal R
hq : q_1 ∈ (p₀.asIdeal + span {x}).minimalPrimes
q : PrimeSpectrum R := { asIdeal := q_1, isPrime := ⋯ }
this : q.asIdeal.IsPrime
hxq : x ∈ q.asIdeal
⊢ ∃ (q : PrimeSpectrum R), x ∈ q.asIdeal ∧ p₀ < q ∧ q.asIdeal < 𝔪

Tactic:
⟨q, hxq, lt_of_le_not_ge (le_sup_left.trans hq.1.2) fun h ↦ hn (h hxq), ?_⟩

Premises used: le_sup_left, And.right, And.left, lt_of_le_not_ge, And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : Membership.mem (γ := Ideal R) 𝔪 x
hn : x ∉ p₀.asIdeal
e : (↑(zeroLocus (↑p₀.asIdeal : Set R)) : Type u_1) ≃o PrimeSpectrum (R ⧸ p₀.asIdeal) :=
  p₀.asIdeal.primeSpectrumQuotientOrderIsoZeroLocus.symm
q_1 : Ideal R
hq : q_1 ∈ (p₀.asIdeal + span {x}).minimalPrimes
q : PrimeSpectrum R := { asIdeal := q_1, isPrime := ⋯ }
this : q.asIdeal.IsPrime
hxq : x ∈ q.asIdeal
neg : q.asIdeal < 𝔪
⊢ ∃ (q : PrimeSpectrum R), x ∈ q.asIdeal ∧ p₀ < q ∧ q.asIdeal < 𝔪

Tactic:
refine ⟨q, hxq, lt_of_le_not_ge (le_sup_left.trans hq.1.2) fun h ↦ hn (h hxq), ?_⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : Membership.mem (γ := Ideal R) 𝔪 x
hn : x ∉ p₀.asIdeal
e : (↑(zeroLocus (↑p₀.asIdeal : Set R)) : Type u_1) ≃o PrimeSpectrum (R ⧸ p₀.asIdeal) :=
  p₀.asIdeal.primeSpectrumQuotientOrderIsoZeroLocus.symm
q_1 : Ideal R
hq : q_1 ∈ (p₀.asIdeal + span {x}).minimalPrimes
q : PrimeSpectrum R := { asIdeal := q_1, isPrime := ⋯ }
this : q.asIdeal.IsPrime
hxq : x ∈ q.asIdeal
⊢ q.asIdeal < 𝔪

Tactic:
lt_of_le_of_ne (IsLocalRing.le_maximalIdeal_of_isPrime q.1) fun hqm ↦ ?_

Premises used: IsLocalRing.le_maximalIdeal_of_isPrime, PrimeSpectrum.asIdeal, lt_of_le_of_ne
-- Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : Membership.mem (γ := Ideal R) 𝔪 x
hn : x ∉ p₀.asIdeal
e : (↑(zeroLocus (↑p₀.asIdeal : Set R)) : Type u_1) ≃o PrimeSpectrum (R ⧸ p₀.asIdeal) :=
  p₀.asIdeal.primeSpectrumQuotientOrderIsoZeroLocus.symm
q_1 : Ideal R
hq : q_1 ∈ (p₀.asIdeal + span {x}).minimalPrimes
q : PrimeSpectrum R := { asIdeal := q_1, isPrime := ⋯ }
this : q.asIdeal.IsPrime
hxq : x ∈ q.asIdeal
neg : ∀ (hqm : q.asIdeal = 𝔪), False
⊢ q.asIdeal < 𝔪

Tactic:
refine lt_of_le_of_ne (IsLocalRing.le_maximalIdeal_of_isPrime q.1) fun hqm ↦ ?_

Premises used: IsLocalRing.le_maximalIdeal_of_isPrime, PrimeSpectrum.asIdeal, lt_of_le_of_ne
-- Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : Membership.mem (γ := Ideal R) 𝔪 x
hn : x ∉ p₀.asIdeal
e : (↑(zeroLocus (↑p₀.asIdeal : Set R)) : Type u_1) ≃o PrimeSpectrum (R ⧸ p₀.asIdeal) :=
  p₀.asIdeal.primeSpectrumQuotientOrderIsoZeroLocus.symm
q_1 : Ideal R
hq : q_1 ∈ (p₀.asIdeal + span {x}).minimalPrimes
q : PrimeSpectrum R := { asIdeal := q_1, isPrime := ⋯ }
this : q.asIdeal.IsPrime
hxq : x ∈ q.asIdeal
hqm : q.asIdeal = 𝔪
⊢ height.{u_1} (R := R ⧸ p₀.asIdeal)
      (asIdeal
        ((e : (a : (↑(zeroLocus (↑p₀.asIdeal : Set R)) : Type u_1)) → PrimeSpectrum (R ⧸ p₀.asIdeal))
          (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦
            Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑p₀.asIdeal : Set R)) x) q ⋯))) ≤
    1

Tactic:
have h : (e ⟨q, le_sup_left.trans hq.1.2⟩).1.height ≤ 1 :=
    map_height_le_one_of_mem_minimalPrimes hq