-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasColimitsOfShape.{v', u', v, v + 1} J TopCat
F : J ⥤ PresheafedSpace.{v, u, v} C
j₁ j₂ j₃ : J
f : j₁ ⟶ j₂
g : j₂ ⟶ j₃
a :
  ∀ (U : (Opens (↑(colimit (F ⋙ forget C)) : Type v))ᵒᵖ),
    Eq (α :=
      obj (unop (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j₃)) (F.obj j₃).presheaf))) U ⟶
        obj (unop (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j₁)) (F.obj j₁).presheaf))) U)
      (NatTrans.app
        ((opEquiv (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j₁)) (F.obj j₁).presheaf))
              (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j₃)) (F.obj j₃).presheaf)) :
            (a :
                op ((pushforward C (colimit.ι (F ⋙ forget C) j₁)).obj (F.obj j₁).presheaf) ⟶
                  op ((pushforward C (colimit.ι (F ⋙ forget C) j₃)).obj (F.obj j₃).presheaf)) →
              unop (op ((pushforward C (colimit.ι (F ⋙ forget C) j₃)).obj (F.obj j₃).presheaf)) ⟶
                unop (op ((pushforward C (colimit.ι (F ⋙ forget C) j₁)).obj (F.obj j₁).presheaf)))
          (Quiver.Hom.op
            (map (pushforward C (colimit.ι (F ⋙ forget C) j₃)) (F.map (f ≫ g)).c ≫
              Iso.inv
                  (Pushforward.comp ((F ⋙ forget C).map (f ≫ g)) (colimit.ι (F ⋙ forget C) j₃) (F.obj j₁).presheaf) ≫
                Iso.hom (pushforwardEq ⋯ (F.obj j₁).presheaf))))
        U)
      (NatTrans.app
        ((opEquiv (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j₁)) (F.obj j₁).presheaf))
              (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j₃)) (F.obj j₃).presheaf)) :
            (a :
                op ((pushforward C (colimit.ι (F ⋙ forget C) j₁)).obj (F.obj j₁).presheaf) ⟶
                  op ((pushforward C (colimit.ι (F ⋙ forget C) j₃)).obj (F.obj j₃).presheaf)) →
              unop (op ((pushforward C (colimit.ι (F ⋙ forget C) j₃)).obj (F.obj j₃).presheaf)) ⟶
                unop (op ((pushforward C (colimit.ι (F ⋙ forget C) j₁)).obj (F.obj j₁).presheaf)))
          (Quiver.Hom.op
              (map (pushforward C (colimit.ι (F ⋙ forget C) j₂)) (F.map f).c ≫
                Iso.inv (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j₂) (F.obj j₁).presheaf) ≫
                  Iso.hom (pushforwardEq ⋯ (F.obj j₁).presheaf)) ≫
            Quiver.Hom.op
              (map (pushforward C (colimit.ι (F ⋙ forget C) j₃)) (F.map g).c ≫
                Iso.inv (Pushforward.comp ((F ⋙ forget C).map g) (colimit.ι (F ⋙ forget C) j₃) (F.obj j₂).presheaf) ≫
                  Iso.hom (pushforwardEq ⋯ (F.obj j₂).presheaf))))
        U)
⊢ Eq (α :=
    Quiver.Hom (V := Presheaf.{v, v, u} C (colimit (F ⋙ forget C)))
      (unop (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j₃)) (F.obj j₃).presheaf)))
      (unop (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j₁)) (F.obj j₁).presheaf))))
    ((opEquiv (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j₁)) (F.obj j₁).presheaf))
            (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j₃)) (F.obj j₃).presheaf)) :
          (a :
              op ((pushforward C (colimit.ι (F ⋙ forget C) j₁)).obj (F.obj j₁).presheaf) ⟶
                op ((pushforward C (colimit.ι (F ⋙ forget C) j₃)).obj (F.obj j₃).presheaf)) →
            unop (op ((pushforward C (colimit.ι (F ⋙ forget C) j₃)).obj (F.obj j₃).presheaf)) ⟶
              unop (op ((pushforward C (colimit.ι (F ⋙ forget C) j₁)).obj (F.obj j₁).presheaf)))
        (Quiver.Hom.op
          (map (pushforward C (colimit.ι (F ⋙ forget C) j₃)) (F.map (f ≫ g)).c ≫
            Iso.inv (Pushforward.comp ((F ⋙ forget C).map (f ≫ g)) (colimit.ι (F ⋙ forget C) j₃) (F.obj j₁).presheaf) ≫
              Iso.hom (pushforwardEq ⋯ (F.obj j₁).presheaf))) :
      Quiver.Hom (V := Presheaf.{v, v, u} C (colimit (F ⋙ forget C)))
        (unop (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j₃)) (F.obj j₃).presheaf)))
        (unop (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j₁)) (F.obj j₁).presheaf))))
    ((opEquiv (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j₁)) (F.obj j₁).presheaf))
            (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j₃)) (F.obj j₃).presheaf)) :
          (a :
              op ((pushforward C (colimit.ι (F ⋙ forget C) j₁)).obj (F.obj j₁).presheaf) ⟶
                op ((pushforward C (colimit.ι (F ⋙ forget C) j₃)).obj (F.obj j₃).presheaf)) →
            unop (op ((pushforward C (colimit.ι (F ⋙ forget C) j₃)).obj (F.obj j₃).presheaf)) ⟶
              unop (op ((pushforward C (colimit.ι (F ⋙ forget C) j₁)).obj (F.obj j₁).presheaf)))
        (Quiver.Hom.op
            (map (pushforward C (colimit.ι (F ⋙ forget C) j₂)) (F.map f).c ≫
              Iso.inv (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j₂) (F.obj j₁).presheaf) ≫
                Iso.hom (pushforwardEq ⋯ (F.obj j₁).presheaf)) ≫
          Quiver.Hom.op
            (map (pushforward C (colimit.ι (F ⋙ forget C) j₃)) (F.map g).c ≫
              Iso.inv (Pushforward.comp ((F ⋙ forget C).map g) (colimit.ι (F ⋙ forget C) j₃) (F.obj j₂).presheaf) ≫
                Iso.hom (pushforwardEq ⋯ (F.obj j₂).presheaf))) :
      Quiver.Hom (V := Presheaf.{v, v, u} C (colimit (F ⋙ forget C)))
        (unop (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j₃)) (F.obj j₃).presheaf)))
        (unop (op (obj (pushforward C (colimit.ι (F ⋙ forget C) j₁)) (F.obj j₁).presheaf))))

Tactic:
refine NatTrans.ext (funext fun U => ?_)

Premises used: CategoryTheory.NatTrans.ext, funext