awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
p : PrimeSpectrum (R × S)
h :
  Membership.mem (γ := Set (PrimeSpectrum (R × S)))
    (zeroLocus (↑(RingHom.ker (F := R × S →+* S) (RingHom.snd R S)) : Set (R × S))) p
⊢ Membership.mem (γ := Set (PrimeSpectrum (R × S))) (Set.range (ι := PrimeSpectrum S) (comap (RingHom.snd R S))) p
have refine_2 : ∀ (p_1 : Ideal R) (hp : p_1.IsPrime) (eq : p.asIdeal = p_1.prod ⊤),
  Membership.mem (γ := Set (PrimeSpectrum (R × S))) (Set.range (ι := PrimeSpectrum S) (comap (RingHom.snd R S))) p
Tactic: obtain ⟨p, hp, eq⟩ | ⟨p, hp, eq⟩ := p.1.ideal_prod_prime.mp p.2
-- 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
p : PrimeSpectrum (R × S)
h :
  Membership.mem (γ := Set (PrimeSpectrum (R × S)))
    (zeroLocus (↑(RingHom.ker (F := R × S →+* S) (RingHom.snd R S)) : Set (R × S))) p
refine_2 :
  ∀ (p_1 : Ideal R) (hp : p_1.IsPrime) (eq : p.asIdeal = p_1.prod ⊤),
    Membership.mem (γ := Set (PrimeSpectrum (R × S))) (Set.range (ι := PrimeSpectrum S) (comap (RingHom.snd R S))) p
⊢ Membership.mem (γ := Set (PrimeSpectrum (R × S))) (Set.range (ι := PrimeSpectrum S) (comap (RingHom.snd R S))) p
have refine_2₁ : ∀ (p_1 : Ideal S) (hp : p_1.IsPrime) (eq : p.asIdeal = Ideal.prod ⊤ p_1),
  Membership.mem (γ := Set (PrimeSpectrum (R × S))) (Set.range (ι := PrimeSpectrum S) (comap (RingHom.snd R S))) p
Tactic: obtain ⟨p, hp, eq⟩ | ⟨p, hp, eq⟩ := p.1.ideal_prod_prime.mp p.2
-- 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
p_1 : PrimeSpectrum (R × S)
h :
  Membership.mem (γ := Set (PrimeSpectrum (R × S)))
    (zeroLocus (↑(RingHom.ker (F := R × S →+* S) (RingHom.snd R S)) : Set (R × S))) p_1
