-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i j : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
⊢ Eq (α :=
    limit (D.diagramOverOpen U) ⟶
      (componentwiseDiagram D.diagram.multispan
            (Functor.obj
                (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                  Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                U :
              Opens (↑(↑D.glued : TopCat) : Type v))).obj
        (op (WalkingMultispan.left (i, j))))
    (D.diagramOverOpenπ U i ≫
        D.ιInvAppπEqMap U ≫
          (D.U i).presheaf.map
              (Quiver.Hom.op (X :=
                Set.image (α := (↑(↑(D.V (i, i)) : TopCat) : Type v))
                  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                        TopCat.carrier) (D.f i i).base) :
                    (a : (↑(↑(D.V (i, i)) : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v))
                  ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                          TopCat.carrier) (D.f i i).base) :
                      (a : (↑(↑(D.V (i, i)) : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v)) ⁻¹'
                    U.carrier))
                (Y := U.carrier)
                (homOfLE (x :=
                  Set.image (α := (↑(↑(D.V (i, i)) : TopCat) : Type v))
                    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                          TopCat.carrier) (D.f i i).base) :
                      (a : (↑(↑(D.V (i, i)) : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v))
                    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                            TopCat.carrier) (D.f i i).base) :
                        (a : (↑(↑(D.V (i, i)) : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v)) ⁻¹'
                      U.carrier))
                  (y := U.carrier) ⋯)) ≫
            (D.U i).presheaf.map
                ((opensFunctor (D.f i i)).op.map (𝟙 ((Opens.map (D.f i i).base).op.obj (op U)) ≫ eqToHom ⋯)) ≫
              CategoryStruct.comp (Y :=
                (D.U i).presheaf.obj
                  (op
                    (Functor.obj (C := Opens (↑(↑D.glued : TopCat) : Type v))
                      (Opens.map (Hom.base (D.ι i)) :
                        Opens (↑(↑D.glued : TopCat) : Type v) ⥤ Opens (↑(↑(D.U i) : TopCat) : Type v))
                      (Functor.obj
                          (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                            Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                          U :
                        Opens (↑(↑D.glued : TopCat) : Type v)))))
                ((D.U i).presheaf.map (Quiver.Hom.op (eqToHom ⋯)) :
                  (D.U i).presheaf.obj
                      (op
                        ((opensFunctor (D.f i i)).obj
                          ((Opens.map (D.t i i).base).1 (unop ((Opens.map (D.f i i).base).op.obj (op U)))))) ⟶
                    (D.U i).presheaf.obj
                      (op
                        (Functor.obj (C := Opens (↑(↑D.glued : TopCat) : Type v))
                          (Opens.map (Hom.base (D.ι i)) :
                            Opens (↑(↑D.glued : TopCat) : Type v) ⥤ Opens (↑(↑(D.U i) : TopCat) : Type v))
                          (Functor.obj
                              (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                                Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                              U :
                            Opens (↑(↑D.glued : TopCat) : Type v)))))
                ((D.f i j).c.app
                      (op
                        (Functor.obj (C := Opens (↑(↑D.glued : TopCat) : Type v))
                          (Opens.map (Hom.base (D.ι i)) :
                            Opens (↑(↑D.glued : TopCat) : Type v) ⥤ Opens (↑(↑(D.U i) : TopCat) : Type v))
                          (Functor.obj
                              (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                                Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                              U :
                            Opens (↑(↑D.glued : TopCat) : Type v)))) ≫
                    (D.V (i, j)).presheaf.map (eqToHom ⋯) :
                  (D.U i).presheaf.obj
                      (op
                        (Functor.obj (C := Opens (↑(↑D.glued : TopCat) : Type v))
                          (Opens.map (Hom.base (D.ι i)) :
                            Opens (↑(↑D.glued : TopCat) : Type v) ⥤ Opens (↑(↑(D.U i) : TopCat) : Type v))
                          (Functor.obj
                              (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                                Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                              U :
                            Opens (↑(↑D.glued : TopCat) : Type v)))) ⟶
                    (D.diagramOverOpen U).obj (op (WalkingMultispan.left (i, j)))) :
      limit (D.diagramOverOpen U) ⟶
        (componentwiseDiagram D.diagram.multispan
              (Functor.obj
                  (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                    Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                  U :
                Opens (↑(↑D.glued : TopCat) : Type v))).obj
          (op (WalkingMultispan.left (i, j))))
    (limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j))) :
      limit (D.diagramOverOpen U) ⟶ (D.diagramOverOpen U).obj (op (WalkingMultispan.left (i, j))))
have iterate : Eq (α :=
  limit (D.diagramOverOpen U) ⟶
    (componentwiseDiagram D.diagram.multispan
          (Functor.obj
              (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) sorry :
                Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
              U :
            Opens (↑(↑D.glued : TopCat) : Type v))).obj
      (op (WalkingMultispan.left (i, j))))
  (D.diagramOverOpenπ U i ≫
      CategoryStruct.comp (Y :=
        (D.U i).presheaf.obj
          (op
            (Functor.obj (C := Opens (↑(↑D.glued : TopCat) : Type v))
              (Opens.map (Hom.base (D.ι i)) :
                Opens (↑(↑D.glued : TopCat) : Type v) ⥤ Opens (↑(↑(D.U i) : TopCat) : Type v))
              (Functor.obj
                  (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) sorry :
                    Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                  U :
                Opens (↑(↑D.glued : TopCat) : Type v)))))
        ((D.U i).presheaf.map
            (((Iso.inv (eqToIso sorry) ≫
                  Quiver.Hom.op (X :=
                    Set.image (α := (↑(↑(D.V (i, i)) : TopCat) : Type v))
                      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                            TopCat.carrier) (D.f i i).base) :
                        (a : (↑(↑(D.V (i, i)) : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v))
                      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                              TopCat.carrier) (D.f i i).base) :
                          (a : (↑(↑(D.V (i, i)) : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v)) ⁻¹'
                        U.carrier))
                    (Y := U.carrier)
                    (homOfLE (x :=
                      Set.image (α := (↑(↑(D.V (i, i)) : TopCat) : Type v))
                        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                              TopCat.carrier) (D.f i i).base) :
                          (a : (↑(↑(D.V (i, i)) : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v))
                        ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                                TopCat.carrier) (D.f i i).base) :
                            (a : (↑(↑(D.V (i, i)) : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v)) ⁻¹'
                          U.carrier))
                      (y := U.carrier) sorry)) ≫
                (opensFunctor (D.f i i)).op.map (𝟙 ((Opens.map (D.f i i).base).op.obj (op U)) ≫ eqToHom sorry)) ≫
              Quiver.Hom.op (eqToHom sorry)) :
          (D.U i).presheaf.obj
              (op
                (Functor.obj (C := Opens (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v))
                  (Opens.map (Hom.base (colimit.ι D.diagram.multispan (unop (op (WalkingMultispan.right i))))) :
                    Opens (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v) ⥤
                      Opens (↑(↑(D.diagram.multispan.obj (unop (op (WalkingMultispan.right i)))) : TopCat) : Type v))
                  (Functor.obj
                      (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) sorry :
                        Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                      U :
                    Opens (↑(↑D.glued : TopCat) : Type v)))) ⟶
            (D.U i).presheaf.obj
              (op
                (Functor.obj (C := Opens (↑(↑D.glued : TopCat) : Type v))
                  (Opens.map (Hom.base (D.ι i)) :
                    Opens (↑(↑D.glued : TopCat) : Type v) ⥤ Opens (↑(↑(D.U i) : TopCat) : Type v))
                  (Functor.obj
                      (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) sorry :
                        Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                      U :
                    Opens (↑(↑D.glued : TopCat) : Type v)))))
        ((D.f i j).c.app
              (op
                (Functor.obj (C := Opens (↑(↑D.glued : TopCat) : Type v))
                  (Opens.map (Hom.base (D.ι i)) :
                    Opens (↑(↑D.glued : TopCat) : Type v) ⥤ Opens (↑(↑(D.U i) : TopCat) : Type v))
                  (Functor.obj
                      (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) sorry :
                        Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                      U :
                    Opens (↑(↑D.glued : TopCat) : Type v)))) ≫
            (D.V (i, j)).presheaf.map (eqToHom sorry) :
          (D.U i).presheaf.obj
              (op
                (Functor.obj (C := Opens (↑(↑D.glued : TopCat) : Type v))
                  (Opens.map (Hom.base (D.ι i)) :
                    Opens (↑(↑D.glued : TopCat) : Type v) ⥤ Opens (↑(↑(D.U i) : TopCat) : Type v))
                  (Functor.obj
                      (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) sorry :
                        Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                      U :
                    Opens (↑(↑D.glued : TopCat) : Type v)))) ⟶
            (D.diagramOverOpen U).obj (op (WalkingMultispan.left (i, j)))) :
    limit (D.diagramOverOpen U) ⟶
      (componentwiseDiagram D.diagram.multispan
            (Functor.obj
                (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) sorry :
                  Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                U :
              Opens (↑(↑D.glued : TopCat) : Type v))).obj
        (op (WalkingMultispan.left (i, j))))
  (limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j))) :
    limit (D.diagramOverOpen U) ⟶ (D.diagramOverOpen U).obj (op (WalkingMultispan.left (i, j))))
Tactic: iterate 3 rw [← Functor.map_comp_assoc]