awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
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
⊢ s ⊂ t ↔ vanishingIdeal t < vanishingIdeal s
have rw₁ : s ⊆ t ∧ ¬vanishingIdeal s ≤ vanishingIdeal 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]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
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
⊢ s ⊂ t ↔ vanishingIdeal t < vanishingIdeal s
have rw₂ : vanishingIdeal t ≤ vanishingIdeal s ∧ ¬vanishingIdeal s ≤ vanishingIdeal 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]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
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
⊢ s ⊂ t ↔ vanishingIdeal t < vanishingIdeal s
have rw₃ : vanishingIdeal t ≤ vanishingIdeal s ∧ ¬vanishingIdeal s ≤ vanishingIdeal t ↔
  vanishingIdeal t ≤ vanishingIdeal s ∧ ¬vanishingIdeal s ≤ vanishingIdeal t
Tactic: rw [Set.ssubset_def, vanishingIdeal_anti_mono_iff hs, vanishingIdeal_anti_mono_iff ht,
    lt_iff_le_not_ge]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsDomain R
⊢ T1Space.{u} (PrimeSpectrum R) ↔ IsField R
have refine_1 : T1Space.{u} (PrimeSpectrum R) → IsField R
Tactic: refine ⟨?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsDomain R
refine_1 : T1Space.{u} (PrimeSpectrum R) → IsField R
⊢ T1Space.{u} (PrimeSpectrum R) ↔ IsField R
have refine_2 : ∀ (h : IsField R), T1Space.{u} (PrimeSpectrum R)
Tactic: refine ⟨?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsDomain R
h : IsField R
⊢ T1Space.{u} (PrimeSpectrum R)
have refine_2 : ∀ (x : PrimeSpectrum R), x.asIdeal.IsMaximal
Tactic: refine ⟨fun x => (isClosed_singleton_iff_isMaximal x).2 ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsDomain R
h : IsField R
x : PrimeSpectrum R
⊢ x.asIdeal.IsMaximal
have pos : ∀ (hx : x.asIdeal = ⊥), x.asIdeal.IsMaximal
Tactic: by_cases hx : x.asIdeal = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsDomain R
h : IsField R
x : PrimeSpectrum R
pos : ∀ (hx : x.asIdeal = ⊥), x.asIdeal.IsMaximal
⊢ x.asIdeal.IsMaximal
have neg : ∀ (hx : ¬x.asIdeal = ⊥), x.asIdeal.IsMaximal
Tactic: by_cases hx : x.asIdeal = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ IsIrreducible (X := PrimeSpectrum R) Z(↑I) ↔ I.IsPrime
have rw : Set.Nonempty (α := PrimeSpectrum R) Z(↑I) ∧ IsPreirreducible (X := PrimeSpectrum R) Z(↑I) ↔
  I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
Tactic: rw [Ideal.isPrime_iff, IsIrreducible]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ Set.Nonempty (α := PrimeSpectrum R) Z(↑I) ∧ IsPreirreducible (X := PrimeSpectrum R) Z(↑I) ↔
    I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
have h₁ : Set.Nonempty (α := PrimeSpectrum R) Z(↑I) ↔ I ≠ ⊤
Tactic: apply and_congr
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsRadical
h₁ : Set.Nonempty (α := PrimeSpectrum R) Z(↑I) ↔ I ≠ ⊤
⊢ Set.Nonempty (α := PrimeSpectrum R) Z(↑I) ∧ IsPreirreducible (X := PrimeSpectrum R) Z(↑I) ↔
    I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
