-- Mathlib/AlgebraicGeometry/Cover/Open.lean
theorem affineBasisCover_is_basis (X : Scheme.{u}) :
    TopologicalSpace.IsTopologicalBasis
      {x : Set X |
        ∃ a : X.affineBasisCover.J, x = Set.range (X.affineBasisCover.map a).base}

Proof state:
case h_nhds.intro.intro.intro.intro.intro.intro.intro.refine_2
X : Scheme
a : ↑↑X.toPresheafedSpace
U : Set ↑↑X.toPresheafedSpace
haU : a ∈ U
hU : IsOpen U
x : ↑↑(X.affineCover.obj (X.affineCover.f a)).toPresheafedSpace
e : (ConcreteCategory.hom (X.affineCover.map (X.affineCover.f a)).base) x = a
U' : Set ↑↑(X.affineCover.obj (X.affineCover.f a)).toPresheafedSpace :=
  ⇑(ConcreteCategory.hom (X.affineCover.map (X.affineCover.f a)).base) ⁻¹' U
hxU' : x ∈ U'
s : ↑⋯.choose
hxV : x ∈ ↑(PrimeSpectrum.basicOpen s)
hVU : ↑(PrimeSpectrum.basicOpen s) ⊆ U'
⊢ ⇑(ConcreteCategory.hom (X.affineCover.map (X.affineCover.f a)).base) '' (PrimeSpectrum.basicOpen s).carrier ⊆ U

Tactic:
rw [Set.image_subset_iff]

Result:
case h_nhds.intro.intro.intro.intro.intro.intro.intro.refine_2
X : Scheme
a : ↑↑X.toPresheafedSpace
U : Set ↑↑X.toPresheafedSpace
haU : a ∈ U
hU : IsOpen U
x : ↑↑(X.affineCover.obj (X.affineCover.f a)).toPresheafedSpace
e : (ConcreteCategory.hom (X.affineCover.map (X.affineCover.f a)).base) x = a
U' : Set ↑↑(X.affineCover.obj (X.affineCover.f a)).toPresheafedSpace :=
  ⇑(ConcreteCategory.hom (X.affineCover.map (X.affineCover.f a)).base) ⁻¹' U
hxU' : x ∈ U'
s : ↑⋯.choose
hxV : x ∈ ↑(PrimeSpectrum.basicOpen s)
hVU : ↑(PrimeSpectrum.basicOpen s) ⊆ U'
⊢ (PrimeSpectrum.basicOpen s).carrier ⊆ ⇑(ConcreteCategory.hom (X.affineCover.map (X.affineCover.f a)).base) ⁻¹' U

Proof state:
X : Scheme
a : ↑↑X.toPresheafedSpace
U : Set ↑↑X.toPresheafedSpace
hU : IsOpen U
x : ↑↑(X.affineCover.obj (X.affineCover.f a)).toPresheafedSpace
haU : (ConcreteCategory.hom (X.affineCover.map (X.affineCover.f a)).base) x ∈ U
e : (ConcreteCategory.hom (X.affineCover.map (X.affineCover.f a)).base) x = a
U' : Set ↑↑(X.affineCover.obj (X.affineCover.f a)).toPresheafedSpace :=
  ⇑(ConcreteCategory.hom (X.affineCover.map (X.affineCover.f a)).base) ⁻¹' U
⊢ x ∈ U'

Tactic:
exact haU

Result:
no goals

Proof state:
X : Scheme
a : ↑↑X.toPresheafedSpace
U : Set ↑↑X.toPresheafedSpace
haU : a ∈ U
hU : IsOpen U
x : ↑↑(X.affineCover.obj (X.affineCover.f a)).toPresheafedSpace
e : (ConcreteCategory.hom (X.affineCover.map (X.affineCover.f a)).base) x = a
U' : Set ↑↑(X.affineCover.obj (X.affineCover.f a)).toPresheafedSpace :=
  ⇑(ConcreteCategory.hom (X.affineCover.map (X.affineCover.f a)).base) ⁻¹' U
⊢ x ∈ U'

Tactic:
rw [← e] at haU

