-- 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.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))
            x r)))
      ⇑(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))
            x r)))
    (Set.image (α := ↥(X.affineCover.X x)) (⇑(X.affineCover.f x)) (Opens.carrier (PrimeSpectrum.basicOpen r)))
have simp : 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 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))))
  ((fun (a : ↥(X.affineCover.X x)) ↦ (X.affineCover.f x) a) '' Opens.carrier (PrimeSpectrum.basicOpen r))
Tactic: simp only [affineBasisCover, Precoverage.ZeroHypercover.bind_toPreZeroHypercover, Set.range_comp,
    PreZeroHypercover.bind_f, Hom.comp_base, TopCat.hom_comp, ContinuousMap.coe_comp]