-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D : GlueData
i : D.toLocallyRingedSpaceGlueData.J
y : (↑(D.toLocallyRingedSpaceGlueData.U i).toTopCat : Type u)
j : PreZeroHypercover.I₀ (S := D.U i) (Precoverage.ZeroHypercover.toPreZeroHypercover (D.U i).affineCover)
z : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (D.U i).affineCover) j)
hz : (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (D.U i).affineCover) j) z = y
⊢ Membership.mem (α := (↑(D.mapGlueData forgetToLocallyRingedSpace).glued.toTopCat : Type u)) (γ :=
    Set (↑(↑(D.mapGlueData forgetToLocallyRingedSpace).glued.toPresheafedSpace : TopCat) : Type u))
    (Set.image (α := ↥(D.U i))
      (⇑(TopCat.Hom.hom (Hom.base (LocallyRingedSpace.Hom.toHom ((D.mapGlueData forgetToLocallyRingedSpace).ι i)))) :
        (a : ↥(D.U i)) → (↑(↑(D.mapGlueData forgetToLocallyRingedSpace).glued.toPresheafedSpace : TopCat) : Type u))
      (Set.range (ι :=
        (↑(↑(Spec.toLocallyRingedSpace.obj
                    (op
                      (Classical.indefiniteDescription
                          (fun (R : CommRingCat.{u}) ↦
                            Nonempty.{u + 1}
                              ((D.U i).restrict (U :=
                                  Functor.obj (Opens.toTopCat (D.U i).toTopCat)
                                    (↑(Classical.choose (p := fun (U : OpenNhds j) ↦
                                          ∃ (R : CommRingCat.{u}),
                                            Nonempty.{u + 1}
                                              ((D.U i).restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)))
                                          ⋯) :
                                      TopologicalSpace.Opens (↑(D.U i).toTopCat : Type u)))
                                  (f :=
                                  (↑(Classical.choose (p := fun (U : OpenNhds j) ↦
                                          ∃ (R : CommRingCat.{u}),
                                            Nonempty.{u + 1}
                                              ((D.U i).restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)))
                                          ⋯) :
                                      TopologicalSpace.Opens (↑(D.U i).toTopCat : Type u)).inclusion')
                                  ⋯ ≅
                                Spec.toLocallyRingedSpace.obj (op R)))
                          ⋯).1)).toPresheafedSpace :
              TopCat) :
          Type u))
        (⇑(TopCat.Hom.hom
              (Hom.toLRSHom
                  (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (D.U i).affineCover) j)).base) :
          (a :
              (↑(↑(Spec.toLocallyRingedSpace.obj
                          (op
                            (Classical.indefiniteDescription
                                (fun (R : CommRingCat) ↦
                                  Nonempty ((D.U i).restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)))
                                ⋯).1)).toPresheafedSpace :
                    TopCat) :
                Type u)) →
            ↥(D.U i))))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (Y :=
            (↑(D.mapGlueData forgetToLocallyRingedSpace).glued.toPresheafedSpace : TopCat))
            (Hom.base (LocallyRingedSpace.Hom.toHom ((D.mapGlueData forgetToLocallyRingedSpace).ι i))) :
          (a : (↑(↑((D.mapGlueData forgetToLocallyRingedSpace).U i).toPresheafedSpace : TopCat) : Type u)) →
            (↑(↑(D.mapGlueData forgetToLocallyRingedSpace).glued.toPresheafedSpace : TopCat) : Type u))
        y :
      (↑(↑(D.mapGlueData forgetToLocallyRingedSpace).glued.toPresheafedSpace : TopCat) : Type u))

Tactic:
Set.mem_image_of_mem _ ⟨z, hz⟩

Premises used: Set.Mem, Set.mem_image_of_mem, Exists.intro