-- 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
j : J
w :
  Eq (α := (F ⋙ obj coyoneda (op (obj yoneda X))).obj j ⟶ obj yoneda X ⟶ colimit F)
    ((F.whiskerLeft (NatTrans.app (Iso.hom largeCurriedYonedaLemma) (op X))).app j ≫
      CategoryStruct.comp (Y := colimit (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X) ⋙ uliftFunctor.{u₁, v₁}))
        (colimit.ι (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X) ⋙ uliftFunctor.{u₁, v₁}) j :
          (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X) ⋙ uliftFunctor.{u₁, v₁}).obj j ⟶
            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))
    (map (obj coyoneda (op (obj yoneda X))) (colimit.ι F j))
⊢ CategoryStruct.comp (Y := colimit (F ⋙ obj coyoneda (op (obj yoneda X))))
      (colimit.ι (F ⋙ obj coyoneda (op (obj yoneda X))) j)
      (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)) =
    CategoryStruct.comp (Y := colimit (F ⋙ obj coyoneda (op (obj yoneda X))))
      (colimit.ι (F ⋙ obj coyoneda (op (obj yoneda X))) j) (colimit.post F (obj coyoneda (op (obj yoneda X))))

Tactic:
rw [colimit.ι_post, ι_colimMap_assoc]

Premises used: CategoryTheory.Limits.colimit.ι_post, CategoryTheory.Limits.ι_colimMap_assoc