have h₂ : IsPreirreducible (X := PrimeSpectrum R) Z(↑I) ↔ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
Tactic: apply and_congr
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ Set.Nonempty (α := PrimeSpectrum R) Z(↑I) ↔ I ≠ ⊤
have h₁ : Ne (α := Set (PrimeSpectrum R)) Z(↑I) ∅ ↔ I ≠ ⊤
Tactic: rw [Set.nonempty_iff_ne_empty, Ne, zeroLocus_empty_iff_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsRadical
h₁ : Ne (α := Set (PrimeSpectrum R)) Z(↑I) ∅ ↔ I ≠ ⊤
⊢ Set.Nonempty (α := PrimeSpectrum R) Z(↑I) ↔ I ≠ ⊤
have h₂ : ¬Eq (α := Set (PrimeSpectrum R)) Z(↑I) ∅ ↔ I ≠ ⊤
Tactic: rw [Set.nonempty_iff_ne_empty, Ne, zeroLocus_empty_iff_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
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 ≠ ⊤
⊢ Set.Nonempty (α := PrimeSpectrum R) Z(↑I) ↔ I ≠ ⊤
have h₃ : ¬I = ⊤ ↔ I ≠ ⊤
Tactic: rw [Set.nonempty_iff_ne_empty, Ne, zeroLocus_empty_iff_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ IsPreirreducible (X := PrimeSpectrum R) Z(↑I) ↔ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
have 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)
Tactic: trans ∀ x y : Ideal R, Z(I) ⊆ Z(x) ∪ Z(y) → Z(I) ⊆ Z(x) ∨ Z(I) ⊆ Z(y)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
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)
⊢ IsPreirreducible (X := PrimeSpectrum R) Z(↑I) ↔ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
have 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
Tactic: trans ∀ x y : Ideal R, Z(I) ⊆ Z(x) ∪ Z(y) → Z(I) ⊆ Z(x) ∨ Z(I) ⊆ Z(y)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ 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)
have 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)
Tactic: simp_rw [isPreirreducible_iff_isClosed_union_isClosed, isClosed_iff_zeroLocus_ideal]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ (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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
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)
⊢ (∀ (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)
have 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₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ (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
have simp_rw : (∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I) ↔ ∀ {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]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I) ↔ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
have mp : (∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I) → ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
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
⊢ (∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I) ↔ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
have mpr : (∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I) → ∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I) → ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
have 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
Tactic: simp_rw [← SetLike.mem_coe, ← Set.singleton_subset_iff, ← Ideal.span_le, ←
          Ideal.span_singleton_mul_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I) →
    ∀ {x y : R},
      HMul.hMul (α := Ideal R) (Ideal.span {x}) (Ideal.span {y}) ≤ I → Ideal.span {x} ≤ I ∨ Ideal.span {y} ≤ I
