-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
D : GlueData
i j : D.J
x : ↥(D.U i)
y : ↥(D.U j)
⊢ 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)
have 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)
Tactic: simp_rw [← D.ι_isoCarrier_inv]