awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
x_1 : PrimeSpectrum R
hx : x_1 ∈ imageOfDf f
x : R
⊢ Membership.mem (γ := Ideal R)
      (asIdeal (PrimeSpectrum.comap C { asIdeal := Ideal.map (F := R →+* R[X]) C x_1.asIdeal, isPrime := ⋯ })) x ↔
    x ∈ x_1.asIdeal
have h : ∀
  (h :
    Membership.mem (γ := Ideal R)
      (asIdeal (PrimeSpectrum.comap C { asIdeal := Ideal.map (F := R →+* R[X]) C x_1.asIdeal, isPrime := sorry })) x),
  x ∈ x_1.asIdeal
Tactic: refine ⟨fun h => ?_, fun h => subset_span (mem_image_of_mem C.1 h)⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
x_1 : PrimeSpectrum R
hx : x_1 ∈ imageOfDf f
x : R
h :
  Membership.mem (γ := Ideal R)
    (asIdeal (PrimeSpectrum.comap C { asIdeal := Ideal.map (F := R →+* R[X]) C x_1.asIdeal, isPrime := ⋯ })) x
⊢ x ∈ x_1.asIdeal
have h₁ : coeff ((C : (a : R) → R[X]) x) 0 ∈ x_1.asIdeal
Tactic: rw [← @coeff_C_zero R x _]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC (goal)
Goal:
R : Type u_1
inst : CommRing R
U : Set (PrimeSpectrum R[X])
s : Set R[X]
z : zeroLocus s = Uᶜ
⊢ IsOpen (PrimeSpectrum.comap C '' U)
have rw : IsOpen.{u_1} (X := PrimeSpectrum R) (⋃ (i : (↑s : Type u_1)), PrimeSpectrum.comap C '' (zeroLocus {(↑i : R[X])})ᶜ)
Tactic: rw [← compl_compl U, ← z, ← iUnion_of_singleton_coe s, zeroLocus_iUnion, compl_iInter,
    image_iUnion]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC (goal)
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)), PrimeSpectrum.comap C '' (zeroLocus {(↑i : R[X])})ᶜ)
have simp_rw : IsOpen.{u_1} (X := PrimeSpectrum R) (⋃ (i : (↑s : Type u_1)), imageOfDf (↑i : R[X]))
Tactic: simp_rw [← imageOfDf_eq_comap_C_compl_zeroLocus]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
⊢ ∃ x ∈ s, IsClosed (X := PrimeSpectrum R) {x}
have simp_rw : ∃ x ∈ s, x.asIdeal.IsMaximal
Tactic: simp_rw [isClosed_singleton_iff_isMaximal]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
⊢ ∃ x ∈ s, x.asIdeal.IsMaximal
have obtain : ∀ (I : Ideal R) (hI' : sᶜ = zeroLocus (↑I : Set R)), ∃ x ∈ s, x.asIdeal.IsMaximal
Tactic: obtain ⟨I, hI'⟩ := (isClosed_iff_zeroLocus_ideal _).mp hs.isClosed_compl
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (goal)
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)
⊢ ∃ x ∈ s, x.asIdeal.IsMaximal
have simp_rw : ∃ (x : PrimeSpectrum R), ¬(↑I : Set R) ⊆ (↑x.asIdeal : Set R) ∧ x.asIdeal.IsMaximal
Tactic: simp_rw [← @Set.notMem_compl_iff _ s, hI', mem_zeroLocus]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (hypothesis)
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)
⊢ ∃ (x : PrimeSpectrum R), ¬(↑I : Set R) ⊆ (↑x.asIdeal : Set R) ∧ x.asIdeal.IsMaximal
have this : s ≠ ∅
Tactic: have := hs'.ne_empty
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (goal)
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 ≠ ∅
⊢ ∃ (x : PrimeSpectrum R), ¬(↑I : Set R) ⊆ (↑x.asIdeal : Set R) ∧ x.asIdeal.IsMaximal
have contrapose! : ∀ (this : ∀ (x : PrimeSpectrum R) (_ : ¬(↑I : Set R) ⊆ (↑x.asIdeal : Set R)), ¬x.asIdeal.IsMaximal), s = ∅
Tactic: contrapose! this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (hypothesis)
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
⊢ s = ∅
have this₁ : ∀ (x : PrimeSpectrum R), x.asIdeal.IsMaximal → (↑I : Set R) ⊆ (↑x.asIdeal : Set R)
Tactic: simp_rw [not_imp_not] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (goal)
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)
⊢ s = ∅
have rw : I.jacobson = jacobson ⊥
Tactic: rw [← Set.compl_univ, eq_compl_comm, hI', eq_comm, ← zeroLocus_bot,
    zeroLocus_eq_iff, Ideal.radical_eq_jacobson, Ideal.radical_eq_jacobson]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (goal)
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 ⊥
have refine : ∀ (b : Ideal R), Membership.mem (γ := Set (Ideal R)) {J : Ideal R | ⊥ ≤ J ∧ J.IsMaximal} b → I.jacobson ≤ b
Tactic: refine le_antisymm (le_sInf ?_) (Ideal.jacobson_mono bot_le)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
⊢ JacobsonSpace.{u_1} (PrimeSpectrum R)
have rw : ∀ (Z : Set (PrimeSpectrum R)), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints (PrimeSpectrum R)).Nonempty
Tactic: rw [jacobsonSpace_iff_locallyClosed]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (hypothesis)
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
⊢ (U ∩ Z ∩ closedPoints (PrimeSpectrum R)).Nonempty
have hU₁ : ∃ (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
Cleared hypotheses: hU, hZ
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (hypothesis)
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
⊢ (U ∩ Z ∩ closedPoints (PrimeSpectrum R)).Nonempty
have hZ₁ : ∃ (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
Cleared hypotheses: hU, hZ
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (goal)
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)
⊢ (U ∩ Z ∩ closedPoints (PrimeSpectrum R)).Nonempty
have 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))
Tactic: obtain ⟨⟨I, rfl⟩, ⟨J, rfl⟩⟩ := And.intro hU hZ
Cleared hypotheses: U, Z, hS, hU, hZ
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (goal)
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))
⊢ Set.Nonempty (α := PrimeSpectrum R)
    ((zeroLocus (↑I : Set R))ᶜ ∩ zeroLocus (↑J : Set R) ∩ closedPoints (PrimeSpectrum R))
