-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean
theorem isTopologicalBasis_basic_opens :
    TopologicalSpace.IsTopologicalBasis
      (Set.range fun r : A => (basicOpen 𝒜 r : Set (ProjectiveSpectrum 𝒜)))

Proof state:
case h_nhds.intro.intro.intro
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
s : Set A
hs : zeroLocus 𝒜 s = Uᶜ
f : A
hfs : f ∈ s
hfp : f ∉ ↑p.asHomogeneousIdeal
⊢ ↑(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_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
s : Set A
hs : zeroLocus 𝒜 s = Uᶜ
f : A
hfs : f ∈ s
hfp : f ∉ ↑p.asHomogeneousIdeal
⊢ zeroLocus 𝒜 s ⊆ zeroLocus 𝒜 {f}

Proof state:
case h_open.intro
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
r : A
⊢ IsOpen ((fun r => ↑(basicOpen 𝒜 r)) r)

Tactic:
exact isOpen_basicOpen 𝒜

Result:
no goals

Proof state:
case h_nhds.intro.intro.intro
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
s : Set A
hs : zeroLocus 𝒜 s = Uᶜ
f : A
hfs : f ∈ s
hfp : f ∉ ↑p.asHomogeneousIdeal
⊢ zeroLocus 𝒜 s ⊆ zeroLocus 𝒜 {f}

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

Result:
no goals

Proof state:
case h_nhds.intro
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
hp : p ∈ U
s : Set A
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_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
s : Set A
hp : ∃ a ∈ s, a ∉ ↑p.asHomogeneousIdeal
hs : zeroLocus 𝒜 s = Uᶜ
⊢ ∃ v ∈ Set.range fun r => ↑(basicOpen 𝒜 r), p ∈ v ∧ v ⊆ U

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
⊢ IsTopologicalBasis (Set.range fun r => ↑(basicOpen 𝒜 r))

Tactic:
apply TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds

Result:
case h_open
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
⊢ ∀ u ∈ Set.range fun r => ↑(basicOpen 𝒜 r), IsOpen u

case h_nhds
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
⊢ ∀ (a : ProjectiveSpectrum 𝒜) (u : Set (ProjectiveSpectrum 𝒜)),
    a ∈ u → IsOpen u → ∃ v ∈ Set.range fun r => ↑(basicOpen 𝒜 r), a ∈ v ∧ v ⊆ u

Proof state:
case h_nhds
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
⊢ ∀ (a : ProjectiveSpectrum 𝒜) (u : Set (ProjectiveSpectrum 𝒜)),
    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_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
hp : p ∈ U
s : Set A
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_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
s : Set A
hs : zeroLocus 𝒜 s = Uᶜ
f : A
hfs : f ∈ s
hfp : f ∉ ↑p.asHomogeneousIdeal
⊢ ∃ 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_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
s : Set A
hs : zeroLocus 𝒜 s = Uᶜ
f : A
hfs : f ∈ s
hfp : f ∉ ↑p.asHomogeneousIdeal
⊢ ↑(basicOpen 𝒜 f) ⊆ U

Proof state:
case h_open
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
⊢ ∀ u ∈ Set.range fun r => ↑(basicOpen 𝒜 r), IsOpen u

Tactic:
rintro _ ⟨r, rfl⟩

Result:
case h_open.intro
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
r : A
⊢ IsOpen ((fun r => ↑(basicOpen 𝒜 r)) r)

Proof state:
case h_nhds.intro
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
s : Set A
hp : ∃ a ∈ s, a ∉ ↑p.asHomogeneousIdeal
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_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
s : Set A
hs : zeroLocus 𝒜 s = Uᶜ
f : A
hfs : f ∈ s
hfp : f ∉ ↑p.asHomogeneousIdeal
⊢ ∃ v ∈ Set.range fun r => ↑(basicOpen 𝒜 r), p ∈ v ∧ v ⊆ U