-- 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))
have left : 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 sorry ≅ Spec.toLocallyRingedSpace.obj (op R)))
                                        sorry) :
                                    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 sorry ≅ Spec.toLocallyRingedSpace.obj (op R)))
                                        sorry) :
                                    TopologicalSpace.Opens (↑(D.U i).toTopCat : Type u)).inclusion')
                                sorry ≅
                              Spec.toLocallyRingedSpace.obj (op R)))
                        sorry).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 sorry ≅ Spec.toLocallyRingedSpace.obj (op R)))
                              sorry).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: simp only [LocallyRingedSpace.comp_toHom, PresheafedSpace.comp_base,
      TopCat.hom_comp, ContinuousMap.coe_comp, Set.range_comp]