∀ {C : Type u_1} [inst : CategoryTheory.SmallCategory C] {X Y : Cᵒᵖ} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.yoneda.op.comp CategoryTheory.coyoneda).map f)
      ((fun X => CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.yonedaEquiv.toIso) ⋯) Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun X => CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.yonedaEquiv.toIso) ⋯) X).hom
      ((CategoryTheory.evaluation Cᵒᵖ (Type u_1)).map f)