-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem isTopologicalBasis_basic_opens :
    TopologicalSpace.IsTopologicalBasis
      (Set.range fun r : R => (basicOpen r : Set (PrimeSpectrum R)))

Proof state:
case h_nhds.intro.intro.intro
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
⊢ ↑(basicOpen f) ⊆ U

Tactic:
rw [← Set.compl_subset_compl, ← hs, basicOpen_eq_zeroLocus_compl, compl_compl]

Result:
case h_nhds.intro.intro.intro
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
⊢ zeroLocus s ⊆ zeroLocus {f}

Proof state:
case h_nhds.intro.intro.intro
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
⊢ zeroLocus s ⊆ zeroLocus {f}

Tactic:
exact zeroLocus_anti_mono (Set.singleton_subset_iff.mpr hfs)

Result:
no goals

Proof state:
case h_nhds
R : Type u
inst✝ : CommSemiring R
⊢ ∀ (a : PrimeSpectrum R) (u : Set (PrimeSpectrum R)),
    a ∈ u → IsOpen u → ∃ v ∈ Set.range fun r => ↑(basicOpen r), a ∈ v ∧ v ⊆ u

Tactic:
rintro p U hp ⟨s, hs⟩

Result:
case h_nhds.intro
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.range fun r => ↑(basicOpen r), p ∈ v ∧ v ⊆ U

Proof state:
case h_open.intro
R : Type u
inst✝ : CommSemiring R
r : R
⊢ IsOpen ((fun r => ↑(basicOpen r)) r)

Tactic:
exact isOpen_basicOpen

Result:
no goals

Proof state:
case h_nhds.intro
R : Type u
inst✝ : CommSemiring R
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
s : Set R
hp : ∃ a ∈ s, a ∉ ↑p.asIdeal
hs : zeroLocus s = Uᶜ
⊢ ∃ v ∈ Set.range fun r => ↑(basicOpen r), p ∈ v ∧ v ⊆ U

Tactic:
obtain ⟨f, hfs, hfp⟩ := hp

Result:
case h_nhds.intro.intro.intro
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
⊢ ∃ v ∈ Set.range fun r => ↑(basicOpen r), p ∈ v ∧ v ⊆ U

Proof state:
case h_nhds.intro
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.range fun r => ↑(basicOpen r), p ∈ v ∧ v ⊆ U

Tactic:
rw [← compl_compl U, Set.mem_compl_iff, ← hs, mem_zeroLocus, Set.not_subset] at hp

Result:
case h_nhds.intro
R : Type u
inst✝ : CommSemiring R
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
s : Set R
hp : ∃ a ∈ s, a ∉ ↑p.asIdeal
hs : zeroLocus s = Uᶜ
⊢ ∃ v ∈ Set.range fun r => ↑(basicOpen r), p ∈ v ∧ v ⊆ U

Proof state:
case h_nhds.intro.intro.intro
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
⊢ ∃ v ∈ Set.range fun r => ↑(basicOpen r), p ∈ v ∧ v ⊆ U

Tactic:
refine ⟨basicOpen f, ⟨f, rfl⟩, hfp, ?_⟩

Result:
case h_nhds.intro.intro.intro
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
⊢ ↑(basicOpen f) ⊆ U

Proof state:
case h_open
R : Type u
inst✝ : CommSemiring R
⊢ ∀ u ∈ Set.range fun r => ↑(basicOpen r), IsOpen u

Tactic:
rintro _ ⟨r, rfl⟩

Result:
case h_open.intro
R : Type u
inst✝ : CommSemiring R
r : R
⊢ IsOpen ((fun r => ↑(basicOpen r)) r)

Proof state:
R : Type u
inst✝ : CommSemiring R
⊢ TopologicalSpace.IsTopologicalBasis (Set.range fun r => ↑(basicOpen r))

Tactic:
apply TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds

Result:
case h_open
R : Type u
inst✝ : CommSemiring R
⊢ ∀ u ∈ Set.range fun r => ↑(basicOpen r), IsOpen u

case h_nhds
R : Type u
inst✝ : CommSemiring R
⊢ ∀ (a : PrimeSpectrum R) (u : Set (PrimeSpectrum R)),
    a ∈ u → IsOpen u → ∃ v ∈ Set.range fun r => ↑(basicOpen r), a ∈ v ∧ v ⊆ u