-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D : GlueData
i j : D.J
x : ↥(D.U i)
y : ↥(D.U j)
⊢ Eq (α := ↥D.glued)
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (((((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData
                              LocallyRingedSpace.forgetToSheafedSpace).mapGlueData
                          SheafedSpace.forgetToPresheafedSpace).mapGlueData
                      (PresheafedSpace.forget CommRingCat)).ι
                  i ≫
                D.isoCarrier.inv) :
            (a : ↥(D.U i)) → ↥D.glued)
          x :
        ↥D.glued)
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (((((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData
                              LocallyRingedSpace.forgetToSheafedSpace).mapGlueData
                          SheafedSpace.forgetToPresheafedSpace).mapGlueData
                      (PresheafedSpace.forget CommRingCat)).ι
                  j ≫
                D.isoCarrier.inv) :
            (a : ↥(D.U j)) → ↥D.glued)
          y :
        ↥D.glued) ↔
    Eq (α := ↥D.glued)
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (((((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData
                              LocallyRingedSpace.forgetToSheafedSpace).mapGlueData
                          SheafedSpace.forgetToPresheafedSpace).mapGlueData
                      (PresheafedSpace.forget CommRingCat)).ι
                  i ≫
                D.isoCarrier.inv) :
            (a :
                (↑(((((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData
                                  LocallyRingedSpace.forgetToSheafedSpace).mapGlueData
                              SheafedSpace.forgetToPresheafedSpace).mapGlueData
                          (PresheafedSpace.forget CommRingCat)).U
                      i) :
                  Type u)) →
              ↥D.glued)
          x :
        ↥D.glued)
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              D.isoCarrier.inv :
            (a :
                (↑((((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData
                                LocallyRingedSpace.forgetToSheafedSpace).mapGlueData
                            SheafedSpace.forgetToPresheafedSpace).mapGlueData
                        (PresheafedSpace.forget CommRingCat)).glued :
                  Type u)) →
              ↥D.glued)
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                  (Y :=
                  ((((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData
                              LocallyRingedSpace.forgetToSheafedSpace).mapGlueData
                          SheafedSpace.forgetToPresheafedSpace).mapGlueData
                      (PresheafedSpace.forget CommRingCat)).glued)
                  (((((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData
                                LocallyRingedSpace.forgetToSheafedSpace).mapGlueData
                            SheafedSpace.forgetToPresheafedSpace).mapGlueData
                        (PresheafedSpace.forget CommRingCat)).ι
                    j) :
                (a :
                    (↑(((((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData
                                      LocallyRingedSpace.forgetToSheafedSpace).mapGlueData
                                  SheafedSpace.forgetToPresheafedSpace).mapGlueData
                              (PresheafedSpace.forget CommRingCat)).U
                          j) :
                      Type u)) →
                  (↑((((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData
                                  LocallyRingedSpace.forgetToSheafedSpace).mapGlueData
                              SheafedSpace.forgetToPresheafedSpace).mapGlueData
                          (PresheafedSpace.forget CommRingCat)).glued :
                    Type u))
              y :
            (↑((((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData
                            LocallyRingedSpace.forgetToSheafedSpace).mapGlueData
                        SheafedSpace.forgetToPresheafedSpace).mapGlueData
                    (PresheafedSpace.forget CommRingCat)).glued :
              Type u)) :
        ↥D.glued)

Tactic:
rfl