p : Ideal R
hp : p.IsPrime
eq : p_1.asIdeal = p.prod ⊤
⊢ Membership.mem (γ := Set (PrimeSpectrum (R × S))) (Set.range (ι := PrimeSpectrum S) (comap (RingHom.snd R S))) p_1
have refine_2 : 1 ∈ p
Tactic: refine (hp.ne_top <| (Ideal.eq_top_iff_one _).mpr ?_).elim
-- 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
⊢ IsClosed (X := PrimeSpectrum (R × S)) (Set.range (ι := PrimeSpectrum R) (comap (RingHom.fst R S)))
have simp_rw : IsClosed (X := PrimeSpectrum (R × S)) (zeroLocus (↑(RingHom.ker (F := R × S →+* R) (RingHom.fst R S)) : Set (R × S)))
Tactic: simp_rw [range_comap_fst, isClosed_zeroLocus]
-- 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
⊢ IsClosed (X := PrimeSpectrum (R × S)) (Set.range (ι := PrimeSpectrum S) (comap (RingHom.snd R S)))
have simp_rw : IsClosed (X := PrimeSpectrum (R × S)) (zeroLocus (↑(RingHom.ker (F := R × S →+* S) (RingHom.snd R S)) : Set (R × S)))
Tactic: simp_rw [range_comap_snd, isClosed_zeroLocus]
-- 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
⊢ PrimeSpectrum (R × S) ≃ₜ Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)
have refine : IsInducing (X := Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)) (Y := PrimeSpectrum (R × S))
  (⇑(Equiv.symm (primeSpectrumProd R S)) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
Tactic: refine ((primeSpectrumProd R S).symm.toHomeomorphOfIsInducing ?_).symm
-- 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
⊢ IsInducing (X := Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)) (Y := PrimeSpectrum (R × S))
    (⇑(Equiv.symm (primeSpectrumProd R S)) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
have refine_1 : Continuous (X := Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)) (Y := PrimeSpectrum (R × S))
  (⇑(Equiv.symm (primeSpectrumProd R S)) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
Tactic: refine (IsClosedEmbedding.of_continuous_injective_isClosedMap ?_
    (Equiv.injective _) ?_).isInducing
-- 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
refine_1 :
  Continuous (X := Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)) (Y := PrimeSpectrum (R × S))
    (⇑(Equiv.symm (primeSpectrumProd R S)) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
⊢ IsInducing (X := Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)) (Y := PrimeSpectrum (R × S))
    (⇑(Equiv.symm (primeSpectrumProd R S)) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
have refine_2 : IsClosedMap (X := Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)) (Y := PrimeSpectrum (R × S))
  (⇑(Equiv.symm (primeSpectrumProd R S)) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
Tactic: refine (IsClosedEmbedding.of_continuous_injective_isClosedMap ?_
    (Equiv.injective _) ?_).isInducing
-- 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
⊢ Continuous (X := Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)) (Y := PrimeSpectrum (R × S))
    (⇑(Equiv.symm (primeSpectrumProd R S)) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
have refine_1 : Continuous (X := PrimeSpectrum R) (Y := PrimeSpectrum (R × S))
    (Function.comp (β := Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S))
      (⇑(Equiv.symm (primeSpectrumProd R S)) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
      Sum.inl) ∧
  Continuous (X := PrimeSpectrum S) (Y := PrimeSpectrum (R × S))
    (Function.comp (β := Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S))
      (⇑(Equiv.symm (primeSpectrumProd R S)) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S)) Sum.inr)
Tactic: rw [continuous_sum_dom]
-- 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
⊢ Continuous (X := PrimeSpectrum R) (Y := PrimeSpectrum (R × S))
      (Function.comp (β := Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S))
        (⇑(Equiv.symm (primeSpectrumProd R S)) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        Sum.inl) ∧
    Continuous (X := PrimeSpectrum S) (Y := PrimeSpectrum (R × S))
      (Function.comp (β := Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S))
        (⇑(Equiv.symm (primeSpectrumProd R S)) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        Sum.inr)
have refine_1 : (Continuous (Y := PrimeSpectrum (R × S)) fun (x : PrimeSpectrum R) ↦ comap (RingHom.fst R S) x) ∧
  Continuous (Y := PrimeSpectrum (R × S)) fun (x : PrimeSpectrum S) ↦ comap (RingHom.snd R S) x
Tactic: simp only [Function.comp_def, primeSpectrumProd_symm_inl, primeSpectrumProd_symm_inr]
-- 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
⊢ IsClosedMap (X := Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)) (Y := PrimeSpectrum (R × S))
    (⇑(Equiv.symm (primeSpectrumProd R S)) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
have refine_2 : (IsClosedMap (Y := PrimeSpectrum (R × S)) fun (a : PrimeSpectrum R) ↦ comap (RingHom.fst R S) a) ∧
  IsClosedMap (Y := PrimeSpectrum (R × S)) fun (b : PrimeSpectrum S) ↦ comap (RingHom.snd R S) b
Tactic: simp_rw [isClosedMap_sum, primeSpectrumProd_symm_inl, primeSpectrumProd_symm_inr]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
f g : R
⊢ LE.le (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen f) (basicOpen g) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {g})) f
have rw : (↑(basicOpen f) : Set (PrimeSpectrum R)) ⊆ (↑(basicOpen g) : Set (PrimeSpectrum R)) ↔
  Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {g})) f
