-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : Category.{v₁, u₁} C
Y Z : Cᵒᵖ
f : Y ⟶ Z
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁) ⥤ Type (max u₁ v₁))
      (obj (Functor.op yoneda ⋙ coyoneda) Y)
      (obj
        (evaluation Cᵒᵖ (Type v₁) ⋙
          obj (whiskeringRight (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (Type v₁) (Type (max u₁ v₁)))
            uliftFunctor.{u₁, v₁})
        Z))
    (map (Functor.op yoneda ⋙ coyoneda) f ≫
      Iso.hom
        ((fun (X : Cᵒᵖ) ↦
            (NatIso.ofComponents
                (fun (x : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) ↦
                  Equiv.toIso (Equiv.trans yonedaEquiv (Equiv.symm Equiv.ulift)))
                ⋯ :
              Iso (C := Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁) ⥤ Type (max u₁ v₁))
                (obj (Functor.op yoneda ⋙ coyoneda) X)
                (obj
                  (evaluation Cᵒᵖ (Type v₁) ⋙
                    obj (whiskeringRight (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (Type v₁) (Type (max u₁ v₁)))
                      uliftFunctor.{u₁, v₁})
                  X)))
          Z))
    (Iso.hom
        ((fun (X : Cᵒᵖ) ↦
            (NatIso.ofComponents
                (fun (x : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) ↦
                  Equiv.toIso (Equiv.trans yonedaEquiv (Equiv.symm Equiv.ulift)))
                ⋯ :
              Iso (C := Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁) ⥤ Type (max u₁ v₁))
                (obj (Functor.op yoneda ⋙ coyoneda) X)
                (obj
                  (evaluation Cᵒᵖ (Type v₁) ⋙
                    obj (whiskeringRight (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (Type v₁) (Type (max u₁ v₁)))
                      uliftFunctor.{u₁, v₁})
                  X)))
          Y) ≫
      map
        (evaluation Cᵒᵖ (Type v₁) ⋙
          obj (whiskeringRight (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (Type v₁) (Type (max u₁ v₁)))
            uliftFunctor.{u₁, v₁})
        f)
have w : ∀ (F : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (g : obj (obj (Functor.op yoneda ⋙ coyoneda) Y) F),
  Eq (α :=
    obj
      (obj
        (evaluation Cᵒᵖ (Type v₁) ⋙
          obj (whiskeringRight (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (Type v₁) (Type (max u₁ v₁)))
            uliftFunctor.{u₁, v₁})
        Z)
      F)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (map (Functor.op yoneda ⋙ coyoneda) f ≫
            Iso.hom
              ((fun (X : Cᵒᵖ) ↦
                  (NatIso.ofComponents
                      (fun (x : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) ↦
                        Equiv.toIso (Equiv.trans yonedaEquiv (Equiv.symm Equiv.ulift)))
                      sorry :
                    Iso (C := Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁) ⥤ Type (max u₁ v₁))
                      (obj (Functor.op yoneda ⋙ coyoneda) X)
                      (obj
                        (evaluation Cᵒᵖ (Type v₁) ⋙
                          obj
                            (whiskeringRight (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (Type v₁) (Type (max u₁ v₁)))
                            uliftFunctor.{u₁, v₁})
                        X)))
                Z))
          F))
      g)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (Iso.hom
              ((fun (X : Cᵒᵖ) ↦
                  (NatIso.ofComponents
                      (fun (x : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) ↦
                        Equiv.toIso (Equiv.trans yonedaEquiv (Equiv.symm Equiv.ulift)))
                      sorry :
                    Iso (C := Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁) ⥤ Type (max u₁ v₁))
                      (obj (Functor.op yoneda ⋙ coyoneda) X)
                      (obj
                        (evaluation Cᵒᵖ (Type v₁) ⋙
                          obj
                            (whiskeringRight (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (Type v₁) (Type (max u₁ v₁)))
                            uliftFunctor.{u₁, v₁})
                        X)))
                Y) ≫
            map
              (evaluation Cᵒᵖ (Type v₁) ⋙
                obj (whiskeringRight (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (Type v₁) (Type (max u₁ v₁)))
                  uliftFunctor.{u₁, v₁})
              f)
          F))
      g)
Tactic: ext F g