∀ {A : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} A] {B : Type u_6}
  [inst_1 : CategoryTheory.Category.{u_5, u_6} B] {T : Type u_2} [inst_2 : CategoryTheory.Category.{u_1, u_2} T]
  {C : Type u_8} [inst_3 : CategoryTheory.Category.{u_7, u_8} C] (L : CategoryTheory.Functor A T)
  (F : CategoryTheory.Functor C B) (R : CategoryTheory.Functor B T) {X Y : CategoryTheory.Comma L (F.comp R)}
  (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (L.map f.left) { left := Y.left, right := F.obj Y.right, hom := Y.hom }.hom =
    CategoryTheory.CategoryStruct.comp { left := X.left, right := F.obj X.right, hom := X.hom }.hom
      (R.map (F.map f.right))