awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq (α := Ideal R) (vanishingIdeal Set.univ) (nilradical R)
have rw : Eq (α := Ideal R) (⨅ (x : PrimeSpectrum R), ⨅ (_ : Membership.mem (γ := Set (PrimeSpectrum R)) Set.univ x), x.asIdeal)
  (nilradical R)
Tactic: rw [vanishingIdeal, iInf_univ, nilradical_eq_iInf]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
rw :
  Eq (α := Ideal R) (⨅ (x : PrimeSpectrum R), ⨅ (_ : Membership.mem (γ := Set (PrimeSpectrum R)) Set.univ x), x.asIdeal)
    (nilradical R)
⊢ Eq (α := Ideal R) (vanishingIdeal Set.univ) (nilradical R)
have rw₁ : Eq (α := Ideal R) (⨅ (x : PrimeSpectrum R), x.asIdeal) (nilradical R)
Tactic: rw [vanishingIdeal, iInf_univ, nilradical_eq_iInf]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
rw :
  Eq (α := Ideal R) (⨅ (x : PrimeSpectrum R), ⨅ (_ : Membership.mem (γ := Set (PrimeSpectrum R)) Set.univ x), x.asIdeal)
    (nilradical R)
rw₁ : Eq (α := Ideal R) (⨅ (x : PrimeSpectrum R), x.asIdeal) (nilradical R)
⊢ Eq (α := Ideal R) (vanishingIdeal Set.univ) (nilradical R)
have rw₂ : Eq.{u + 1} (α := Ideal R) (⨅ (x : PrimeSpectrum R), x.asIdeal) (iInf asIdeal)
Tactic: rw [vanishingIdeal, iInf_univ, nilradical_eq_iInf]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
⊢ Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus (↑J : Set R)) ↔ J ≤ I.radical
have rw : J ≤ vanishingIdeal (zeroLocus (↑I : Set R)) ↔ J ≤ I.radical
Tactic: rw [subset_zeroLocus_iff_le_vanishingIdeal, vanishingIdeal_zeroLocus_eq_radical]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
rw : J ≤ vanishingIdeal (zeroLocus (↑I : Set R)) ↔ J ≤ I.radical
⊢ Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus (↑J : Set R)) ↔ J ≤ I.radical
have rw₁ : J ≤ I.radical ↔ J ≤ I.radical
Tactic: rw [subset_zeroLocus_iff_le_vanishingIdeal, vanishingIdeal_zeroLocus_eq_radical]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
f g : R
⊢ Subset (α := Set (PrimeSpectrum R)) (zeroLocus {f}) (zeroLocus {g}) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {f})) g
have rw : Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑(Ideal.span {f}) : Set R)) (zeroLocus {g}) ↔
  Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {f})) g
Tactic: rw [← zeroLocus_span {f}, ← zeroLocus_span {g}, zeroLocus_subset_zeroLocus_iff, Ideal.span_le,
    Set.singleton_subset_iff, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
f g : R
rw :
  Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑(Ideal.span {f}) : Set R)) (zeroLocus {g}) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {f})) g
⊢ Subset (α := Set (PrimeSpectrum R)) (zeroLocus {f}) (zeroLocus {g}) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {f})) g
have rw₁ : Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑(Ideal.span {f}) : Set R)) (zeroLocus (↑(Ideal.span {g}) : Set R)) ↔
  Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {f})) g
Tactic: rw [← zeroLocus_span {f}, ← zeroLocus_span {g}, zeroLocus_subset_zeroLocus_iff, Ideal.span_le,
    Set.singleton_subset_iff, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
f g : R
rw :
  Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑(Ideal.span {f}) : Set R)) (zeroLocus {g}) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {f})) g
rw₁ :
  Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑(Ideal.span {f}) : Set R)) (zeroLocus (↑(Ideal.span {g}) : Set R)) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {f})) g
⊢ Subset (α := Set (PrimeSpectrum R)) (zeroLocus {f}) (zeroLocus {g}) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {f})) g
have rw₂ : LE.le (α := Ideal R) (Ideal.span {g}) (Ideal.radical (Ideal.span {f})) ↔
  Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {f})) g
Tactic: rw [← zeroLocus_span {f}, ← zeroLocus_span {g}, zeroLocus_subset_zeroLocus_iff, Ideal.span_le,
    Set.singleton_subset_iff, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
f g : R
rw :
  Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑(Ideal.span {f}) : Set R)) (zeroLocus {g}) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {f})) g
rw₁ :
  Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑(Ideal.span {f}) : Set R)) (zeroLocus (↑(Ideal.span {g}) : Set R)) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {f})) g
