-- Module: Mathlib.CategoryTheory.Limits.Preserves.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasColimitsOfShape.{v₂, u₂, v₁, v₁ + 1} J (Type v₁)
inst_3 : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
X : C
dsimp :
  Eq (α := (colimit (F ⋙ yoneda)).obj (op (obj yoneda X)) ⟶ obj yoneda X ⟶ colimit F)
    (CategoryStruct.comp (Y := colimit (F ⋙ obj coyoneda (op (obj yoneda X))))
        (Iso.hom (colimitObjIsoColimitCompEvaluation (F ⋙ yoneda) (op (obj yoneda X))) :
          (colimit (F ⋙ yoneda)).obj (op (obj yoneda X)) ⟶ colimit ((F ⋙ yoneda).flip.obj (op (obj yoneda X))))
        (CategoryStruct.comp (Y := colimit (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}))
            (colimMap (F.whiskerLeft (NatTrans.app (Iso.hom largeCurriedYonedaLemma) (op X))) :
              colimit (F ⋙ obj coyoneda (op (obj yoneda X))) ⟶
                colimit (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X) ⋙ uliftFunctor.{u₁, v₁}))
            (CategoryStruct.comp (Y := ULift.{u₁, v₁} (colimit (F.flip.obj (op X))))
                (Iso.inv (preservesColimitIso uliftFunctor.{u₁, v₁} (F.flip.obj (op X))))
                ((↾fun (x : ULift.{u₁, v₁} (colimit (F.flip.obj (op X)))) ↦
                    {
                      down :=
                        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                                (Iso.inv (colimitObjIsoColimitCompEvaluation F (op X))) :
                              TypeCat.Fun (colimit (F.flip.obj (op X))) ((colimit F).obj (op X))) :
                            (a : colimit (F.flip.obj (op X))) → (colimit F).obj (op X))
                          x.down }) ≫
                  (yonedaOpCompYonedaObj (colimit F)).inv.app (op X)) :
              colimit (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}) ⟶ obj yoneda X ⟶ colimit F) :
          colimit (F ⋙ obj coyoneda (op (obj yoneda X))) ⟶ obj yoneda X ⟶ colimit F) :
      (colimit (F ⋙ yoneda)).obj (op (obj yoneda X)) ⟶ obj yoneda X ⟶ colimit F)
    (CategoryStruct.comp (Y :=
        colimit
          ((F ⋙ yoneda) ⋙
            obj (evaluation (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁))ᵒᵖ (Type (max u₁ v₁))) (op (obj yoneda X))))
        (Iso.hom (colimitObjIsoColimitCompEvaluation (F ⋙ yoneda) (op (obj yoneda X))) :
          (colimit (F ⋙ yoneda)).obj (op (obj yoneda X)) ⟶
            colimit
              ((F ⋙ yoneda) ⋙
                obj (evaluation (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁))ᵒᵖ (Type (max u₁ v₁))) (op (obj yoneda X))))
        (colimit.post F (obj coyoneda (op (obj yoneda X))) :
          colimit (F ⋙ obj coyoneda (op (obj yoneda X))) ⟶ obj (obj coyoneda (op (obj yoneda X))) (colimit F)) :
      (colimit (F ⋙ yoneda)).obj (op (obj yoneda X)) ⟶ obj yoneda X ⟶ colimit F)
⊢ Eq (α :=
    (Functor.op yoneda ⋙ colimit (F ⋙ yoneda)).obj (op X) ⟶ (Functor.op yoneda ⋙ obj yoneda (colimit F)).obj (op X))
    (Iso.inv (Iso.app (yonedaYonedaColimit F) (op X)) :
      (Functor.op yoneda ⋙ colimit (F ⋙ yoneda)).obj (op X) ⟶ (Functor.op yoneda ⋙ obj yoneda (colimit F)).obj (op X))
    (CategoryStruct.comp (Y :=
        colimit
          ((F ⋙ yoneda) ⋙
            obj (evaluation (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁))ᵒᵖ (Type (max u₁ v₁)))
              (obj (Functor.op yoneda) (op X))))
        (Iso.hom (colimitObjIsoColimitCompEvaluation (F ⋙ yoneda) (obj (Functor.op yoneda) (op X))) :
          (colimit (F ⋙ yoneda)).obj (obj (Functor.op yoneda) (op X)) ⟶
            colimit
              ((F ⋙ yoneda) ⋙
                obj (evaluation (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁))ᵒᵖ (Type (max u₁ v₁)))
                  (obj (Functor.op yoneda) (op X))))
        (colimit.post F (obj coyoneda (op (obj yoneda X))) :
          colimit (F ⋙ obj coyoneda (op (obj yoneda X))) ⟶ obj (obj coyoneda (op (obj yoneda X))) (colimit F)) :
      (colimit (F ⋙ yoneda)).obj (obj (Functor.op yoneda) (op X)) ⟶
        (Functor.op yoneda ⋙ obj yoneda (colimit F)).obj (op X))

Tactic:
dsimp [yonedaYonedaColimit]

Premises used: CategoryTheory.yonedaYonedaColimit