-- 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 : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
j k : D.J
w :
  Eq (α := limit (D.diagramOverOpen U) ⟶ (D.diagramOverOpen U).obj (op (WalkingMultispan.left (j, k))))
    (CategoryStruct.comp (Y :=
      (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.right ((MultispanShape.prod D.J).fst (j, k)))))
      (CategoryStruct.comp (Y := limit (D.diagramOverOpen U)) (D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U)
        (limit.π
          (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)))
          (op (WalkingMultispan.right ((MultispanShape.prod D.J).fst (j, k))))))
      ((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))).map
        (Quiver.Hom.op (WalkingMultispan.Hom.fst (j, k)))))
    (CategoryStruct.comp (Y :=
      (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.right ((MultispanShape.prod D.J).fst (j, k)))))
      (limit.π
        (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)))
        (op (WalkingMultispan.right ((MultispanShape.prod D.J).fst (j, k)))))
      ((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))).map
        (Quiver.Hom.op (WalkingMultispan.Hom.fst (j, k)))))
⊢ Eq (α := limit (D.diagramOverOpen U) ⟶ (D.diagramOverOpen U).obj (op (WalkingMultispan.left (j, k))))
    ((D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫
      limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (j, k))))
    (𝟙 (limit (D.diagramOverOpen U)) ≫ limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (j, k))))

Tactic:
rw [← limit.w (componentwiseDiagram 𝖣.diagram.multispan _)
        (Quiver.Hom.op (WalkingMultispan.Hom.fst (j, k))),
      ← Category.assoc, Category.id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.id_comp