-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Limits.HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
hf :
  IsOpenMap (X := (↑X : Type v)) (Y := (↑Y : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type v)) → (↑Y : Type v))
ℱ 𝒢 : TopCat.Presheaf C Y
u : ℱ ⟶ 𝒢
U : Opens (↑X : Type v)
j : CostructuredArrow (Opens.map f).op (op U)
eq :
  Eq (α := obj (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ) j ⟶ (obj (pullback C f) 𝒢).obj (op U))
    (CategoryStruct.comp (Y :=
        obj
          (obj (const (CostructuredArrow (Opens.map f).op (op U)))
            (Limits.Cocone.pt (J := CostructuredArrow (Opens.map f).op (op U))
              ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ)
                    ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
                (op U))))
          j)
        (NatTrans.app
          (Limits.Cocone.ι
            ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
              (op U)))
          j)
        (NatTrans.app (CategoryTheory.Functor.map (pullback C f) u) (op U)) :
      obj (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ) j ⟶ (obj (pullback C f) 𝒢).obj (op U))
    (NatTrans.app (whiskerLeft (CostructuredArrow.proj (Opens.map f).op (op U)) u) j ≫
        NatTrans.app
          (Limits.Cocone.ι
            ((LeftExtension.mk ((Opens.map f).op.leftKanExtension 𝒢) ((Opens.map f).op.leftKanExtensionUnit 𝒢)).coconeAt
              (op U)))
          j :
      obj (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ) j ⟶
        obj
          (obj (const (CostructuredArrow (Opens.map f).op (op U)))
            (Limits.Cocone.pt (J := CostructuredArrow (Opens.map f).op (op U))
              ((LeftExtension.mk ((Opens.map f).op.leftKanExtension 𝒢)
                    ((Opens.map f).op.leftKanExtensionUnit 𝒢)).coconeAt
                (op U))))
          j)
w :
  Eq (α := obj (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ) j ⟶ 𝒢.obj (op (hf.functor.obj U)))
    (NatTrans.app (whiskerLeft (CostructuredArrow.proj (Opens.map f).op (op U)) u) j ≫
        NatTrans.app
          (Limits.Cocone.ι
            (Limits.coconeOfDiagramTerminal (X :=
              CostructuredArrow.mk (Y :=
                op
                  {
                    carrier :=
                      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                              TopCat.carrier) f) :
                          (a : (↑X : Type v)) → (↑Y : Type v)) ''
                        (↑U : Set (↑X : Type v)),
                    is_open' := ⋯ })
                (Quiver.Hom.op (homOfLE ⋯)))
              {
                lift :=
                  fun
                    (s :
                      Limits.Cone (C := CostructuredArrow (Opens.map f).op (op U))
                        (empty (CostructuredArrow (Opens.map f).op (op U)))) ↦
                  CostructuredArrow.homMk (homOfLE ⋯).op ⋯,
                fac := ⋯, uniq := ⋯ }
              (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ 𝒢)))
          j :
      ℱ.obj (obj (CostructuredArrow.proj (Opens.map f).op (op U)) j) ⟶ 𝒢.obj (op (hf.functor.obj U)))
    (CategoryStruct.comp (Y :=
        Limits.Cocone.pt (J := CostructuredArrow (Opens.map f).op (op U)) (F :=
          CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ)
          (Limits.coconeOfDiagramTerminal (X :=
            CostructuredArrow.mk (Y :=
              op
                {
                  carrier :=
                    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                            TopCat.carrier) f) :
                        (a : (↑X : Type v)) → (↑Y : Type v)) ''
                      (↑U : Set (↑X : Type v)),
                  is_open' := ⋯ })
              (Quiver.Hom.op (homOfLE ⋯)))
            {
              lift :=
                fun
                  (s :
                    Limits.Cone (C := CostructuredArrow (Opens.map f).op (op U))
                      (empty (CostructuredArrow (Opens.map f).op (op U)))) ↦
                CostructuredArrow.homMk (homOfLE ⋯).op ⋯,
              fac := ⋯, uniq := ⋯ }
            (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ)))
        (NatTrans.app
            (Limits.Cocone.ι
              (Limits.coconeOfDiagramTerminal (X :=
                CostructuredArrow.mk (Y :=
                  op
                    {
                      carrier :=
                        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                                TopCat.carrier) f) :
                            (a : (↑X : Type v)) → (↑Y : Type v)) ''
                          (↑U : Set (↑X : Type v)),
                      is_open' := ⋯ })
                  (Quiver.Hom.op (homOfLE ⋯)))
                {
                  lift :=
                    fun
                      (s :
                        Limits.Cone (C := CostructuredArrow (Opens.map f).op (op U))
                          (empty (CostructuredArrow (Opens.map f).op (op U)))) ↦
                    CostructuredArrow.homMk (homOfLE ⋯).op ⋯,
                  fac := ⋯, uniq := ⋯ }
                (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ)))
            j :
          obj (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ) j ⟶
            obj
              (obj (const (CostructuredArrow (Opens.map f).op (op U)))
                (Limits.Cocone.pt (J := CostructuredArrow (Opens.map f).op (op U)) (F :=
                  CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ)
                  (Limits.coconeOfDiagramTerminal (X :=
                    CostructuredArrow.mk (Y :=
                      op
                        {
                          carrier :=
                            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v)))
                                    (CC := TopCat.carrier) f) :
                                (a : (↑X : Type v)) → (↑Y : Type v)) ''
                              (↑U : Set (↑X : Type v)),
                          is_open' := ⋯ : Opens (↑Y : Type v) })
                      (Quiver.Hom.op (homOfLE ⋯)))
                    {
                      lift :=
                        fun
                          (s :
                            Limits.Cone (C := CostructuredArrow (Opens.map f).op (op U))
                              (empty (CostructuredArrow (Opens.map f).op (op U)))) ↦
                        CostructuredArrow.homMk (homOfLE ⋯).op ⋯,
                      fac := ⋯, uniq := ⋯ :
                      Limits.IsLimit (C := CostructuredArrow (Opens.map f).op (op U))
                        (Limits.asEmptyCone
                          (CostructuredArrow.mk (Y :=
                            op
                              {
                                carrier :=
                                  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦
                                          C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) f) :
                                      (a : (↑X : Type v)) → (↑Y : Type v)) ''
                                    (↑U : Set (↑X : Type v)),
                                is_open' := ⋯ : Opens (↑Y : Type v) })
                            (Quiver.Hom.op (homOfLE ⋯)))) }
                    (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ))))
              j)
        (u.app (op (hf.functor.obj U))) :
      obj (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ) j ⟶ 𝒢.obj (op (hf.functor.obj U)))