have mp : ∀ (h : ∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I) (x y : R)
  (h' : HMul.hMul (α := Ideal R) (Ideal.span {x}) (Ideal.span {y}) ≤ I), Ideal.span {x} ⊓ Ideal.span {y} ≤ I
Tactic: refine fun h x y h' => h _ _ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsRadical
h : ∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I
x y : R
h' : HMul.hMul (α := Ideal R) (Ideal.span {x}) (Ideal.span {y}) ≤ I
⊢ Ideal.span {x} ⊓ Ideal.span {y} ≤ I
have mp : ∀ (h' : (HMul.hMul (α := Ideal R) (Ideal.span {x}) (Ideal.span {y})).radical ≤ I),
  Ideal.radical (Ideal.span {x} ⊓ Ideal.span {y}) ≤ I
Tactic: rw [← hI.radical_le_iff] at h' ⊢
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I) → ∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I
have mpr : (∀ {x y : R}, x * y ∈ I → x ∉ I → y ∈ I) → ∀ (x y : Ideal R), x ⊓ y ≤ I → (∃ x_1 ∈ x, x_1 ∉ I) → y ≤ I
Tactic: simp_rw [or_iff_not_imp_left, SetLike.not_le_iff_exists]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ IsIrreducible s ↔ (vanishingIdeal s).IsPrime
have rw : IsIrreducible (closure s) ↔ (vanishingIdeal s).IsPrime
Tactic: rw [← isIrreducible_iff_closure, ← zeroLocus_vanishingIdeal_eq_closure,
    isIrreducible_zeroLocus_iff_of_radical _ (isRadical_vanishingIdeal s)]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
rw : IsIrreducible (closure s) ↔ (vanishingIdeal s).IsPrime
⊢ IsIrreducible s ↔ (vanishingIdeal s).IsPrime
have rw₁ : IsIrreducible (X := PrimeSpectrum R) Z(↑(vanishingIdeal s)) ↔ (vanishingIdeal s).IsPrime
Tactic: rw [← isIrreducible_iff_closure, ← zeroLocus_vanishingIdeal_eq_closure,
    isIrreducible_zeroLocus_iff_of_radical _ (isRadical_vanishingIdeal s)]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
rw : IsIrreducible (closure s) ↔ (vanishingIdeal s).IsPrime
rw₁ : IsIrreducible (X := PrimeSpectrum R) Z(↑(vanishingIdeal s)) ↔ (vanishingIdeal s).IsPrime
⊢ IsIrreducible s ↔ (vanishingIdeal s).IsPrime
have rw₂ : (vanishingIdeal s).IsPrime ↔ (vanishingIdeal s).IsPrime
Tactic: rw [← isIrreducible_iff_closure, ← zeroLocus_vanishingIdeal_eq_closure,
    isIrreducible_zeroLocus_iff_of_radical _ (isRadical_vanishingIdeal s)]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq.{u + 1} (α := Set (Ideal R)) (vanishingIdeal '' {s : Set (PrimeSpectrum R) | IsClosed s ∧ IsIrreducible s})
    {P : Ideal R | P.IsPrime}
have refine_1 : Subset.{u} (α := Set (Ideal R)) (vanishingIdeal '' {s : Set (PrimeSpectrum R) | IsClosed s ∧ IsIrreducible s})
  (vanishingIdeal '' {s : Set (PrimeSpectrum R) | IsIrreducible s})
Tactic: refine (subset_antisymm ?_ ?_).trans vanishingIdeal_isIrreducible
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
refine_1 :
  Subset.{u} (α := Set (Ideal R)) (vanishingIdeal '' {s : Set (PrimeSpectrum R) | IsClosed s ∧ IsIrreducible s})
    (vanishingIdeal '' {s : Set (PrimeSpectrum R) | IsIrreducible s})
⊢ Eq.{u + 1} (α := Set (Ideal R)) (vanishingIdeal '' {s : Set (PrimeSpectrum R) | IsClosed s ∧ IsIrreducible s})
    {P : Ideal R | P.IsPrime}
have refine_2 : Subset.{u} (α := Set (Ideal R)) (vanishingIdeal '' {s : Set (PrimeSpectrum R) | IsIrreducible s})
  (vanishingIdeal '' {s : Set (PrimeSpectrum R) | IsClosed s ∧ IsIrreducible s})
Tactic: refine (subset_antisymm ?_ ?_).trans vanishingIdeal_isIrreducible
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S_1 : Type v
inst : CommSemiring R
inst_1 : CommSemiring S_1
S : Set (PrimeSpectrum R)
h₁ : IsIrreducible S
h₂ : IsClosed S
⊢ IsGenericPoint { asIdeal := vanishingIdeal S, isPrime := ⋯ : PrimeSpectrum R } S
have rw : closure {{ asIdeal := vanishingIdeal S, isPrime := sorry : PrimeSpectrum R }} = S
Tactic: rw [IsGenericPoint, closure_singleton, zeroLocus_vanishingIdeal_eq_closure, h₂.closure_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S_1 : Type v
inst : CommSemiring R
inst_1 : CommSemiring S_1
S : Set (PrimeSpectrum R)
h₁ : IsIrreducible S
h₂ : IsClosed S
rw : closure {{ asIdeal := vanishingIdeal S, isPrime := ⋯ : PrimeSpectrum R }} = S
⊢ IsGenericPoint { asIdeal := vanishingIdeal S, isPrime := ⋯ : PrimeSpectrum R } S
have rw₁ : Z(↑{ asIdeal := vanishingIdeal S, isPrime := sorry : PrimeSpectrum R }.asIdeal) = S
Tactic: rw [IsGenericPoint, closure_singleton, zeroLocus_vanishingIdeal_eq_closure, h₂.closure_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S_1 : Type v
inst : CommSemiring R
inst_1 : CommSemiring S_1
S : Set (PrimeSpectrum R)
h₁ : IsIrreducible S
h₂ : IsClosed S
rw : closure {{ asIdeal := vanishingIdeal S, isPrime := ⋯ : PrimeSpectrum R }} = S
rw₁ : Z(↑{ asIdeal := vanishingIdeal S, isPrime := ⋯ : PrimeSpectrum R }.asIdeal) = S
⊢ IsGenericPoint { asIdeal := vanishingIdeal S, isPrime := ⋯ : PrimeSpectrum R } S
have rw₂ : closure S = S
Tactic: rw [IsGenericPoint, closure_singleton, zeroLocus_vanishingIdeal_eq_closure, h₂.closure_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S_1 : Type v
inst : CommSemiring R
inst_1 : CommSemiring S_1
S : Set (PrimeSpectrum R)
h₁ : IsIrreducible S
h₂ : IsClosed S
rw : closure {{ asIdeal := vanishingIdeal S, isPrime := ⋯ : PrimeSpectrum R }} = S
rw₁ : Z(↑{ asIdeal := vanishingIdeal S, isPrime := ⋯ : PrimeSpectrum R }.asIdeal) = S
rw₂ : closure S = S
⊢ IsGenericPoint { asIdeal := vanishingIdeal S, isPrime := ⋯ : PrimeSpectrum R } S
have rw₃ : S = S
Tactic: rw [IsGenericPoint, closure_singleton, zeroLocus_vanishingIdeal_eq_closure, h₂.closure_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
⊢ CompactSpace.{u} (PrimeSpectrum R)
have refine : ∀ {ι : Type u} (S : ι → Set (PrimeSpectrum R)) (S_closed : ∀ (i : ι), IsClosed (S i))
  (S_empty : Eq.{u + 1} (α := Set (PrimeSpectrum R)) (⋂ (i : ι), S i) ∅),
  ∃ (u : Finset ι), Eq.{u + 1} (α := Set (PrimeSpectrum R)) (⋂ i ∈ u, S i) ∅
Tactic: refine compactSpace_of_finite_subfamily_closed fun S S_closed S_empty ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S_1 : Type v
inst : CommSemiring R
inst_1 : CommSemiring S_1
ι : Type u
S : ι → Set (PrimeSpectrum R)
S_closed : ∀ (i : ι), IsClosed (S i)
S_empty : Eq.{u + 1} (α := Set (PrimeSpectrum R)) (⋂ (i : ι), S i) ∅
⊢ ∃ (u : Finset ι), Eq.{u + 1} (α := Set (PrimeSpectrum R)) (⋂ i ∈ u, S i) ∅
have choose : ∀ (I : (i : ι) → Ideal R) (hI : ∀ (i : ι), S i = Z(↑(I i))),
  ∃ (u : Finset ι), Eq.{u + 1} (α := Set (PrimeSpectrum R)) (⋂ i ∈ u, S i) ∅
Tactic: choose I hI using fun i ↦ (isClosed_iff_zeroLocus_ideal (S i)).mp (S_closed i)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S_1 : Type v
inst : CommSemiring R
inst_1 : CommSemiring S_1
ι : Type u
S : ι → Set (PrimeSpectrum R)
S_closed : ∀ (i : ι), IsClosed (S i)
S_empty : Eq.{u + 1} (α := Set (PrimeSpectrum R)) (⋂ (i : ι), S i) ∅
I : (i : ι) → Ideal R
hI : ∀ (i : ι), S i = Z(↑(I i))
⊢ ∃ (u : Finset ι), Eq.{u + 1} (α := Set (PrimeSpectrum R)) (⋂ i ∈ u, S i) ∅
have simp_rw : ∀ (S_empty : LE.le.{u} (α := Ideal R) ⊤ (⨆ (i : ι), I i)), ∃ (u : Finset ι), LE.le.{u} (α := Ideal R) ⊤ (⨆ i ∈ u, I i)
Tactic: simp_rw [hI, ← zeroLocus_iSup, zeroLocus_empty_iff_eq_top, ← top_le_iff] at S_empty ⊢
Cleared hypotheses: S_empty
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
⊢ DiscreteTopology.{u} (PrimeSpectrum R) ↔
    Finite.{u + 1} (↑{I : Ideal R | I.IsMaximal} : Type u) ∧
      LE.le (α := Ideal R) (sInf {I : Ideal R | I.IsMaximal}) (nilradical R)
have rw : (Set.Finite.{u} (α := Ideal R) {x : Ideal R | x.IsPrime} ∧ ∀ (I : Ideal R), I.IsPrime → I.IsMaximal) ↔
  Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal} ∧
    LE.le (α := Ideal R) (sInf {I : Ideal R | I.IsMaximal}) (nilradical R)
Tactic: rw [discreteTopology_iff_finite_and_krullDimLE_zero, Ring.krullDimLE_zero_iff,
    (equivSubtype R).finite_iff, ← Set.coe_setOf, Set.finite_coe_iff, Set.finite_coe_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
⊢ (Set.Finite.{u} (α := Ideal R) {x : Ideal R | x.IsPrime} ∧ ∀ (I : Ideal R), I.IsPrime → I.IsMaximal) ↔
    Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal} ∧
      LE.le (α := Ideal R) (sInf {I : Ideal R | I.IsMaximal}) (nilradical R)
have refine : Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal} ∧
    LE.le (α := Ideal R) (sInf {I : Ideal R | I.IsMaximal}) (nilradical R) →
  ∀ (fin : Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal})
    (le : LE.le (α := Ideal R) (sInf {I : Ideal R | I.IsMaximal}) (nilradical R)),
    Set.Finite.{u} (α := Ideal R) {x : Ideal R | x.IsPrime} ∧ ∀ (I : Ideal R), I.IsPrime → I.IsMaximal
Tactic: refine ⟨fun h ↦ ⟨h.1.subset fun _ h ↦ h.isPrime, nilradical_eq_sInf R ▸ sInf_le_sInf h.2⟩,
    fun ⟨fin, le⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
h :
  Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal} ∧
    LE.le (α := Ideal R) (sInf {I : Ideal R | I.IsMaximal}) (nilradical R)
fin : Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal}
le : LE.le (α := Ideal R) (sInf {I : Ideal R | I.IsMaximal}) (nilradical R)
I : Ideal R
hI : I.IsPrime
⊢ I.IsMaximal
have le₁ : sInf {I : Ideal R | I.IsMaximal} ≤ I
Tactic: replace le := le.trans (nilradical_le_prime I)
Cleared hypotheses: le
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
h :
  Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal} ∧
    LE.le (α := Ideal R) (sInf {I : Ideal R | I.IsMaximal}) (nilradical R)