have 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))
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 ⊢
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (goal)
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
⊢ ¬Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑J : Set R) ∩ closedPoints (PrimeSpectrum R))
      (zeroLocus (↑I : Set R))
have 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
Tactic: contrapose hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ IsJacobsonRing R ↔ JacobsonSpace.{u_1} (PrimeSpectrum R)
have refine : ∀ (H : JacobsonSpace.{u_1} (PrimeSpectrum R)) (I : Ideal R) (hI : I.IsRadical), I.jacobson ≤ I
Tactic: refine ⟨fun _ ↦ inferInstance, fun H ↦ ⟨fun I hI ↦ le_antisymm ?_ Ideal.le_jacobson⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (goal)
Goal:
R : Type u_1
inst : CommRing R
H : JacobsonSpace.{u_1} (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
⊢ I.jacobson ≤ I
have rw : I.jacobson.radical ≤ I
Tactic: rw [← I.isRadical_jacobson.radical]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (goal)
Goal:
R : Type u_1
inst : CommRing R
H : JacobsonSpace.{u_1} (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
| I
have rw : I.radical
Tactic: rw [← hI.radical]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (goal)
Goal:
R : Type u_1
inst : CommRing R
H : JacobsonSpace.{u_1} (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
⊢ I.jacobson.radical ≤ I
have conv_rhs : I.jacobson.radical ≤ I.radical
Tactic: conv_rhs => rw [← hI.radical]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (goal)
Goal:
R : Type u_1
inst : CommRing R
H : JacobsonSpace.{u_1} (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
⊢ I.jacobson.radical ≤ I.radical
have simp_rw : LE.le (α := Ideal R) (vanishingIdeal (zeroLocus (↑I.jacobson : Set R)) : Ideal R)
  (vanishingIdeal (zeroLocus (↑I : Set R)))
Tactic: simp_rw [← vanishingIdeal_zeroLocus_eq_radical]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (goal)
Goal:
R : Type u_1
inst : CommRing R
H : JacobsonSpace.{u_1} (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
⊢ LE.le (α := Ideal R) (vanishingIdeal (zeroLocus (↑I.jacobson : Set R)) : Ideal R)
    (vanishingIdeal (zeroLocus (↑I : Set R)))
have h : Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus (↑I.jacobson : Set R))
Tactic: apply vanishingIdeal_anti_mono
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (goal)
Goal:
R : Type u_1
inst : CommRing R
H : JacobsonSpace.{u_1} (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
⊢ Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus (↑I.jacobson : Set R))
have h : Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R) ∩ closedPoints (PrimeSpectrum R))
  (zeroLocus (↑I.jacobson : Set R))
Tactic: rw [← H.1 (isClosed_zeroLocus I), (isClosed_zeroLocus _).closure_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (goal)
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
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I.jacobson : Set R)) x
have h : I.jacobson ≤ x.asIdeal
Tactic: change jacobson I ≤ x.asIdeal
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (goal)
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
⊢ IsClopen (X := PrimeSpectrum R) {x}
have obtain : ∀ (y : PrimeSpectrum R) (h' : IsClosed (X := PrimeSpectrum R) {y}),
  IsOpen (X := PrimeSpectrum R) {y} → IsClopen (X := PrimeSpectrum R) {y}
Tactic: obtain ⟨y, rfl : y = x, h'⟩ := exists_isClosed_singleton_of_isJacobsonRing _ h
      ⟨x, Set.mem_singleton x⟩
Cleared hypotheses: x, h_1, h
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsJacobsonRing R
x : PrimeSpectrum R
⊢ [IsOpen (X := PrimeSpectrum R) {x}, IsClopen (X := PrimeSpectrum R) {x},
      IsClosed (X := PrimeSpectrum R) {x} ∧ StableUnderGeneralization (X := PrimeSpectrum R) {x}].TFAE
have tfae_1_to_2 : ∀ (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⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (hypothesis)
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}
⊢ [IsOpen (X := PrimeSpectrum R) {x}, IsClopen (X := PrimeSpectrum R) {x},
      IsClosed (X := PrimeSpectrum R) {x} ∧ StableUnderGeneralization (X := PrimeSpectrum R) {x}].TFAE
have tfae_2_to_3 : ∀ (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⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (hypothesis)
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}
⊢ IsOpen (X := PrimeSpectrum R) {x}
have h₃ : IsMax x
Tactic: rw [isClosed_singleton_iff_isMaximal, ← isMax_iff] at h₁
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (goal)
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})ᶜ
⊢ IsOpen (X := PrimeSpectrum R) {x}
have 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})
Tactic: rw [this, isOpen_compl_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (goal)
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})
have refine : Set.Finite.{u_1} (α := PrimeSpectrum R) {p : PrimeSpectrum R | IsMin p ∧ p ≠ x}
Tactic: refine Set.Finite.isClosed_biUnion ?_ (fun _ _ ↦ isClosed_closure)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (goal)
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}
⊢ IsOpen (X := PrimeSpectrum R) {x}
have suffices : Eq (α := Set (PrimeSpectrum R)) {x}
  (⋃ (p : PrimeSpectrum R),
      ⋃ (_ : Membership.mem (γ := Set (PrimeSpectrum R)) {p : PrimeSpectrum R | IsMin p ∧ p ≠ x} p), closure {p})ᶜ
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
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (goal)
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}
⊢ Eq (α := Set (PrimeSpectrum R)) {x}
    (⋃ (p : PrimeSpectrum R),
        ⋃ (_ : Membership.mem (γ := Set (PrimeSpectrum R)) {p : PrimeSpectrum R | IsMin p ∧ p ≠ x} p), closure {p})ᶜ
