-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
a : ↥X
U : Set ↥X
haU : a ∈ U
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
hxU' : x ∈ U'
h_nhds :
  ∀
    (s :
      (↑((fun (x : (↑X.toTopCat : Type u)) ↦
              Classical.choose (p := fun (R : CommRingCat.{u}) ↦
                Nonempty.{u + 1}
                  (X.restrict (U :=
                      Functor.obj (C := TopologicalSpace.Opens (↑X.toTopCat : Type u)) (Opens.toTopCat X.toTopCat)
                        (↑((fun (x : (↑X.toTopCat : Type u)) ↦
                                Classical.choose (p := fun (U : OpenNhds x) ↦
                                  ∃ (R : CommRingCat.{u}),
                                    Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)))
                                  ⋯)
                              x) :
                          TopologicalSpace.Opens (↑X.toTopCat : Type u)))
                      (f :=
                      (Opens.inclusion'
                          (↑((fun (x : (↑X.toTopCat : Type u)) ↦
                                  Classical.choose (p := fun (U : OpenNhds x) ↦
                                    ∃ (R : CommRingCat.{u}),
                                      Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)))
                                    ⋯)
                                x) :
                            TopologicalSpace.Opens (↑X.toTopCat : Type u)) :
                        Functor.obj (C := TopologicalSpace.Opens (↑X.toTopCat : Type u)) (Opens.toTopCat X.toTopCat)
                            (↑((fun (x : (↑X.toTopCat : Type u)) ↦
                                    Classical.choose (p := fun (U : OpenNhds x) ↦
                                      ∃ (R : CommRingCat.{u}),
                                        Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)))
                                      ⋯)
                                  x) :
                              TopologicalSpace.Opens (↑X.toTopCat : Type u)) ⟶
                          X.toTopCat))
                      ⋯ ≅
                    Spec.toLocallyRingedSpace.obj (op R)))
                ⋯)
            (Cover.idx X.affineCover a)) :
        Type u))
    (hxV :
      x ∈
        (↑(PrimeSpectrum.basicOpen s) :
          Set
            (PrimeSpectrum
              (↑((fun (x : (↑X.toTopCat : Type u)) ↦ Classical.choose ⋯) (Cover.idx X.affineCover a)) : Type u))))
    (hVU :
      (↑(PrimeSpectrum.basicOpen s) :
          Set
            (PrimeSpectrum
              (↑((fun (x : (↑X.toTopCat : Type u)) ↦ Classical.choose ⋯) (Cover.idx X.affineCover a)) : Type u))) ⊆
        U'),
    ∃ (v : Set ↥X),
      Membership.mem (γ := Set (Set ↥X))
          {x : Set ↥X |
            ∃ (a : X.affineBasisCover.I₀), x = Set.range (ι := ↥(X.affineBasisCover.X a)) ⇑(X.affineBasisCover.f a)}
          v ∧
        a ∈ v ∧ v ⊆ U
⊢ ∃ (v : Set ↥X),
    Membership.mem (γ := Set (Set ↥X))
        {x : Set ↥X |
          ∃ (a : X.affineBasisCover.I₀), x = Set.range (ι := ↥(X.affineBasisCover.X a)) ⇑(X.affineBasisCover.f a)}
        v ∧
      a ∈ v ∧ v ⊆ U

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

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.Hom.continuous, AlgebraicGeometry.Scheme.Cover.idx, AlgebraicGeometry.Scheme.affineCover, Continuous.isOpen_preimage, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, PrimeSpectrum.isBasis_basic_opens, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open