fin : Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal}
I : Ideal R
hI : I.IsPrime
le : sInf {I : Ideal R | I.IsMaximal} ≤ I
⊢ I.IsMaximal
have le₁ : ∃ i ∈ fin.toFinset (s := {I : Ideal R | I.IsMaximal}), id i ≤ I
Tactic: rw [← fin.coe_toFinset, ← Finset.inf_id_eq_sInf, hI.inf_le'] at le
Cleared hypotheses: le
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
h :
  Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal} ∧
    LE.le (α := Ideal R) (sInf {I : Ideal R | I.IsMaximal}) (nilradical R)
fin : Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal}
I : Ideal R
hI : I.IsPrime
le : ∃ i ∈ fin.toFinset (s := {I : Ideal R | I.IsMaximal}), id i ≤ I
⊢ I.IsMaximal
have have : ∀ (M : Ideal R) (hM : M ∈ fin.toFinset (s := {I : Ideal R | I.IsMaximal})) (hMI : id M ≤ I), I.IsMaximal
Tactic: have ⟨M, hM, hMI⟩ := le
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
h :
  Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal} ∧
    LE.le (α := Ideal R) (sInf {I : Ideal R | I.IsMaximal}) (nilradical R)
fin : Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal}
I : Ideal R
hI : I.IsPrime
le : ∃ i ∈ fin.toFinset (s := {I : Ideal R | I.IsMaximal}), id i ≤ I
M : Ideal R
hM : M ∈ fin.toFinset (s := {I : Ideal R | I.IsMaximal})
hMI : id M ≤ I
⊢ I.IsMaximal
have hM₁ : Membership.mem (γ := Set (Ideal R)) {I : Ideal R | I.IsMaximal} M
Tactic: rw [fin.mem_toFinset] at hM
Cleared hypotheses: hM, hMI