have 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
Tactic: ext p
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (goal)
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
⊢ 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
have h : p = x ↔ ∀ (i : PrimeSpectrum R), IsMin i → i ≤ p → i = x
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]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (goal)
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
⊢ p = x ↔ ∀ (i : PrimeSpectrum R), IsMin i → i ≤ p → i = x
have h : p = x → ∀ (i : PrimeSpectrum R), IsMin i → i ≤ p → i = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (goal)
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
⊢ p = x ↔ ∀ (i : PrimeSpectrum R), IsMin i → i ≤ p → i = x
have h₃ : (∀ (i : PrimeSpectrum R), IsMin i → i ≤ p → i = x) → p = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (goal)
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 : IsMin i
⊢ i ≤ p → i = p
have h : ∀ (h₂ : IsMin p) (i : PrimeSpectrum R), IsMin i → i ≤ p → i = p
Tactic: rw [stableUnderGeneralization_singleton, ← isMin_iff] at h₂
Cleared hypotheses: h₂, i, h
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (goal)
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
⊢ p = x
have h : x ≤ p
Tactic: apply h₁.eq_of_ge
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (goal)
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
⊢ x ≤ p
have h : ∀ (q : Ideal R) (hq : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊥) q) (hq' : q ≤ p.asIdeal), x ≤ p
Tactic: obtain ⟨q, hq, hq'⟩ := Ideal.exists_minimalPrimes_le (J := p.asIdeal) bot_le