-- 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)
⊢ 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 ⋯ ≅ 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)))
    (Opens.carrier (PrimeSpectrum.basicOpen r))

Tactic:
(PrimeSpectrum.localization_away_comap_range (Localization.Away r) r :)

Premises used: Set.Mem, OreLocalization, Localization.Away, Quotient, PrimeSpectrum.comap, PrimeSpectrum.localization_away_comap_range