rw₂ :
  LE.le (α := Ideal R) (Ideal.span {g}) (Ideal.radical (Ideal.span {f})) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {f})) g
⊢ Subset (α := Set (PrimeSpectrum R)) (zeroLocus {f}) (zeroLocus {g}) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {f})) g
have rw₃ : {g} ⊆ (↑(Ideal.radical (Ideal.span {f})) : Set R) ↔ Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {f})) g
Tactic: rw [← zeroLocus_span {f}, ← zeroLocus_span {g}, zeroLocus_subset_zeroLocus_iff, Ideal.span_le,
    Set.singleton_subset_iff, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
f g : R
rw :
  Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑(Ideal.span {f}) : Set R)) (zeroLocus {g}) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {f})) g
rw₁ :
  Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑(Ideal.span {f}) : Set R)) (zeroLocus (↑(Ideal.span {g}) : Set R)) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {f})) g
rw₂ :
  LE.le (α := Ideal R) (Ideal.span {g}) (Ideal.radical (Ideal.span {f})) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {f})) g
rw₃ :
  {g} ⊆ (↑(Ideal.radical (Ideal.span {f})) : Set R) ↔ Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {f})) g
⊢ Subset (α := Set (PrimeSpectrum R)) (zeroLocus {f}) (zeroLocus {g}) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {f})) g
have rw₄ : g ∈ (↑(Ideal.radical (Ideal.span {f})) : Set R) ↔ Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {f})) g
Tactic: rw [← zeroLocus_span {f}, ← zeroLocus_span {g}, zeroLocus_subset_zeroLocus_iff, Ideal.span_le,
    Set.singleton_subset_iff, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
f g : R
rw :
  Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑(Ideal.span {f}) : Set R)) (zeroLocus {g}) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {f})) g
rw₁ :
  Subset (α := Set (PrimeSpectrum R)) (zeroLocus (↑(Ideal.span {f}) : Set R)) (zeroLocus (↑(Ideal.span {g}) : Set R)) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {f})) g
rw₂ :
  LE.le (α := Ideal R) (Ideal.span {g}) (Ideal.radical (Ideal.span {f})) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {f})) g
rw₃ :
  {g} ⊆ (↑(Ideal.radical (Ideal.span {f})) : Set R) ↔ Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {f})) g
rw₄ : g ∈ (↑(Ideal.radical (Ideal.span {f})) : Set R) ↔ Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {f})) g
⊢ Subset (α := Set (PrimeSpectrum R)) (zeroLocus {f}) (zeroLocus {g}) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {f})) g
have rw₅ : Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {f})) g ↔
  Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {f})) g
Tactic: rw [← zeroLocus_span {f}, ← zeroLocus_span {g}, zeroLocus_subset_zeroLocus_iff, Ideal.span_le,
    Set.singleton_subset_iff, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑(nilradical R) : Set R)) Set.univ
