-- 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 :
  ∀ (η : obj yoneda X ⟶ F.obj j) (Y : Cᵒᵖ) (f : obj (obj yoneda X) 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)
⊢ Eq (α := (obj yoneda X ⟶ F.obj j) ⟶ obj yoneda X ⟶ colimit F)
    (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 })
        ((↾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 }) ≫
          (yonedaOpCompYonedaObj (colimit F)).inv.app (op X)))
    (↾fun (g : obj yoneda X ⟶ F.obj j) ↦ g ≫ colimit.ι F j)

Tactic:
ext η Y f