Tactic: rw [← SetLike.coe_subset_coe, basicOpen_eq_zeroLocus_compl, basicOpen_eq_zeroLocus_compl,
    Set.compl_subset_compl, zeroLocus_subset_zeroLocus_singleton_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
f g : R
rw :
  (↑(basicOpen f) : Set (PrimeSpectrum R)) ⊆ (↑(basicOpen g) : Set (PrimeSpectrum R)) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {g})) f
⊢ LE.le (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen f) (basicOpen g) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {g})) f
have rw₁ : (zeroLocus {f})ᶜ ⊆ (↑(basicOpen g) : Set (PrimeSpectrum R)) ↔
  Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {g})) f
Tactic: rw [← SetLike.coe_subset_coe, basicOpen_eq_zeroLocus_compl, basicOpen_eq_zeroLocus_compl,
    Set.compl_subset_compl, zeroLocus_subset_zeroLocus_singleton_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
f g : R
rw :
  (↑(basicOpen f) : Set (PrimeSpectrum R)) ⊆ (↑(basicOpen g) : Set (PrimeSpectrum R)) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {g})) f
rw₁ :
  (zeroLocus {f})ᶜ ⊆ (↑(basicOpen g) : Set (PrimeSpectrum R)) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {g})) f
⊢ LE.le (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen f) (basicOpen g) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {g})) f
have rw₂ : Subset (α := Set (PrimeSpectrum R)) (zeroLocus {f})ᶜ (zeroLocus {g})ᶜ ↔
  Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {g})) f
Tactic: rw [← SetLike.coe_subset_coe, basicOpen_eq_zeroLocus_compl, basicOpen_eq_zeroLocus_compl,
    Set.compl_subset_compl, zeroLocus_subset_zeroLocus_singleton_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
f g : R
rw :
  (↑(basicOpen f) : Set (PrimeSpectrum R)) ⊆ (↑(basicOpen g) : Set (PrimeSpectrum R)) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {g})) f
rw₁ :
  (zeroLocus {f})ᶜ ⊆ (↑(basicOpen g) : Set (PrimeSpectrum R)) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {g})) f
rw₂ :
  Subset (α := Set (PrimeSpectrum R)) (zeroLocus {f})ᶜ (zeroLocus {g})ᶜ ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {g})) f
⊢ LE.le (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen f) (basicOpen g) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {g})) f
have rw₃ : Subset (α := Set (PrimeSpectrum R)) (zeroLocus {g}) (zeroLocus {f}) ↔
  Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {g})) f
Tactic: rw [← SetLike.coe_subset_coe, basicOpen_eq_zeroLocus_compl, basicOpen_eq_zeroLocus_compl,
    Set.compl_subset_compl, zeroLocus_subset_zeroLocus_singleton_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
f g : R
rw :
  (↑(basicOpen f) : Set (PrimeSpectrum R)) ⊆ (↑(basicOpen g) : Set (PrimeSpectrum R)) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {g})) f
rw₁ :
  (zeroLocus {f})ᶜ ⊆ (↑(basicOpen g) : Set (PrimeSpectrum R)) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {g})) f
rw₂ :
  Subset (α := Set (PrimeSpectrum R)) (zeroLocus {f})ᶜ (zeroLocus {g})ᶜ ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {g})) f
rw₃ :
  Subset (α := Set (PrimeSpectrum R)) (zeroLocus {g}) (zeroLocus {f}) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {g})) f
⊢ LE.le (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen f) (basicOpen g) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {g})) f
have rw₄ : Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {g})) f ↔
  Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {g})) f
Tactic: rw [← SetLike.coe_subset_coe, basicOpen_eq_zeroLocus_compl, basicOpen_eq_zeroLocus_compl,
    Set.compl_subset_compl, zeroLocus_subset_zeroLocus_singleton_iff]
-- 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
f g : R
inst_2 : Algebra R S
inst_3 : IsLocalization.Away f S
⊢ LE.le (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen f) (basicOpen g) ↔
    IsUnit.{v} (M := S) ((algebraMap R S : (a : R) → S) g : S)