Result:
X : Scheme
a : ↑↑X.toPresheafedSpace
U : Set ↑↑X.toPresheafedSpace
hU : IsOpen U
x : ↑↑(X.affineCover.obj (X.affineCover.f a)).toPresheafedSpace
haU : (ConcreteCategory.hom (X.affineCover.map (X.affineCover.f a)).base) x ∈ U
e : (ConcreteCategory.hom (X.affineCover.map (X.affineCover.f a)).base) x = a
U' : Set ↑↑(X.affineCover.obj (X.affineCover.f a)).toPresheafedSpace :=
  ⇑(ConcreteCategory.hom (X.affineCover.map (X.affineCover.f a)).base) ⁻¹' U
⊢ x ∈ U'

Proof state:
case h_nhds.intro
X : Scheme
a : ↑↑X.toPresheafedSpace
U : Set ↑↑X.toPresheafedSpace
haU : a ∈ U
hU : IsOpen U
x : ↑↑(X.affineCover.obj (X.affineCover.f a)).toPresheafedSpace
e : (ConcreteCategory.hom (X.affineCover.map (X.affineCover.f a)).base) x = a
U' : Set ↑↑(X.affineCover.obj (X.affineCover.f a)).toPresheafedSpace :=
  ⇑(ConcreteCategory.hom (X.affineCover.map (X.affineCover.f a)).base) ⁻¹' U
hxU' : x ∈ U'
⊢ ∃ v ∈ {x | ∃ a, x = Set.range ⇑(ConcreteCategory.hom (X.affineBasisCover.map a).base)}, a ∈ v ∧ v ⊆ U

Tactic:
rcases PrimeSpectrum.isBasis_basic_opens.exists_subset_of_mem_open hxU'
    ((X.affineCover.map (X.affineCover.f a)).base.hom.continuous_toFun.isOpen_preimage _
      hU) with
  ⟨_, ⟨_, ⟨s, rfl⟩, rfl⟩, hxV, hVU⟩

Result:
case h_nhds.intro.intro.intro.intro.intro.intro.intro
X : Scheme
a : ↑↑X.toPresheafedSpace
U : Set ↑↑X.toPresheafedSpace
haU : a ∈ U
hU : IsOpen U
x : ↑↑(X.affineCover.obj (X.affineCover.f a)).toPresheafedSpace
e : (ConcreteCategory.hom (X.affineCover.map (X.affineCover.f a)).base) x = a
U' : Set ↑↑(X.affineCover.obj (X.affineCover.f a)).toPresheafedSpace :=
  ⇑(ConcreteCategory.hom (X.affineCover.map (X.affineCover.f a)).base) ⁻¹' U
hxU' : x ∈ U'
s : ↑⋯.choose
hxV : x ∈ ↑(PrimeSpectrum.basicOpen s)
hVU : ↑(PrimeSpectrum.basicOpen s) ⊆ U'
⊢ ∃ v ∈ {x | ∃ a, x = Set.range ⇑(ConcreteCategory.hom (X.affineBasisCover.map a).base)}, a ∈ v ∧ v ⊆ U

Proof state:
case h_open
X : Scheme
⊢ ∀ u ∈ {x | ∃ a, x = Set.range ⇑(ConcreteCategory.hom (X.affineBasisCover.map a).base)}, IsOpen u

Tactic:
rintro _ ⟨a, rfl⟩

Result:
case h_open.intro
X : Scheme
a : X.affineBasisCover.J
⊢ IsOpen (Set.range ⇑(ConcreteCategory.hom (X.affineBasisCover.map a).base))

Proof state:
case h_nhds.intro
X : Scheme
a : ↑↑X.toPresheafedSpace
U : Set ↑↑X.toPresheafedSpace
haU : a ∈ U
hU : IsOpen U
x : ↑↑(X.affineCover.obj (X.affineCover.f a)).toPresheafedSpace
e : (ConcreteCategory.hom (X.affineCover.map (X.affineCover.f a)).base) x = a
⊢ ∃ v ∈ {x | ∃ a, x = Set.range ⇑(ConcreteCategory.hom (X.affineBasisCover.map a).base)}, a ∈ v ∧ v ⊆ U

Tactic:
let U' := (X.affineCover.map (X.affineCover.f a)).base ⁻¹' U

