-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
Goal:
X : Scheme
x : ↥X
r :
  (↑(⋯.choose (p := fun (R : CommRingCat.{u}) ↦
        Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)))) :
    Type u)
⊢ Eq (α := Set ↥X)
    (Set.image (α := ↥(X.affineCover.X x))
      (⇑(TopCat.Hom.hom (X.affineCover.f x).base) : (a : ↥(X.affineCover.X x)) → ↥X)
      (Set.range (ι :=
        ↥((X.affineCover.bind fun (i : X.affineCover.I₀) ↦
                Precoverage.ZeroHypercover.toPreZeroHypercover
                  (affineBasisCoverOfAffine
                    (Classical.choose (p := fun (R : CommRingCat.{u}) ↦
                      Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))) ⋯))).X
            (Sigma.mk (β := fun (i : X.affineCover.I₀) ↦
              PreZeroHypercover.I₀ (S := X.affineCover.X i)
                (Precoverage.ZeroHypercover.toPreZeroHypercover
                  (affineBasisCoverOfAffine
                    (Classical.choose (p := fun (R : CommRingCat.{u}) ↦
                      Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))) ⋯))))
              x r)))
        (⇑(TopCat.Hom.hom
                (PresheafedSpace.Hom.base
                  (LocallyRingedSpace.Hom.toHom
                    (Hom.toLRSHom'
                      (PreZeroHypercover.f
                        (Precoverage.ZeroHypercover.toPreZeroHypercover
                          (affineBasisCoverOfAffine
                            (Classical.choose (p := fun (R : CommRingCat.{u}) ↦
                              Nonempty.{u + 1}
                                (X.restrict (U :=
                                    Functor.obj (Opens.toTopCat X.toTopCat)
                                      (↑(Classical.choose (p := fun (U : OpenNhds x) ↦
                                            ∃ (R : CommRingCat.{u}),
                                              Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)))
                                            ⋯) :
                                        TopologicalSpace.Opens (↑X.toTopCat : Type u)))
                                    ⋯ ≅
                                  Spec.toLocallyRingedSpace.obj (op R)))
                              ⋯)))
                        r)))) :
              C(↥((X.affineCover.bind fun (i : X.affineCover.I₀) ↦
                        Precoverage.ZeroHypercover.toPreZeroHypercover
                          (affineBasisCoverOfAffine
                            (Classical.choose (p := fun (R : CommRingCat.{u}) ↦
                              Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))) ⋯))).X
                    (Sigma.mk (β := fun (i : X.affineCover.I₀) ↦
                      PreZeroHypercover.I₀ (S := X.affineCover.X i)
                        (Precoverage.ZeroHypercover.toPreZeroHypercover
                          (affineBasisCoverOfAffine
                            (Classical.choose (p := fun (R : CommRingCat.{u}) ↦
                              Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))) ⋯))))
                      x r)),
                ↥(X.affineCover.X x))) :
          (a :
              ↥((X.affineCover.bind fun (i : X.affineCover.I₀) ↦
                      (affineBasisCoverOfAffine (Classical.choose ⋯)).toPreZeroHypercover).X
                  ⟨x, r⟩)) →
            ↥(X.affineCover.X x))))
    ((fun (a : ↥(X.affineCover.X x)) ↦ (X.affineCover.f x) a) '' Opens.carrier (PrimeSpectrum.basicOpen r))
have e_s : Eq (α := Set ↥(X.affineCover.X x))
  (Set.range (ι :=
    ↥((X.affineCover.bind fun (i : X.affineCover.I₀) ↦
            Precoverage.ZeroHypercover.toPreZeroHypercover
              (affineBasisCoverOfAffine
                (Classical.choose (p := fun (R : CommRingCat.{u}) ↦
                  Nonempty.{u + 1} (X.restrict sorry ≅ Spec.toLocallyRingedSpace.obj (op R))) sorry))).X
        (Sigma.mk (β := fun (i : X.affineCover.I₀) ↦
          PreZeroHypercover.I₀ (S := X.affineCover.X i)
            (Precoverage.ZeroHypercover.toPreZeroHypercover
              (affineBasisCoverOfAffine
                (Classical.choose (p := fun (R : CommRingCat.{u}) ↦
                  Nonempty.{u + 1} (X.restrict sorry ≅ Spec.toLocallyRingedSpace.obj (op R))) sorry))))
          x r)))
    (⇑(TopCat.Hom.hom
            (PresheafedSpace.Hom.base
              (LocallyRingedSpace.Hom.toHom
                (Hom.toLRSHom'
                  (PreZeroHypercover.f
                    (Precoverage.ZeroHypercover.toPreZeroHypercover
                      (affineBasisCoverOfAffine
                        (Classical.choose (p := fun (R : CommRingCat.{u}) ↦
                          Nonempty.{u + 1}
                            (X.restrict (U :=
                                Functor.obj (Opens.toTopCat X.toTopCat)
                                  (↑(Classical.choose (p := fun (U : OpenNhds x) ↦
                                        ∃ (R : CommRingCat.{u}),
                                          Nonempty.{u + 1} (X.restrict sorry ≅ Spec.toLocallyRingedSpace.obj (op R)))
                                        sorry) :
                                    TopologicalSpace.Opens (↑X.toTopCat : Type u)))
                                sorry ≅
                              Spec.toLocallyRingedSpace.obj (op R)))
                          sorry)))
                    r)))) :
          C(↥((X.affineCover.bind fun (i : X.affineCover.I₀) ↦
                    Precoverage.ZeroHypercover.toPreZeroHypercover
                      (affineBasisCoverOfAffine
                        (Classical.choose (p := fun (R : CommRingCat.{u}) ↦
                          Nonempty.{u + 1} (X.restrict sorry ≅ Spec.toLocallyRingedSpace.obj (op R))) sorry))).X
                (Sigma.mk (β := fun (i : X.affineCover.I₀) ↦
                  PreZeroHypercover.I₀ (S := X.affineCover.X i)
                    (Precoverage.ZeroHypercover.toPreZeroHypercover
                      (affineBasisCoverOfAffine
                        (Classical.choose (p := fun (R : CommRingCat.{u}) ↦
                          Nonempty.{u + 1} (X.restrict sorry ≅ Spec.toLocallyRingedSpace.obj (op R))) sorry))))
                  x r)),
            ↥(X.affineCover.X x))) :
      (a :
          ↥((X.affineCover.bind fun (i : X.affineCover.I₀) ↦
                  (affineBasisCoverOfAffine (Classical.choose sorry)).toPreZeroHypercover).X
              ⟨x, r⟩)) →
        ↥(X.affineCover.X x)))
  (Opens.carrier (PrimeSpectrum.basicOpen r))
Tactic: congr