-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
x : ↥X
r :
  (↑(⋯.choose (p := fun (R : CommRingCat.{u}) ↦
        Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)))) :
    Type u)
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 ⋯ ≅ 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))
⊢ 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)))

Tactic:
simp only [affineBasisCover, Precoverage.ZeroHypercover.bind_toPreZeroHypercover, Set.range_comp,
    PreZeroHypercover.bind_f, Hom.comp_base, TopCat.hom_comp, ContinuousMap.coe_comp]

Premises used: Set.range_comp, AlgebraicGeometry.Scheme.affineBasisCover, ContinuousMap.coe_comp, CategoryTheory.PreZeroHypercover.bind_f, CategoryTheory.Precoverage.ZeroHypercover.bind_toPreZeroHypercover, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.hom_comp