have rw : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑(Ideal.radical 0) : Set R)) Set.univ
Tactic: rw [nilradical, zeroLocus_radical, Ideal.zero_eq_bot, zeroLocus_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
rw : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑(Ideal.radical 0) : Set R)) Set.univ
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑(nilradical R) : Set R)) Set.univ
have rw₁ : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑0 : Set R)) Set.univ
Tactic: rw [nilradical, zeroLocus_radical, Ideal.zero_eq_bot, zeroLocus_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
rw : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑(Ideal.radical 0) : Set R)) Set.univ
rw₁ : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑0 : Set R)) Set.univ
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑(nilradical R) : Set R)) Set.univ
have rw₂ : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑⊥ : Set R)) Set.univ
Tactic: rw [nilradical, zeroLocus_radical, Ideal.zero_eq_bot, zeroLocus_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
rw : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑(Ideal.radical 0) : Set R)) Set.univ
rw₁ : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑0 : Set R)) Set.univ
rw₂ : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑⊥ : Set R)) Set.univ
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑(nilradical R) : Set R)) Set.univ
have rw₃ : Eq.{u + 1} (α := Set (PrimeSpectrum R)) Set.univ Set.univ
Tactic: rw [nilradical, zeroLocus_radical, Ideal.zero_eq_bot, zeroLocus_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
s : Set R
h : 1 ∈ s
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus s) ∅
have rw : ∀ (x : PrimeSpectrum R), x ∉ zeroLocus s
Tactic: rw [Set.eq_empty_iff_forall_notMem]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus s) x
⊢ False
have hx₁ : s ⊆ (↑x.asIdeal : Set R)
Tactic: rw [mem_zeroLocus] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ (↑x.asIdeal : Set R)
⊢ False
have x_prime : x.asIdeal.IsPrime
Tactic: have x_prime : x.asIdeal.IsPrime := by infer_instance
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ (↑x.asIdeal : Set R)
x_prime : x.asIdeal.IsPrime
⊢ x.asIdeal = ⊤
have rw : 1 ∈ x.asIdeal
Tactic: rw [Ideal.eq_top_iff_one]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ (↑x.asIdeal : Set R)
x_prime : x.asIdeal.IsPrime
⊢ False
have eq_top : x.asIdeal = ⊤
Tactic: have eq_top : x.asIdeal = ⊤ := by
    rw [Ideal.eq_top_iff_one]
    exact hx h
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) ∅ ↔ I = ⊤
have mp : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) ∅ → I = ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
mp : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) ∅ → I = ⊤
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) ∅ ↔ I = ⊤
have mpr : I = ⊤ → Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) ∅
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) ∅ → I = ⊤
have mp : I ≠ ⊤ → Set.Nonempty (α := PrimeSpectrum R) (zeroLocus (↑I : Set R))
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
h : I ≠ ⊤
⊢ Set.Nonempty (α := PrimeSpectrum R) (zeroLocus (↑I : Set R))
have mp : ∀ (M : Ideal R) (hM : M.IsMaximal) (hIM : I ≤ M), Set.Nonempty (α := PrimeSpectrum R) (zeroLocus (↑I : Set R))
Tactic: rcases Ideal.exists_le_maximal I h with ⟨M, hM, hIM⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑⊤ : Set R)) ∅
have mpr : 1 ∈ (↑⊤ : Set R)
Tactic: apply zeroLocus_empty_of_one_mem
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ vanishingIdeal s = ⊤ ↔ s = ∅
have rw : ⊤ ≤ vanishingIdeal s ↔ s = ∅
Tactic: rw [← top_le_iff, ← subset_zeroLocus_iff_le_vanishingIdeal, Submodule.top_coe, zeroLocus_univ,
    Set.subset_empty_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
rw : ⊤ ≤ vanishingIdeal s ↔ s = ∅
⊢ vanishingIdeal s = ⊤ ↔ s = ∅
have rw₁ : s ⊆ zeroLocus (↑⊤ : Set R) ↔ s = ∅
Tactic: rw [← top_le_iff, ← subset_zeroLocus_iff_le_vanishingIdeal, Submodule.top_coe, zeroLocus_univ,
    Set.subset_empty_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
rw : ⊤ ≤ vanishingIdeal s ↔ s = ∅
rw₁ : s ⊆ zeroLocus (↑⊤ : Set R) ↔ s = ∅
⊢ vanishingIdeal s = ⊤ ↔ s = ∅
have rw₂ : s ⊆ zeroLocus Set.univ ↔ s = ∅
Tactic: rw [← top_le_iff, ← subset_zeroLocus_iff_le_vanishingIdeal, Submodule.top_coe, zeroLocus_univ,
    Set.subset_empty_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
rw : ⊤ ≤ vanishingIdeal s ↔ s = ∅
rw₁ : s ⊆ zeroLocus (↑⊤ : Set R) ↔ s = ∅
rw₂ : s ⊆ zeroLocus Set.univ ↔ s = ∅
⊢ vanishingIdeal s = ⊤ ↔ s = ∅
have rw₃ : s ⊆ ∅ ↔ s = ∅
Tactic: rw [← top_le_iff, ← subset_zeroLocus_iff_le_vanishingIdeal, Submodule.top_coe, zeroLocus_univ,
    Set.subset_empty_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
rw : ⊤ ≤ vanishingIdeal s ↔ s = ∅
rw₁ : s ⊆ zeroLocus (↑⊤ : Set R) ↔ s = ∅
rw₂ : s ⊆ zeroLocus Set.univ ↔ s = ∅
rw₃ : s ⊆ ∅ ↔ s = ∅
⊢ vanishingIdeal s = ⊤ ↔ s = ∅
have rw₄ : s = ∅ ↔ s = ∅
Tactic: rw [← top_le_iff, ← subset_zeroLocus_iff_le_vanishingIdeal, Submodule.top_coe, zeroLocus_univ,
    Set.subset_empty_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
s : Set R
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus s) Set.univ ↔ s ⊆ (↑(nilradical R) : Set R)
have rw : Subset (α := Set (PrimeSpectrum R)) Set.univ (zeroLocus s) ↔ s ⊆ (↑(nilradical R) : Set R)
Tactic: rw [← Set.univ_subset_iff, subset_zeroLocus_iff_subset_vanishingIdeal, vanishingIdeal_univ]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
s : Set R
rw : Subset (α := Set (PrimeSpectrum R)) Set.univ (zeroLocus s) ↔ s ⊆ (↑(nilradical R) : Set R)
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus s) Set.univ ↔ s ⊆ (↑(nilradical R) : Set R)
have rw₁ : s ⊆ (↑(vanishingIdeal Set.univ) : Set R) ↔ s ⊆ (↑(nilradical R) : Set R)
Tactic: rw [← Set.univ_subset_iff, subset_zeroLocus_iff_subset_vanishingIdeal, vanishingIdeal_univ]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
s : Set R
rw : Subset (α := Set (PrimeSpectrum R)) Set.univ (zeroLocus s) ↔ s ⊆ (↑(nilradical R) : Set R)
rw₁ : s ⊆ (↑(vanishingIdeal Set.univ) : Set R) ↔ s ⊆ (↑(nilradical R) : Set R)
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus s) Set.univ ↔ s ⊆ (↑(nilradical R) : Set R)
have rw₂ : s ⊆ (↑(nilradical R) : Set R) ↔ s ⊆ (↑(nilradical R) : Set R)
Tactic: rw [← Set.univ_subset_iff, subset_zeroLocus_iff_subset_vanishingIdeal, vanishingIdeal_univ]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
s s' : Set R
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus s ∪ zeroLocus s') (zeroLocus (↑(Ideal.span s ⊓ Ideal.span s') : Set R))
have rw : Eq (α := Set (PrimeSpectrum R)) (zeroLocus s ∪ zeroLocus s')
  (zeroLocus (↑(Ideal.span s) : Set R) ∪ zeroLocus (↑(Ideal.span s') : Set R))
Tactic: rw [zeroLocus_inf]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
t t' : Set (PrimeSpectrum R)
r : R
⊢ r ∈ vanishingIdeal t ⊔ vanishingIdeal t' → r ∈ vanishingIdeal (t ∩ t')
have rw : (∃ y ∈ vanishingIdeal t, ∃ z ∈ vanishingIdeal t', y + z = r) → ∀ x ∈ t ∩ t', r ∈ x.asIdeal
Tactic: rw [Submodule.mem_sup, mem_vanishingIdeal]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
t t' : Set (PrimeSpectrum R)
f : R
hf : f ∈ vanishingIdeal t
g : R
hg : g ∈ vanishingIdeal t'
x : PrimeSpectrum R
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f + g ∈ x.asIdeal
have rw : ∀ (hf : ∀ x ∈ t, f ∈ x.asIdeal) (g : R) (hg : ∀ x ∈ t', g ∈ x.asIdeal) (x : PrimeSpectrum R) (hxt : x ∈ t)
  (hxt' : x ∈ t'), f + g ∈ x.asIdeal
Tactic: rw [mem_vanishingIdeal] at hf hg
Cleared hypotheses: hf, g, hg, x, hxt, hxt'
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
t t' : Set (PrimeSpectrum R)
f : R
hf : ∀ x ∈ t, f ∈ x.asIdeal
g : R
hg : ∀ x ∈ t', g ∈ x.asIdeal
x : PrimeSpectrum R
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f + g ∈ x.asIdeal
have h₁ : f ∈ x.asIdeal
Tactic: apply Submodule.add_mem
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
t t' : Set (PrimeSpectrum R)
f : R
hf : ∀ x ∈ t, f ∈ x.asIdeal
g : R
hg : ∀ x ∈ t', g ∈ x.asIdeal
x : PrimeSpectrum R
hxt : x ∈ t
hxt' : x ∈ t'
h₁ : f ∈ x.asIdeal
⊢ f + g ∈ x.asIdeal
have h₂ : g ∈ x.asIdeal
Tactic: apply Submodule.add_mem
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
f : R
I : PrimeSpectrum R
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus {f})ᶜ I ↔ f ∉ I.asIdeal
have rw : f ∉ (↑I.asIdeal : Set R) ↔ f ∉ I.asIdeal
Tactic: rw [Set.mem_compl_iff, mem_zeroLocus, Set.singleton_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
s : Set R
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (insert 0 s)) (zeroLocus s)
have rw : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (s ∪ {0})) (zeroLocus s)
Tactic: rw [← Set.union_singleton, zeroLocus_union, zeroLocus_singleton_zero, Set.inter_univ]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
s : Set R
rw : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (s ∪ {0})) (zeroLocus s)
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (insert 0 s)) (zeroLocus s)
have rw₁ : Eq (α := Set (PrimeSpectrum R)) (zeroLocus s ∩ zeroLocus {0}) (zeroLocus s)
Tactic: rw [← Set.union_singleton, zeroLocus_union, zeroLocus_singleton_zero, Set.inter_univ]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
s : Set R
rw : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (s ∪ {0})) (zeroLocus s)
rw₁ : Eq (α := Set (PrimeSpectrum R)) (zeroLocus s ∩ zeroLocus {0}) (zeroLocus s)
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (insert 0 s)) (zeroLocus s)
have rw₂ : Eq (α := Set (PrimeSpectrum R)) (zeroLocus s ∩ Set.univ) (zeroLocus s)
Tactic: rw [← Set.union_singleton, zeroLocus_union, zeroLocus_singleton_zero, Set.inter_univ]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
s : Set R
rw : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (s ∪ {0})) (zeroLocus s)
rw₁ : Eq (α := Set (PrimeSpectrum R)) (zeroLocus s ∩ zeroLocus {0}) (zeroLocus s)
rw₂ : Eq (α := Set (PrimeSpectrum R)) (zeroLocus s ∩ Set.univ) (zeroLocus s)
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (insert 0 s)) (zeroLocus s)
have rw₃ : Eq (α := Set (PrimeSpectrum R)) (zeroLocus s) (zeroLocus s)
Tactic: rw [← Set.union_singleton, zeroLocus_union, zeroLocus_singleton_zero, Set.inter_univ]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
s : Set R
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (s \ {0})) (zeroLocus s)
have rw : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (insert 0 (s \ {0}))) (zeroLocus (insert 0 s))
Tactic: rw [← zeroLocus_insert_zero, ← zeroLocus_insert_zero (s := s)]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
r : R
hr : IsUnit r
s : Set R
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (r • s)) (zeroLocus s)
have h : ∀ (x : PrimeSpectrum R),
  Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (r • s)) x ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus s) x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x : PrimeSpectrum R
