-- 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
⊢ 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)
have 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)
Tactic: ext η Y f