have simp_rw : Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {g})) f ↔
  IsUnit.{v} (M := S) ((algebraMap R S : (a : R) → S) g : S)
Tactic: simp_rw [basicOpen_le_basicOpen_iff, Ideal.mem_radical_iff, Ideal.mem_span_singleton,
    IsLocalization.Away.algebraMap_isUnit_iff f]
-- 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
f g : R
inst_2 : Algebra R S
inst_3 : IsLocalization.Away f S
simp_rw :
  Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {g})) f ↔
    IsUnit.{v} (M := S) ((algebraMap R S : (a : R) → S) g : S)
⊢ LE.le (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen f) (basicOpen g) ↔
    IsUnit.{v} (M := S) ((algebraMap R S : (a : R) → S) g : S)
have simp_rw₁ : (∃ (n : ℕ), Membership.mem (γ := Ideal R) (Ideal.span {g}) (f ^ n)) ↔
  IsUnit.{v} (M := S) ((algebraMap R S : (a : R) → S) g : S)
Tactic: simp_rw [basicOpen_le_basicOpen_iff, Ideal.mem_radical_iff, Ideal.mem_span_singleton,
    IsLocalization.Away.algebraMap_isUnit_iff f]
-- 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
f g : R
inst_2 : Algebra R S
inst_3 : IsLocalization.Away f S
simp_rw :
  Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {g})) f ↔
    IsUnit.{v} (M := S) ((algebraMap R S : (a : R) → S) g : S)
simp_rw₁ :
  (∃ (n : ℕ), Membership.mem (γ := Ideal R) (Ideal.span {g}) (f ^ n)) ↔
    IsUnit.{v} (M := S) ((algebraMap R S : (a : R) → S) g : S)
⊢ LE.le (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen f) (basicOpen g) ↔
    IsUnit.{v} (M := S) ((algebraMap R S : (a : R) → S) g : S)
have simp_rw₂ : (∃ (n : ℕ), g ∣ f ^ n) ↔ IsUnit.{v} (M := S) ((algebraMap R S : (a : R) → S) g : S)
Tactic: simp_rw [basicOpen_le_basicOpen_iff, Ideal.mem_radical_iff, Ideal.mem_span_singleton,
    IsLocalization.Away.algebraMap_isUnit_iff f]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
f g : R
⊢ LE.le (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen (f * g)) (basicOpen f)
have rw : LE.le (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen f ⊓ basicOpen g) (basicOpen f)
Tactic: rw [basicOpen_mul f g]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
f g : R
⊢ LE.le (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen (f * g)) (basicOpen g)
have rw : LE.le (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen f ⊓ basicOpen g) (basicOpen g)
Tactic: rw [basicOpen_mul f g]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
r : R
n : ℕ
⊢ LE.le (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen r) (basicOpen (r ^ n))
have zero : LE.le (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen r) (basicOpen (HPow.hPow (β := ℕ) r 0))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
r : R
n : ℕ
zero : LE.le (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen r) (basicOpen (HPow.hPow (β := ℕ) r 0))
⊢ LE.le (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen r) (basicOpen (r ^ n))
have succ : ∀ (n : ℕ), LE.le (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen r) (basicOpen (r ^ (n + 1)))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
⊢ TopologicalSpace.IsTopologicalBasis.{u} (α := PrimeSpectrum R)
    (Set.range fun (r : R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R)))
have h_open : ∀ (u : Set (PrimeSpectrum R)),
  Membership.mem (γ := Set (Set (PrimeSpectrum R))) (Set.range fun (r : R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R)))
      u →
    IsOpen u
Tactic: apply TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
h_open :
  ∀ (u : Set (PrimeSpectrum R)),
    Membership.mem (γ := Set (Set (PrimeSpectrum R))) (Set.range fun (r : R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R)))
        u →
      IsOpen u