⊢ IsMax x ↔ x.asIdeal.IsMaximal
have refine : ∀ (hx : IsMax x) (I : Ideal R) (hI : x.asIdeal < I), I = ⊤
Tactic: refine ⟨fun hx ↦ ⟨⟨x.2.ne_top, fun I hI ↦ ?_⟩⟩, fun hx y e ↦ (hx.eq_of_le y.2.ne_top e).ge⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x : PrimeSpectrum R
hx : IsMax x
I : Ideal R
hI : x.asIdeal < I
⊢ I = ⊤
have by_contra : ∀ (e : ¬I = ⊤), False
Tactic: by_contra e
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
x : PrimeSpectrum R
hx : IsMax x
I : Ideal R
hI : x.asIdeal < I
e : ¬I = ⊤
⊢ False
have obtain : ∀ (m : Ideal R) (hm : m.IsMaximal) (hm' : I ≤ m), False
Tactic: obtain ⟨m, hm, hm'⟩ := Ideal.exists_le_maximal I e
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
m : Ideal R
inst_1 : m.IsMaximal
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑m : Set R)) {{ asIdeal := m, isPrime := ⋯ : PrimeSpectrum R }}
have h : ∀ (I : PrimeSpectrum R),
  Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑m : Set R)) I ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) {{ asIdeal := m, isPrime := sorry : PrimeSpectrum R }} I
Tactic: ext I
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
m : Ideal R
inst_1 : m.IsMaximal
I : PrimeSpectrum R
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑m : Set R)) I ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) {{ asIdeal := m, isPrime := ⋯ : PrimeSpectrum R }} I
have h : ∀ (h : Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑m : Set R)) I),
  Membership.mem (γ := Set (PrimeSpectrum R)) {{ asIdeal := m, isPrime := sorry : PrimeSpectrum R }} I
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
m : Ideal R
inst_1 : m.IsMaximal
I : PrimeSpectrum R
h :
  ∀ (h : Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑m : Set R)) I),
    Membership.mem (γ := Set (PrimeSpectrum R)) {{ asIdeal := m, isPrime := ⋯ : PrimeSpectrum R }} I
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑m : Set R)) I ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) {{ asIdeal := m, isPrime := ⋯ : PrimeSpectrum R }} I
have h₁ : ∀ (h : Membership.mem (γ := Set (PrimeSpectrum R)) {{ asIdeal := m, isPrime := sorry : PrimeSpectrum R }} I),
  Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑m : Set R)) I
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