∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_1, u_3} C] (X : C)
  {X_1 Y : CategoryTheory.Functor C (Type (max u_2 u_1))} (f : X_1 ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.uliftCoyoneda.{u_2, u_1, u_3}.rightOp.comp CategoryTheory.coyoneda).obj X).map f)
      ((fun x => (CategoryTheory.uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso) Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun x => (CategoryTheory.uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso) X_1).hom
      ((((CategoryTheory.evaluation C (Type (max u_1 u_2))).comp
                ((CategoryTheory.Functor.whiskeringRight (CategoryTheory.Functor C (Type (max u_1 u_2)))
                      (Type (max u_1 u_2)) (Type (max (max u_2 u_3) u_1))).obj
                  CategoryTheory.uliftFunctor.{u_3, max u_1 u_2})).obj
            X).map
        f)