-- 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 k : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
h :
  Eq (α :=
    (D.U i).presheaf.obj (op U) ⟶
      (Functor.obj (TopCat.Presheaf.pushforward C (D.f j k).base) (D.V (j, k)).presheaf).obj
        (op
          (Functor.obj (C := Opens (↑(↑D.glued : TopCat) : Type v))
            (Opens.map (Hom.base (D.ι j)) :
              Opens (↑(↑D.glued : TopCat) : Type v) ⥤ Opens (↑(↑(D.U 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)))))
    ((D.f i j).c.app (op U) ≫
        (D.t j i).c.app ((Opens.map (D.f i j).base).op.obj (op U)) ≫
          NatTrans.app (Hom.c (pullback.fst (D.f j i) (D.f j k)))
              (op ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U))))) ≫
            invApp (pullback.snd (D.f j i) (D.f j k))
                ((Opens.map (Hom.base (pullback.fst (D.f j i) (D.f j k))) :
                      Opens (↑(↑(D.V (j, i)) : TopCat) : Type v) ⥤
                        Opens (↑(↑(pullback (D.f j i) (D.f j k)) : TopCat) : Type v)).1
                  ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U))))) ≫
              (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
                (Functor.obj (TopCat.Presheaf.pushforward C (D.f j k).base) (D.V (j, k)).presheaf).map
                  (Quiver.Hom.op (eqToHom ⋯)) :
      (D.U i).presheaf.obj (op U) ⟶
        (Functor.obj (TopCat.Presheaf.pushforward C (D.f j k).base) (D.V (j, k)).presheaf).obj
          (op
            (Functor.obj (C := Opens (↑(↑D.glued : TopCat) : Type v))
              (Opens.map (Hom.base (D.ι j)) :
                Opens (↑(↑D.glued : TopCat) : Type v) ⥤ Opens (↑(↑(D.U 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)))))
    (CategoryStruct.comp (Y :=
        (Functor.obj (TopCat.Presheaf.pushforward C (Hom.base (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j)))
              (pullback (D.f j i) (D.f j k)).presheaf).obj
          (op U))
        (NatTrans.app (Hom.c (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j)) (op U))
        (invApp (pullback.snd (D.f j i) (D.f j k))
            ((Opens.map (Hom.base (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j)) :
                  Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤
                    Opens (↑(↑(pullback (D.f j i) (D.f j k)) : TopCat) : Type v)).1
              U) ≫
          (D.V (j, k)).presheaf.map (eqToHom ⋯)) :
      (D.U i).presheaf.obj (op U) ⟶
        (D.V (j, k)).presheaf.obj
          ((Opens.map (D.f j k).base).op.obj
            (op
              (Functor.obj (C := Opens (↑(↑D.glued : TopCat) : Type v))
                (Opens.map (Hom.base (D.ι j)) :
                  Opens (↑(↑D.glued : TopCat) : Type v) ⥤ Opens (↑(↑(D.U 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))))))
⊢ Eq (α :=
    (D.U i).presheaf.obj (op U) ⟶
      (Functor.obj (TopCat.Presheaf.pushforward C (D.f j k).base) (D.V (j, k)).presheaf).obj
        (op
          (Functor.obj (C := Opens (↑(↑D.glued : TopCat) : Type v))
            (Opens.map (Hom.base (D.ι j)) :
              Opens (↑(↑D.glued : TopCat) : Type v) ⥤ Opens (↑(↑(D.U 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)))))
    ((D.f i j).c.app (op U) ≫
        (D.t j i).c.app ((Opens.map (D.f i j).base).op.obj (op U)) ≫
          invApp (D.f j i) ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U)))) ≫
            CategoryStruct.comp (Y :=
              (D.U j).presheaf.obj
                (op
                  (Functor.obj (C := Opens (↑(↑D.glued : TopCat) : Type v))
                    (Opens.map (Hom.base (D.ι j)) :
                      Opens (↑(↑D.glued : TopCat) : Type v) ⥤ Opens (↑(↑(D.U 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)))))
              ((D.U j).presheaf.map (Quiver.Hom.op (eqToHom ⋯)) :
                (D.U j).presheaf.obj
                    (op
                      ((opensFunctor (D.f j i)).obj
                        ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U)))))) ⟶
                  (D.U j).presheaf.obj
                    (op
                      (Functor.obj (C := Opens (↑(↑D.glued : TopCat) : Type v))
                        (Opens.map (Hom.base (D.ι j)) :
                          Opens (↑(↑D.glued : TopCat) : Type v) ⥤ Opens (↑(↑(D.U 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)))))
              ((D.f j k).c.app
                  (op
                    (Functor.obj (C := Opens (↑(↑D.glued : TopCat) : Type v))
                      (Opens.map (Hom.base (D.ι j)) :
                        Opens (↑(↑D.glued : TopCat) : Type v) ⥤ Opens (↑(↑(D.U 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)))) :
                (D.U j).presheaf.obj
                    (op
                      (Functor.obj (C := Opens (↑(↑D.glued : TopCat) : Type v))
                        (Opens.map (Hom.base (D.ι j)) :
                          Opens (↑(↑D.glued : TopCat) : Type v) ⥤ Opens (↑(↑(D.U 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)))) ⟶
                  (Functor.obj (TopCat.Presheaf.pushforward C (D.f j k).base) (D.V (j, k)).presheaf).obj
                    (op
                      (Functor.obj (C := Opens (↑(↑D.glued : TopCat) : Type v))
                        (Opens.map (Hom.base (D.ι j)) :
                          Opens (↑(↑D.glued : TopCat) : Type v) ⥤ Opens (↑(↑(D.U 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))))) :
      (D.U i).presheaf.obj (op U) ⟶
        (Functor.obj (TopCat.Presheaf.pushforward C (D.f j k).base) (D.V (j, k)).presheaf).obj
          (op
            (Functor.obj (C := Opens (↑(↑D.glued : TopCat) : Type v))
              (Opens.map (Hom.base (D.ι j)) :
                Opens (↑(↑D.glued : TopCat) : Type v) ⥤ Opens (↑(↑(D.U 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)))))
    (CategoryStruct.comp (Y :=
        (Functor.obj (TopCat.Presheaf.pushforward C (Hom.base (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j)))
              (pullback (D.f j i) (D.f j k)).presheaf).obj
          (op U))
        (NatTrans.app (Hom.c (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j)) (op U))
        (invApp (pullback.snd (D.f j i) (D.f j k))
            ((Opens.map (Hom.base (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j)) :
                  Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤
                    Opens (↑(↑(pullback (D.f j i) (D.f j k)) : TopCat) : Type v)).1
              U) ≫
          (D.V (j, k)).presheaf.map (eqToHom ⋯)) :
      (D.U i).presheaf.obj (op U) ⟶
        (D.V (j, k)).presheaf.obj
          ((Opens.map (D.f j k).base).op.obj
            (op
              (Functor.obj (C := Opens (↑(↑D.glued : TopCat) : Type v))
                (Opens.map (Hom.base (D.ι j)) :
                  Opens (↑(↑D.glued : TopCat) : Type v) ⥤ Opens (↑(↑(D.U 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))))))

Tactic:
rw [(D.f j k).c.naturality, f_invApp_f_app_assoc]

Premises used: CategoryTheory.GlueData.f, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app_assoc, CategoryTheory.NatTrans.naturality, AlgebraicGeometry.PresheafedSpace.Hom.c, AlgebraicGeometry.PresheafedSpace.GlueData.toGlueData