-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
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.toLocallyRingedSpaceGlueData.glued.toTopCat : Type u)) (γ :=
      Set (↑(↑D.toLocallyRingedSpaceGlueData.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 (C := TopologicalSpace.Opens (↑(D.U i).toTopCat : Type u))
                                    (Opens.toTopCat (D.U i).toTopCat)
                                    (↑((fun (x : (↑(D.U i).toTopCat : Type u)) ↦
                                            Classical.choose (p := fun (U : OpenNhds x) ↦
                                              ∃ (R : CommRingCat.{u}),
                                                Nonempty.{u + 1}
                                                  ((D.U i).restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)))
                                              ⋯)
                                          j) :
                                      TopologicalSpace.Opens (↑(D.U i).toTopCat : Type u)))
                                  (f :=
                                  (Opens.inclusion'
                                      (↑((fun (x : (↑(D.U i).toTopCat : Type u)) ↦
                                              Classical.choose (p := fun (U : OpenNhds x) ↦
                                                ∃ (R : CommRingCat.{u}),
                                                  Nonempty.{u + 1}
                                                    ((D.U i).restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)))
                                                ⋯)
                                            j) :
                                        TopologicalSpace.Opens (↑(D.U i).toTopCat : Type u)) :
                                    Functor.obj (C := TopologicalSpace.Opens (↑(D.U i).toTopCat : Type u))
                                        (Opens.toTopCat (D.U i).toTopCat)
                                        (↑((fun (x : (↑(D.U i).toTopCat : Type u)) ↦
                                                Classical.choose (p := fun (U : OpenNhds x) ↦
                                                  ∃ (R : CommRingCat.{u}),
                                                    Nonempty.{u + 1}
                                                      ((D.U i).restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)))
                                                  ⋯)
                                              j) :
                                          TopologicalSpace.Opens (↑(D.U i).toTopCat : Type u)) ⟶
                                      (D.U i).toTopCat))
                                  ⋯ ≅
                                Spec.toLocallyRingedSpace.obj (op R)))
                          ⋯).1)).toPresheafedSpace :
              TopCat) :
          Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (Y := (↑D.toLocallyRingedSpaceGlueData.glued.toPresheafedSpace : TopCat))
              (Hom.base
                (LocallyRingedSpace.Hom.toHom
                  (Hom.toLRSHom
                      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (D.U i).affineCover) j) ≫
                    D.toLocallyRingedSpaceGlueData.ι i)))) :
          (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.toLocallyRingedSpaceGlueData.glued.toPresheafedSpace : TopCat) : Type u)))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (Y := (↑D.toLocallyRingedSpaceGlueData.glued.toPresheafedSpace : TopCat))
              (Hom.base (LocallyRingedSpace.Hom.toHom (D.toLocallyRingedSpaceGlueData.ι i))) :
            (a : (↑(↑(D.toLocallyRingedSpaceGlueData.U i).toPresheafedSpace : TopCat) : Type u)) →
              (↑(↑D.toLocallyRingedSpaceGlueData.glued.toPresheafedSpace : TopCat) : Type u))
          y :
        (↑(↑D.toLocallyRingedSpaceGlueData.glued.toPresheafedSpace : TopCat) : Type u)) ∧
    LocallyRingedSpace.IsOpenImmersion (Y := D.toLocallyRingedSpaceGlueData.glued)
      (Hom.toLRSHom (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (D.U i).affineCover) j) ≫
        D.toLocallyRingedSpaceGlueData.ι i)
have left : Membership.mem (α := (↑D.toLocallyRingedSpaceGlueData.glued.toTopCat : Type u)) (γ :=
  Set (↑(↑D.toLocallyRingedSpaceGlueData.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 (C := TopologicalSpace.Opens (↑(D.U i).toTopCat : Type u))
                                (Opens.toTopCat (D.U i).toTopCat)
                                (↑((fun (x : (↑(D.U i).toTopCat : Type u)) ↦
                                        Classical.choose (p := fun (U : OpenNhds x) ↦
                                          ∃ (R : CommRingCat.{u}),
                                            Nonempty.{u + 1}
                                              ((D.U i).restrict sorry ≅ Spec.toLocallyRingedSpace.obj (op R)))
                                          sorry)
                                      j) :
                                  TopologicalSpace.Opens (↑(D.U i).toTopCat : Type u)))
                              (f :=
                              (Opens.inclusion'
                                  (↑((fun (x : (↑(D.U i).toTopCat : Type u)) ↦
                                          Classical.choose (p := fun (U : OpenNhds x) ↦
                                            ∃ (R : CommRingCat.{u}),
                                              Nonempty.{u + 1}
                                                ((D.U i).restrict sorry ≅ Spec.toLocallyRingedSpace.obj (op R)))
                                            sorry)
                                        j) :
                                    TopologicalSpace.Opens (↑(D.U i).toTopCat : Type u)) :
                                Functor.obj (C := TopologicalSpace.Opens (↑(D.U i).toTopCat : Type u))
                                    (Opens.toTopCat (D.U i).toTopCat)
                                    (↑((fun (x : (↑(D.U i).toTopCat : Type u)) ↦
                                            Classical.choose (p := fun (U : OpenNhds x) ↦
                                              ∃ (R : CommRingCat.{u}),
                                                Nonempty.{u + 1}
                                                  ((D.U i).restrict sorry ≅ Spec.toLocallyRingedSpace.obj (op R)))
                                              sorry)
                                          j) :
                                      TopologicalSpace.Opens (↑(D.U i).toTopCat : Type u)) ⟶
                                  (D.U i).toTopCat))
                              sorry ≅
                            Spec.toLocallyRingedSpace.obj (op R)))
                      sorry).1)).toPresheafedSpace :
          TopCat) :
      Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          (Y := (↑D.toLocallyRingedSpaceGlueData.glued.toPresheafedSpace : TopCat))
          (Hom.base
            (LocallyRingedSpace.Hom.toHom
              (Hom.toLRSHom
                  (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (D.U i).affineCover) j) ≫
                D.toLocallyRingedSpaceGlueData.ι i)))) :
      (a :
          (↑(↑(Spec.toLocallyRingedSpace.obj
                      (op
                        (Classical.indefiniteDescription
                            (fun (R : CommRingCat) ↦
                              Nonempty ((D.U i).restrict sorry ≅ Spec.toLocallyRingedSpace.obj (op R)))
                            sorry).1)).toPresheafedSpace :
                TopCat) :
            Type u)) →
        (↑(↑D.toLocallyRingedSpaceGlueData.glued.toPresheafedSpace : TopCat) : Type u)))
  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (Y :=
          (↑D.toLocallyRingedSpaceGlueData.glued.toPresheafedSpace : TopCat))
          (Hom.base (LocallyRingedSpace.Hom.toHom (D.toLocallyRingedSpaceGlueData.ι i))) :
        (a : (↑(↑(D.toLocallyRingedSpaceGlueData.U i).toPresheafedSpace : TopCat) : Type u)) →
          (↑(↑D.toLocallyRingedSpaceGlueData.glued.toPresheafedSpace : TopCat) : Type u))
      y :
    (↑(↑D.toLocallyRingedSpaceGlueData.glued.toPresheafedSpace : TopCat) : Type u))
Tactic: constructor