Result:
case h_nhds.intro
X : Scheme
a : ↑↑X.toPresheafedSpace
U : Set ↑↑X.toPresheafedSpace
haU : a ∈ U
hU : IsOpen U
x : ↑↑(X.affineCover.obj (X.affineCover.f a)).toPresheafedSpace
e : (ConcreteCategory.hom (X.affineCover.map (X.affineCover.f a)).base) x = a
U' : Set ↑↑(X.affineCover.obj (X.affineCover.f a)).toPresheafedSpace :=
  ⇑(ConcreteCategory.hom (X.affineCover.map (X.affineCover.f a)).base) ⁻¹' U
⊢ ∃ v ∈ {x | ∃ a, x = Set.range ⇑(ConcreteCategory.hom (X.affineBasisCover.map a).base)}, a ∈ v ∧ v ⊆ U

Proof state:
case h_nhds.intro.intro.intro.intro.intro.intro.intro.refine_2
X : Scheme
a : ↑↑X.toPresheafedSpace
U : Set ↑↑X.toPresheafedSpace
haU : a ∈ U
hU : IsOpen U
x : ↑↑(X.affineCover.obj (X.affineCover.f a)).toPresheafedSpace
e : (ConcreteCategory.hom (X.affineCover.map (X.affineCover.f a)).base) x = a
U' : Set ↑↑(X.affineCover.obj (X.affineCover.f a)).toPresheafedSpace :=
  ⇑(ConcreteCategory.hom (X.affineCover.map (X.affineCover.f a)).base) ⁻¹' U
hxU' : x ∈ U'
s : ↑⋯.choose
hxV : x ∈ ↑(PrimeSpectrum.basicOpen s)
hVU : ↑(PrimeSpectrum.basicOpen s) ⊆ U'
⊢ (PrimeSpectrum.basicOpen s).carrier ⊆ ⇑(ConcreteCategory.hom (X.affineCover.map (X.affineCover.f a)).base) ⁻¹' U

Tactic:
exact hVU

Result:
no goals

Proof state:
case h_nhds.intro.intro.intro.intro.intro.intro.intro.refine_1
X : Scheme
a : ↑↑X.toPresheafedSpace
U : Set ↑↑X.toPresheafedSpace
haU : a ∈ U
hU : IsOpen U
x : ↑↑(X.affineCover.obj (X.affineCover.f a)).toPresheafedSpace
e : (ConcreteCategory.hom (X.affineCover.map (X.affineCover.f a)).base) x = a
U' : Set ↑↑(X.affineCover.obj (X.affineCover.f a)).toPresheafedSpace :=
  ⇑(ConcreteCategory.hom (X.affineCover.map (X.affineCover.f a)).base) ⁻¹' U
hxU' : x ∈ U'
s : ↑⋯.choose
hxV : x ∈ ↑(PrimeSpectrum.basicOpen s)
hVU : ↑(PrimeSpectrum.basicOpen s) ⊆ U'
⊢ a ∈ ⇑(ConcreteCategory.hom (X.affineCover.map (X.affineCover.f a)).base) '' (PrimeSpectrum.basicOpen s).carrier

Tactic:
exact ⟨x, hxV, e⟩

Result:
no goals

Proof state:
case h_open.intro
X : Scheme
a : X.affineBasisCover.J
⊢ IsOpen (Set.range ⇑(ConcreteCategory.hom (X.affineBasisCover.map a).base))

Tactic:
exact IsOpenImmersion.isOpen_range (X.affineBasisCover.map a)

Result:
no goals

Proof state:
X : Scheme
⊢ IsTopologicalBasis {x | ∃ a, x = Set.range ⇑(ConcreteCategory.hom (X.affineBasisCover.map a).base)}

Tactic:
apply TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds

Result:
case h_open
X : Scheme
⊢ ∀ u ∈ {x | ∃ a, x = Set.range ⇑(ConcreteCategory.hom (X.affineBasisCover.map a).base)}, IsOpen u

case h_nhds
X : Scheme
⊢ ∀ (a : ↑↑X.toPresheafedSpace) (u : Set ↑↑X.toPresheafedSpace),
    a ∈ u →
      IsOpen u → ∃ v ∈ {x | ∃ a, x = Set.range ⇑(ConcreteCategory.hom (X.affineBasisCover.map a).base)}, a ∈ v ∧ v ⊆ u