⊢ TopologicalSpace.IsTopologicalBasis.{u} (α := PrimeSpectrum R)
    (Set.range fun (r : R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R)))
have h_nhds : ∀ (a : PrimeSpectrum R) (u : Set (PrimeSpectrum R)),
  a ∈ u →
    IsOpen u →
      ∃ (v : Set (PrimeSpectrum R)),
        Membership.mem (γ := Set (Set (PrimeSpectrum R)))
            (Set.range fun (r : R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R))) v ∧
          a ∈ v ∧ v ⊆ u
Tactic: apply TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
hp : p ∈ U
s : Set R
hs : zeroLocus s = Uᶜ
⊢ ∃ (v : Set (PrimeSpectrum R)),
    Membership.mem (γ := Set (Set (PrimeSpectrum R))) (Set.range fun (r : R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R)))
        v ∧
      p ∈ v ∧ v ⊆ U
have h_nhds : ∀ (s : Set R) (hp : ∃ a ∈ s, a ∉ (↑p.asIdeal : Set R)) (hs : zeroLocus s = Uᶜ),
  ∃ (v : Set (PrimeSpectrum R)),
    Membership.mem (γ := Set (Set (PrimeSpectrum R))) (Set.range fun (r : R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R)))
        v ∧
      p ∈ v ∧ v ⊆ U
Tactic: rw [← compl_compl U, Set.mem_compl_iff, ← hs, mem_zeroLocus, Set.not_subset] at hp
Cleared hypotheses: hp, s, hs
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
s : Set R
hp : ∃ a ∈ s, a ∉ (↑p.asIdeal : Set R)
hs : zeroLocus s = Uᶜ
⊢ ∃ (v : Set (PrimeSpectrum R)),
    Membership.mem (γ := Set (Set (PrimeSpectrum R))) (Set.range fun (r : R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R)))
        v ∧
      p ∈ v ∧ v ⊆ U
have h_nhds : ∀ (f : R) (hfs : f ∈ s) (hfp : f ∉ (↑p.asIdeal : Set R)),
  ∃ (v : Set (PrimeSpectrum R)),
    Membership.mem (γ := Set (Set (PrimeSpectrum R))) (Set.range fun (r : R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R)))
        v ∧
      p ∈ v ∧ v ⊆ U
Tactic: obtain ⟨f, hfs, hfp⟩ := hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
s : Set R
hs : zeroLocus s = Uᶜ
f : R
hfs : f ∈ s
hfp : f ∉ (↑p.asIdeal : Set R)
⊢ ∃ (v : Set (PrimeSpectrum R)),
    Membership.mem (γ := Set (Set (PrimeSpectrum R))) (Set.range fun (r : R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R)))
        v ∧
      p ∈ v ∧ v ⊆ U
have h_nhds : (↑(basicOpen f) : Set (PrimeSpectrum R)) ⊆ U
Tactic: refine ⟨basicOpen f, ⟨f, rfl⟩, hfp, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
s : Set R
hs : zeroLocus s = Uᶜ
f : R
hfs : f ∈ s
hfp : f ∉ (↑p.asIdeal : Set R)
⊢ (↑(basicOpen f) : Set (PrimeSpectrum R)) ⊆ U
have h_nhds : Subset (α := Set (PrimeSpectrum R)) (zeroLocus s) (zeroLocus {f})
Tactic: rw [← Set.compl_subset_compl, ← hs, basicOpen_eq_zeroLocus_compl, compl_compl]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
⊢ TopologicalSpace.IsTopologicalBasis
    (Set.image (α := TopologicalSpace.Opens (PrimeSpectrum R)) SetLike.coe (Set.range basicOpen))
have h : Set.image (α := TopologicalSpace.Opens (PrimeSpectrum R)) SetLike.coe (Set.range basicOpen) =
  Set.range fun (r : R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R))
Tactic: convert! isTopologicalBasis_basic_opens (R := R)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
⊢ Set.image (α := TopologicalSpace.Opens (PrimeSpectrum R)) SetLike.coe (Set.range basicOpen) =
    Set.range fun (r : R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R))
