∀ {T : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} T] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{u_1, u_2} D] (F : CategoryTheory.Functor T D) (Y : D) (X : T)
  {Y_1 Z : CategoryTheory.CostructuredArrow ((CategoryTheory.Over.forget X).comp F) Y} (m : Y_1 ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (F.map
        (((CategoryTheory.CostructuredArrow.proj ((CategoryTheory.Over.forget X).comp F) Y).comp
              (CategoryTheory.Over.forget X)).map
          m))
      ((fun g => g.hom) Z) =
    (fun g => g.hom) Y_1