-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
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'
⊢ ∃ (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
have 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 sorry ≅ Spec.toLocallyRingedSpace.obj (op R)))
                                sorry)
                            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 sorry ≅ Spec.toLocallyRingedSpace.obj (op R)))
                                  sorry)
                              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 sorry ≅ Spec.toLocallyRingedSpace.obj (op R)))
                                    sorry)
                                x) :
                            TopologicalSpace.Opens (↑X.toTopCat : Type u)) ⟶
                        X.toTopCat))
                    sorry ≅
                  Spec.toLocallyRingedSpace.obj (op R)))
              sorry)
          (Cover.idx X.affineCover a)) :
      Type u))
  (hxV :
    x ∈
      (↑(PrimeSpectrum.basicOpen s) :
        Set
          (PrimeSpectrum
            (↑((fun (x : (↑X.toTopCat : Type u)) ↦ Classical.choose sorry) (Cover.idx X.affineCover a)) : Type u))))
  (hVU :
    (↑(PrimeSpectrum.basicOpen s) :
        Set
          (PrimeSpectrum
            (↑((fun (x : (↑X.toTopCat : Type u)) ↦ Classical.choose sorry) (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
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⟩