⊢ Eq (α := obj (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ) j ⟶ 𝒢.obj (op (hf.functor.obj U)))
    (CategoryStruct.comp (Y :=
      obj
        (obj (const (CostructuredArrow (Opens.map f).op (op U)))
          (Limits.Cocone.pt (J := CostructuredArrow (Opens.map f).op (op U))
            ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
              (op U))))
        j)
      (NatTrans.app
        (Limits.Cocone.ι
          ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
            (op U)))
        j)
      (NatTrans.app (CategoryTheory.Functor.map (pullback C f) u) (op U) ≫
        Iso.hom
          (Limits.IsColimit.coconePointUniqueUpToIso
            ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit 𝒢 (op U))
            (Limits.colimitOfDiagramTerminal
              {
                lift :=
                  fun
                    (s :
                      Limits.Cone (C := CostructuredArrow (Opens.map f).op (op U))
                        (empty (CostructuredArrow (Opens.map f).op (op U)))) ↦
                  CostructuredArrow.homMk (homOfLE ⋯).op ⋯,
                fac := ⋯, uniq := ⋯ }
              (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ 𝒢)))))
    (CategoryStruct.comp (Y :=
      obj
        (obj (const (CostructuredArrow (Opens.map f).op (op U)))
          (Limits.Cocone.pt (J := CostructuredArrow (Opens.map f).op (op U))
            ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
              (op U))))
        j)
      (NatTrans.app
        (Limits.Cocone.ι
          ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
            (op U)))
        j)
      (CategoryStruct.comp (Y := ℱ.obj (op (hf.functor.obj U)))
        (Iso.hom
            (Limits.IsColimit.coconePointUniqueUpToIso
              ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit ℱ (op U))
              (Limits.colimitOfDiagramTerminal
                {
                  lift :=
                    fun
                      (s :
                        Limits.Cone (C := CostructuredArrow (Opens.map f).op (op U))
                          (empty (CostructuredArrow (Opens.map f).op (op U)))) ↦
                    CostructuredArrow.homMk (homOfLE ⋯).op ⋯,
                  fac := ⋯, uniq := ⋯ }
                (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ))) :
          (obj (pullback C f) ℱ).obj (op U) ⟶ ℱ.obj (op (hf.functor.obj U)))
        (u.app (op (hf.functor.obj U)) : ℱ.obj (op (hf.functor.obj U)) ⟶ 𝒢.obj (op (hf.functor.obj U)))))

Tactic:
rw [Limits.IsColimit.comp_coconePointUniqueUpToIso_hom_assoc, reassoc_of% eq,
    Limits.IsColimit.comp_coconePointUniqueUpToIso_hom]

Premises used: CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom_assoc