-- 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
η : obj yoneda X ⟶ F.obj j
Y : Cᵒᵖ
f : obj (obj yoneda X) Y
w :
  Eq (α := (colimit F).obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((colimit F).map (Quiver.Hom.op f)) :
          (a : (colimit F).obj (op X)) → (colimit F).obj Y)
        (((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (colimitObjIsoColimitCompEvaluation F (op X))) :
                TypeCat.Fun (colimit (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X))) ((colimit F).obj (op X))) :
              (a : colimit (F ⋙ (evaluation Cᵒᵖ (Type v₁)).obj (op X))) → (colimit F).obj (op X))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X)) j) :
                  (a : (F.obj j).obj (op X)) → colimit (F ⋙ (evaluation Cᵒᵖ (Type v₁)).obj (op X)))
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app (op X)) : (a : X ⟶ X) → (F.obj j).obj (op X)) (𝟙 X) :
                  (F.obj j).obj (op X)) :
              colimit (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X))) :
          (colimit F).obj (op X)) :
      (colimit F).obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι F j) Y) :
          (a : (F.obj j).obj Y) → (colimit F).obj Y)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app Y) : (a : unop Y ⟶ X) → (F.obj j).obj Y) f :
          (F.obj j).obj Y) :
      (colimit F).obj Y)
⊢ Eq (α := (colimit F).obj Y)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (TypeCat.Fun.toFun
            (ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app (NatTrans.app (Iso.hom largeCurriedYonedaLemma) (op X)) (F.obj j) ≫
                CategoryStruct.comp (Y := ULift.{u₁, v₁} (colimit (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X))))
                  (↾fun (x : ULift.{u₁, v₁} ((F.obj j).obj (op X))) ↦
                    {
                      down :=
                        (ConcreteCategory.hom (FC := TypeCat.Fun)
                              (colimit.ι (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X)) j) :
                            (a : (F.obj j).obj (op X)) → colimit (F ⋙ (evaluation Cᵒᵖ (Type v₁)).obj (op X)))
                          x.down :
                      ULift.{u₁, v₁} (colimit (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X))) })
                  ((↾fun (x : ULift.{u₁, v₁} (colimit (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X)))) ↦
                      {
                        down :=
                          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                                  (Iso.inv (colimitObjIsoColimitCompEvaluation F (op X))) :
                                TypeCat.Fun (colimit (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X)))
                                  ((colimit F).obj (op X))) :
                              (a : colimit (F ⋙ (evaluation Cᵒᵖ (Type v₁)).obj (op X))) → (colimit F).obj (op X))
                            x.down :
                        ULift.{u₁, v₁} ((colimit F).obj (op X)) }) ≫
                    (yonedaOpCompYonedaObj (colimit F)).inv.app (op X))))
            η)
          Y))
      f)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (TypeCat.Fun.toFun
            (ConcreteCategory.hom (FC := TypeCat.Fun) (↾fun (g : obj yoneda X ⟶ F.obj j) ↦ g ≫ colimit.ι F j)) η)
          Y))
      f)

Tactic:
dsimp [largeCurriedYonedaLemma, yonedaOpCompYonedaObj, yonedaEquiv]

Premises used: CategoryTheory.yonedaOpCompYonedaObj, CategoryTheory.yonedaEquiv, CategoryTheory.largeCurriedYonedaLemma