-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D : GlueData
i j : D.J
x : ↥(D.U i)
y : ↥(D.U j)
simp_rw :
  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)
⊢ Eq (α := ↥D.glued) ((D.ι i) x : ↥D.glued) ((D.ι j) 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.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i ≫
                D.isoCarrier.inv) :
            (a :
                (↑(D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.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.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.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.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued)
                  (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι j) :
                (a :
                    (↑(D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.U
                          j) :
                      Type u)) →
                  (↑D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued :
                    Type u))
              y :
            (↑D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued :
              Type u)) :
        ↥D.glued)

Tactic:
simp_rw [← D.ι_isoCarrier_inv]

Premises used: AlgebraicGeometry.Scheme.GlueData.ι_isoCarrier_inv