∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] (F : CategoryTheory.Functor Cᵒᵖ (Type u_2))
  {X Y : F.Elementsᵒᵖ} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.id F.Elementsᵒᵖ).map f)
      ((fun X =>
            (CategoryTheory.CategoryOfElements.isoMk
                ((CategoryTheory.CategoryOfElements.fromCostructuredArrow F).obj
                  (Opposite.op ((CategoryTheory.CategoryOfElements.toCostructuredArrow F).obj X)))
                (Opposite.unop X)
                (CategoryTheory.Iso.refl
                  ((CategoryTheory.CategoryOfElements.fromCostructuredArrow F).obj
                      (Opposite.op ((CategoryTheory.CategoryOfElements.toCostructuredArrow F).obj X))).fst)
                ⋯).op)
          Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun X =>
            (CategoryTheory.CategoryOfElements.isoMk
                ((CategoryTheory.CategoryOfElements.fromCostructuredArrow F).obj
                  (Opposite.op ((CategoryTheory.CategoryOfElements.toCostructuredArrow F).obj X)))
                (Opposite.unop X)
                (CategoryTheory.Iso.refl
                  ((CategoryTheory.CategoryOfElements.fromCostructuredArrow F).obj
                      (Opposite.op ((CategoryTheory.CategoryOfElements.toCostructuredArrow F).obj X))).fst)
                ⋯).op)
          X).hom
      (((CategoryTheory.CategoryOfElements.toCostructuredArrow F).comp
            (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp).map
        f)