-- 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 ≫
        CategoryStruct.comp (Y := limit (D.diagramOverOpen U)) (D.ιInvApp U)
          (D.diagramOverOpenπ U j ≫
            (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.snd (i, j))) ≫
              𝟙
                ((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 j ≫
      (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.snd (i, j))) ≫
        𝟙
          ((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)))))
have rw : D.diagramOverOpenπ U i ≫
    D.ιInvAppπEqMap U ≫
      D.ιInvApp U ≫
        limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j))) ≫
          𝟙
            ((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))) ≫
    𝟙
      ((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))))
Tactic: rw [limit.w_assoc]