have h : Set.range (ι := R) (Function.comp (β := TopologicalSpace.Opens (PrimeSpectrum R)) SetLike.coe basicOpen) =
  Set.range fun (r : R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R))
Tactic: rw [← Set.range_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
f : R
⊢ Eq (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen f) ⊥ ↔ IsNilpotent f
have rw : (zeroLocus {f})ᶜ = (↑⊥ : Set (PrimeSpectrum R)) ↔ IsNilpotent f
Tactic: rw [← TopologicalSpace.Opens.coe_inj, basicOpen_eq_zeroLocus_compl]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
f : R
⊢ (zeroLocus {f})ᶜ = (↑⊥ : Set (PrimeSpectrum R)) ↔ IsNilpotent f
have simp : (∀ (x : PrimeSpectrum R), f ∈ x.asIdeal) ↔ ∀ (J : Ideal R), J.IsPrime → f ∈ J
Tactic: simp only [Set.eq_univ_iff_forall, Set.singleton_subset_iff, TopologicalSpace.Opens.coe_bot,
    nilpotent_iff_mem_prime, Set.compl_empty_iff, mem_zeroLocus, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
⊢ Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S)) = (↑(basicOpen r) : Set (PrimeSpectrum R))
have rw : {p : PrimeSpectrum R | Disjoint (↑(Submonoid.powers r) : Set R) (↑p.asIdeal : Set R)} =
  (↑(basicOpen r) : Set (PrimeSpectrum R))
Tactic: rw [localization_comap_range S (Submonoid.powers r)]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
⊢ {p : PrimeSpectrum R | Disjoint (↑(Submonoid.powers r) : Set R) (↑p.asIdeal : Set R)} =
    (↑(basicOpen r) : Set (PrimeSpectrum R))
have h : ∀ (x : PrimeSpectrum R),
  Membership.mem (γ := Set (PrimeSpectrum R))
      {p : PrimeSpectrum R | Disjoint (↑(Submonoid.powers r) : Set R) (↑p.asIdeal : Set R)} x ↔
    x ∈ (↑(basicOpen r) : Set (PrimeSpectrum R))
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
x : PrimeSpectrum R
⊢ Membership.mem (γ := Set (PrimeSpectrum R))
      {p : PrimeSpectrum R | Disjoint (↑(Submonoid.powers r) : Set R) (↑p.asIdeal : Set R)} x ↔
    x ∈ (↑(basicOpen r) : Set (PrimeSpectrum R))
have h : (↑(Submonoid.powers r) : Set R) ⊓ (↑x.asIdeal : Set R) ≤ ⊥ ↔ r ∉ x.asIdeal
Tactic: simp only [mem_zeroLocus, basicOpen_eq_zeroLocus_compl, SetLike.mem_coe, Set.mem_setOf_eq,
    Set.singleton_subset_iff, Set.mem_compl_iff, disjoint_iff_inf_le]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
x : PrimeSpectrum R
⊢ (↑(Submonoid.powers r) : Set R) ⊓ (↑x.asIdeal : Set R) ≤ ⊥ ↔ r ∉ x.asIdeal
have h : (↑(Submonoid.powers r) : Set R) ⊓ (↑x.asIdeal : Set R) ≤ ⊥ → r ∉ x.asIdeal
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
x : PrimeSpectrum R
h : (↑(Submonoid.powers r) : Set R) ⊓ (↑x.asIdeal : Set R) ≤ ⊥ → r ∉ x.asIdeal
⊢ (↑(Submonoid.powers r) : Set R) ⊓ (↑x.asIdeal : Set R) ≤ ⊥ ↔ r ∉ x.asIdeal
have h₁ : r ∉ x.asIdeal → (↑(Submonoid.powers r) : Set R) ⊓ (↑x.asIdeal : Set R) ≤ ⊥
Tactic: constructor