-- 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)
erw :
  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.f i j).c.app
            (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)) ⋯ :
                      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
            (CategoryStruct.comp (Y :=
              (Opens.map (D.f i j).base).op.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)))))
              ((Opens.map (D.f i j).base).op.map
                  (((Iso.inv (eqToIso ⋯) ≫
                        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) ⋯)) ≫
                      (opensFunctor (D.f i i)).op.map (𝟙 ((Opens.map (D.f i i).base).op.obj (op U)) ≫ eqToHom ⋯)) ≫
                    Quiver.Hom.op (eqToHom ⋯)) :
                (Opens.map (D.f i j).base).op.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)) ⋯ :
                              Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                            U :
                          Opens (↑(↑D.glued : TopCat) : Type v)))) ⟶
                  (Opens.map (D.f i j).base).op.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)))))
              (eqToHom ⋯ :
                (Opens.map (D.f i j).base).op.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)))) ⟶
                  op
                    (Functor.obj (C := Opens (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v))
                      (Opens.map (Hom.base (colimit.ι D.diagram.multispan (WalkingMultispan.left (i, j)))) :
                        Opens (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v) ⥤
                          Opens (↑(↑(D.diagram.multispan.obj (WalkingMultispan.left (i, j))) : 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))))) :
      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.f i j).c.app
            (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)) ⋯ :
                      Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                    U :
                  Opens (↑(↑D.glued : TopCat) : Type v)))) ≫
          CategoryStruct.comp (Y :=
            (Functor.obj (TopCat.Presheaf.pushforward C (D.f i j).base) (D.V (i, j)).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)))))
            ((Functor.obj (TopCat.Presheaf.pushforward C (D.f i j).base) (D.V (i, j)).presheaf).map
                (((Iso.inv (eqToIso ⋯) ≫
                      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) ⋯)) ≫
                    (opensFunctor (D.f i i)).op.map (𝟙 ((Opens.map (D.f i i).base).op.obj (op U)) ≫ eqToHom ⋯)) ≫
                  Quiver.Hom.op (eqToHom ⋯)) :
              (Functor.obj (TopCat.Presheaf.pushforward C (D.f i j).base) (D.V (i, j)).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)) ⋯ :
                            Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                          U :
                        Opens (↑(↑D.glued : TopCat) : Type v)))) ⟶
                (Functor.obj (TopCat.Presheaf.pushforward C (D.f i j).base) (D.V (i, j)).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.V (i, j)).presheaf.map (eqToHom ⋯) :
              (D.V (i, j)).presheaf.obj
                  ((Opens.map (D.f i j).base).op.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.V (i, j)).presheaf.obj
                  (op
                    (Functor.obj (C := Opens (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v))
                      (Opens.map (Hom.base (colimit.ι D.diagram.multispan (WalkingMultispan.left (i, j)))) :
                        Opens (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v) ⥤
                          Opens (↑(↑(D.diagram.multispan.obj (WalkingMultispan.left (i, j))) : 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))))) :
      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))))

Tactic:
erw [← (D.V (i, j)).presheaf.map_comp]

Premises used: Prod.mk, CategoryTheory.GlueData.V, AlgebraicGeometry.PresheafedSpace.presheaf, CategoryTheory.Functor.map_comp, AlgebraicGeometry.PresheafedSpace.GlueData.toGlueData