-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Yoneda (goal)
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
⊢ 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)
have 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)
Tactic: dsimp [largeCurriedYonedaLemma, yonedaOpCompYonedaObj, yonedaEquiv]