-- 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
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

Tactic:
have hxU' : x ∈ U' := by rw [← e] at haU; exact haU

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
hxU' : x ∈ 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
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

Tactic:
refine ⟨_, ⟨⟨_, s⟩, rfl⟩, ?_, ?_⟩ <;> rw [affineBasisCover_map_range]

Result:
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

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

Proof state:
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

Tactic:
rintro a U haU hU

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

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

Tactic:
rcases X.affineCover.covers a with ⟨x, e⟩

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
⊢ ∃ v ∈ {x | ∃ a, x = Set.range ⇑(ConcreteCategory.hom (X.affineBasisCover.map a).base)}, a ∈ v ∧ v ⊆ U