-- 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'
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'
h_nhds :
  Membership.mem (γ := Set ↥X)
    (Set.range (ι :=
      ↥(X.affineBasisCover.X
          (Sigma.mk (β := fun (i : X.affineCover.I₀) ↦
            PreZeroHypercover.I₀ (C := Scheme) (S := X.affineCover.X i)
              ((fun (i : X.affineCover.I₀) ↦
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                      ((fun (x : X.affineCover.I₀) ↦
                          (affineBasisCoverOfAffine
                              ((fun (x : (↑X.toTopCat : Type u)) ↦
                                  Classical.choose (p := fun (R : CommRingCat.{u}) ↦
                                    Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))) ⋯)
                                x) :
                            (Spec
                                ((fun (x : (↑X.toTopCat : Type u)) ↦
                                    Classical.choose (p := fun (R : CommRingCat.{u}) ↦
                                      Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))) ⋯)
                                  x)).OpenCover))
                        i) :
                    PreZeroHypercover (X.affineCover.X i)))
                i))
            (Cover.idx X.affineCover a) s)))
      ⇑(X.affineBasisCover.f
          (Sigma.mk (β := fun (i : X.affineCover.I₀) ↦
            PreZeroHypercover.I₀ (C := Scheme) (S := X.affineCover.X i)
              ((fun (i : X.affineCover.I₀) ↦
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                      ((fun (x : X.affineCover.I₀) ↦
                          (affineBasisCoverOfAffine
                              ((fun (x : (↑X.toTopCat : Type u)) ↦
                                  Classical.choose (p := fun (R : CommRingCat.{u}) ↦
                                    Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))) ⋯)
                                x) :
                            (Spec
                                ((fun (x : (↑X.toTopCat : Type u)) ↦
                                    Classical.choose (p := fun (R : CommRingCat.{u}) ↦
                                      Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))) ⋯)
                                  x)).OpenCover))
                        i) :
                    PreZeroHypercover (X.affineCover.X i)))
                i))
            (Cover.idx X.affineCover a) s)))
    a
⊢ ∃ (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₁ : Set.range (ι :=
    ↥(X.affineBasisCover.X
        (Sigma.mk (β := fun (i : X.affineCover.I₀) ↦
          PreZeroHypercover.I₀ (C := Scheme) (S := X.affineCover.X i)
            ((fun (i : X.affineCover.I₀) ↦
                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                    ((fun (x : X.affineCover.I₀) ↦
                        (affineBasisCoverOfAffine
                            ((fun (x : (↑X.toTopCat : Type u)) ↦
                                Classical.choose (p := fun (R : CommRingCat.{u}) ↦
                                  Nonempty.{u + 1} (X.restrict sorry ≅ Spec.toLocallyRingedSpace.obj (op R))) sorry)
                              x) :
                          (Spec
                              ((fun (x : (↑X.toTopCat : Type u)) ↦
                                  Classical.choose (p := fun (R : CommRingCat.{u}) ↦
                                    Nonempty.{u + 1} (X.restrict sorry ≅ Spec.toLocallyRingedSpace.obj (op R))) sorry)
                                x)).OpenCover))
                      i) :
                  PreZeroHypercover (X.affineCover.X i)))
              i))
          (Cover.idx X.affineCover a) s)))
    ⇑(X.affineBasisCover.f
        (Sigma.mk (β := fun (i : X.affineCover.I₀) ↦
          PreZeroHypercover.I₀ (C := Scheme) (S := X.affineCover.X i)
            ((fun (i : X.affineCover.I₀) ↦
                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                    ((fun (x : X.affineCover.I₀) ↦
                        (affineBasisCoverOfAffine
                            ((fun (x : (↑X.toTopCat : Type u)) ↦
                                Classical.choose (p := fun (R : CommRingCat.{u}) ↦
                                  Nonempty.{u + 1} (X.restrict sorry ≅ Spec.toLocallyRingedSpace.obj (op R))) sorry)
                              x) :
                          (Spec
                              ((fun (x : (↑X.toTopCat : Type u)) ↦
                                  Classical.choose (p := fun (R : CommRingCat.{u}) ↦
                                    Nonempty.{u + 1} (X.restrict sorry ≅ Spec.toLocallyRingedSpace.obj (op R))) sorry)
                                x)).OpenCover))
                      i) :
                  PreZeroHypercover (X.affineCover.X i)))
              i))
          (Cover.idx X.affineCover a) s)) ⊆
  U
Tactic: refine ⟨_, ⟨⟨_, s⟩, rfl⟩, ?_, ?_⟩