-- 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 (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Eq (α :=
    (D.V (i, k)).presheaf.obj (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)) ⟶
      (D.V (k, i)).presheaf.obj
        (op
          (Functor.obj (C := Opens (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
            (opensFunctor (pullback.fst (D.f k i) (D.f k j))) ((Opens.map (D.t' k i j).base).1 U))))
    ((D.t k i).c.app (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)) ≫
      (D.V (k, i)).presheaf.map (eqToHom ⋯))
    ((D.t k i).c.app (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)) ≫
      CategoryStruct.comp (Y :=
        (D.V (k, i)).presheaf.obj
          (op
            (Functor.obj (C := Opens (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
              (opensFunctor (pullback.fst (D.f k i) (D.f k j)))
              (Functor.obj (Opens.map (Hom.base (pullback.fst (D.f k i) (D.f k j))))
                ((Opens.map (D.t k i).base).obj (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U))))))
        ((D.V (k, i)).presheaf.map
            (Quiver.Hom.op (X :=
              Set.image (α := (↑(↑(pullback (D.f k i) (D.f k j)) : 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 k i) (D.f k j)) : TopCat))
                      (Hom.base (pullback.fst (D.f k i) (D.f k j)))) :
                  (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : 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 k i) (D.f k j)) : TopCat))
                        (Hom.base (pullback.fst (D.f k i) (D.f k j)))) :
                    (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) →
                      (↑(↑(D.V (k, i)) : TopCat) : Type v)) ⁻¹'
                  ((Opens.map (D.t k i).base).obj
                      (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)).carrier))
              (Y :=
              ((Opens.map (D.t k i).base).obj
                  (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)).carrier)
              (eqToHom (X :=
                Set.image (α := (↑(↑(pullback (D.f k i) (D.f k j)) : 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 k i) (D.f k j)) : TopCat))
                        (Hom.base (pullback.fst (D.f k i) (D.f k j)))) :
                    (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : 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 k i) (D.f k j)) : TopCat))
                          (Hom.base (pullback.fst (D.f k i) (D.f k j)))) :
                      (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) →
                        (↑(↑(D.V (k, i)) : TopCat) : Type v)) ⁻¹'
                    ((Opens.map (D.t k i).base).obj
                        (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)).carrier))
                (Y :=
                ((Opens.map (D.t k i).base).obj
                    (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)).carrier)
                ⋯)) :
          (D.V (k, i)).presheaf.obj
              (op ((Opens.map (D.t k i).base).obj (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U))) ⟶
            (D.V (k, i)).presheaf.obj
              (op
                (Functor.obj (C := Opens (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
                  (opensFunctor (pullback.fst (D.f k i) (D.f k j)))
                  (Functor.obj (Opens.map (Hom.base (pullback.fst (D.f k i) (D.f k j))))
                    ((Opens.map (D.t k i).base).obj
                      (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U))))))
        (CategoryStruct.comp (Y :=
            (D.V (k, i)).presheaf.obj
              (op
                (Functor.obj (opensFunctor (pullback.fst (D.f k i) (D.f k j)))
                  (unop
                    (op
                      ((Opens.map (D.t' k i j).base).obj
                        (Functor.obj (Opens.map (Hom.base (pullback.snd (D.f i j) (D.f i k))))
                          (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U))))))))
            ((D.V (k, i)).presheaf.map
              (CategoryTheory.Functor.map (Functor.op (opensFunctor (pullback.fst (D.f k i) (D.f k j)))) (eqToHom ⋯)))
            ((D.V (k, i)).presheaf.map
              (CategoryTheory.Functor.map (Functor.op (opensFunctor (pullback.fst (D.f k i) (D.f k j))))
                (Quiver.Hom.op ((Opens.map (D.t' k i j).base).map (Quiver.Hom.unop (eqToHom ⋯)))))) :
          (D.V (k, i)).presheaf.obj
              (op
                (Functor.obj (C := Opens (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
                  (opensFunctor (pullback.fst (D.f k i) (D.f k j)))
                  (unop
                    (op
                      (Functor.obj (Opens.map (Hom.base (pullback.fst (D.f k i) (D.f k j))))
                        ((Opens.map (D.t k i).base).obj
                          (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U))))))) ⟶
            (D.V (k, i)).presheaf.obj
              (op
                (Functor.obj (C := Opens (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
                  (opensFunctor (pullback.fst (D.f k i) (D.f k j))) ((Opens.map (D.t' k i j).base).1 U)))))

Tactic:
simp_rw [← (𝖣.V (k, i)).presheaf.map_comp]