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