-- 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.f i i).c.app (op U) ≫
            (D.V (i, i)).presheaf.map (𝟙 ((Opens.map (D.f i i).base).op.obj (op U)) ≫ eqToHom ⋯) ≫
              invApp (D.f i i) ((Opens.map (D.t i i).base).1 (unop ((Opens.map (D.f i i).base).op.obj (op 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.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 erw : 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 ≫
    D.ιInvAppπEqMap U ≫
      (D.f i i).c.app (op U) ≫
        invApp (D.f i i) (unop ((Opens.map (D.f i i).base).op.obj (op U))) ≫
          (D.U i).presheaf.map
              ((opensFunctor (D.f i i)).op.map (𝟙 ((Opens.map (D.f i i).base).op.obj (op U)) ≫ eqToHom sorry)) ≫
            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 (Quiver.Hom.op (eqToHom sorry)) :
                (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)) 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) (op (WalkingMultispan.left (i, j))))
Tactic: erw [IsOpenImmersion.inv_naturality_assoc]