-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
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)
change :
  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 ≫
          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.f i i).c.app (op U) ≫
                (D.t i i).c.app ((Opens.map (D.f i i).base).op.obj (op U)) ≫
                  invApp (D.f i i)
                      (unop (op ((Opens.map (D.t i i).base).1 (unop ((Opens.map (D.f i i).base).op.obj (op U)))))) ≫
                    (D.U i).presheaf.map (Quiver.Hom.op (eqToHom ⋯)) :
              (D.U i).presheaf.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))))
⊢ 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 ≫
        NatTrans.app
          (Cone.π
            { pt := (D.U i).presheaf.obj (op U),
              π :=
                { app := fun (j : (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ) ↦ D.ιInvAppπApp U (unop j),
                  naturality := ⋯ } })
          (op (WalkingMultispan.left (i, j))))
    (limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j))))

Tactic:
change _ ≫ _ ≫ (_ ≫ _) ≫ _ = _

Premises used: CategoryTheory.CategoryStruct.comp