-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
i j k : D.J
U : Opens (↑(↑(D.V (i, j)) : TopCat) : Type v)
this :
  ∀ (U : (Opens (↑(↑(D.U i) : TopCat) : Type v))ᵒᵖ),
    (D.f i j).c.app U ≫
        NatTrans.app (Hom.c (pullback.fst (D.f i j) (D.f i k))) (op ((Opens.map (D.f i j).base).obj (unop U))) =
      ((D.f i k).c.app U ≫
          NatTrans.app (Hom.c (pullback.snd (D.f i j) (D.f i k))) (op ((Opens.map (D.f i k).base).obj (unop U)))) ≫
        (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom ⋯)
h :
  (D.V (i, k)).presheaf.map
      (CategoryStruct.comp (Y :=
        op
          (Functor.obj (C := Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
            (opensFunctor (pullback.snd (D.f i j) (D.f i k)))
            (Functor.obj (Opens.map (Hom.base (pullback.snd (D.f i j) (D.f i k))))
              ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))))))
        (Quiver.Hom.op (X :=
            Set.image (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                    TopCat.carrier) (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat))
                    (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
                (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
              ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                      TopCat.carrier) (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat))
                      (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
                  (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
                    (↑(↑(D.V (i, k)) : TopCat) : Type v)) ⁻¹'
                ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))).carrier))
            (Y := ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))).carrier)
            (homOfLE (x :=
              Set.image (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
                (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                      TopCat.carrier) (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat))
                      (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
                  (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
                ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                        TopCat.carrier) (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat))
                        (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
                    (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
                      (↑(↑(D.V (i, k)) : TopCat) : Type v)) ⁻¹'
                  ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))).carrier))
              (y := ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))).carrier) ⋯) :
          op ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))).carrier ⟶
            op
              (Set.image (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
                (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                      TopCat.carrier) (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat))
                      (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
                  (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
                ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                        TopCat.carrier) (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat))
                        (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
                    (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
                      (↑(↑(D.V (i, k)) : TopCat) : Type v)) ⁻¹'
                  ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))).carrier)))
        (CategoryTheory.Functor.map (Functor.op (opensFunctor (pullback.snd (D.f i j) (D.f i k))))
              (eqToHom ⋯ ≫
                CategoryTheory.Functor.map (Functor.op (Opens.map (Hom.base (pullback.fst (D.f i j) (D.f i k)))))
                  (eqToHom ⋯)) ≫
            eqToHom ⋯ :
          op
              (Functor.obj (C := Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
                (opensFunctor (pullback.snd (D.f i j) (D.f i k)))
                (unop
                  (Functor.obj (Functor.op (Opens.map (Hom.base (pullback.snd (D.f i j) (D.f i k) ≫ D.f i k))))
                    (op ((opensFunctor (D.f i j)).obj U))))) ⟶
            (Opens.map (D.f i k).base).op.obj (op ((opensFunctor (D.f i j)).obj U)))) =
    𝟙
      ((Functor.obj (TopCat.Presheaf.pushforward C (D.f i k).base) (D.V (i, k)).presheaf).obj
        (op ((opensFunctor (D.f i j)).obj U)))
⊢ Eq (α :=
    (D.U i).presheaf.obj (op ((opensFunctor (D.f i j)).obj U)) ⟶
      (Functor.obj (TopCat.Presheaf.pushforward C (D.f i k).base) (D.V (i, k)).presheaf).obj
        (op ((opensFunctor (D.f i j)).obj U)))
    ((D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)))
    ((D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) ≫
      (D.V (i, k)).presheaf.map
        (CategoryStruct.comp (Y :=
          op
            (Functor.obj (C := Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
              (opensFunctor (pullback.snd (D.f i j) (D.f i k)))
              (Functor.obj (Opens.map (Hom.base (pullback.snd (D.f i j) (D.f i k))))
                ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))))))
          (Quiver.Hom.op (X :=
              Set.image (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
                (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                      TopCat.carrier) (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat))
                      (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
                  (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
                ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                        TopCat.carrier) (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat))
                        (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
                    (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
                      (↑(↑(D.V (i, k)) : TopCat) : Type v)) ⁻¹'
                  ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))).carrier))
              (Y := ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))).carrier)
              (homOfLE (x :=
                Set.image (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
                  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                        TopCat.carrier) (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat))
                        (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
                    (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
                  ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                          TopCat.carrier) (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat))
                          (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
                      (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
                        (↑(↑(D.V (i, k)) : TopCat) : Type v)) ⁻¹'
                    ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))).carrier))
                (y := ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))).carrier) ⋯) :
            op ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))).carrier ⟶
              op
                (Set.image (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
                  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                        TopCat.carrier) (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat))
                        (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
                    (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
                  ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                          TopCat.carrier) (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat))
                          (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
                      (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
                        (↑(↑(D.V (i, k)) : TopCat) : Type v)) ⁻¹'
                    ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))).carrier)))
          (CategoryTheory.Functor.map (Functor.op (opensFunctor (pullback.snd (D.f i j) (D.f i k))))
                (eqToHom ⋯ ≫
                  CategoryTheory.Functor.map (Functor.op (Opens.map (Hom.base (pullback.fst (D.f i j) (D.f i k)))))
                    (eqToHom ⋯)) ≫
              eqToHom ⋯ :
            op
                (Functor.obj (C := Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
                  (opensFunctor (pullback.snd (D.f i j) (D.f i k)))
                  (unop
                    (Functor.obj (Functor.op (Opens.map (Hom.base (pullback.snd (D.f i j) (D.f i k) ≫ D.f i k))))
                      (op ((opensFunctor (D.f i j)).obj U))))) ⟶
              (Opens.map (D.f i k).base).op.obj (op ((opensFunctor (D.f i j)).obj U)))))

Tactic:
convert! (Category.comp_id _).symm

Premises used: CategoryTheory.Category.comp_id, Eq.symm