∀ {A : Type u_4} [inst : CategoryTheory.Category.{u_1, u_4} A] {B : Type u_8}
  [inst_1 : CategoryTheory.Category.{u_7, u_8} B] {T : Type u_6} [inst_2 : CategoryTheory.Category.{u_3, u_6} T]
  {C : Type u_5} [inst_3 : CategoryTheory.Category.{u_2, u_5} 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 ((CategoryTheory.Comma.preRight L F R).map f)
      ((fun X =>
            CategoryTheory.Comma.isoMk (CategoryTheory.Iso.refl ((CategoryTheory.Comma.preRight L F R).obj X).left)
              (CategoryTheory.Iso.refl ((CategoryTheory.Comma.preRight L F R).obj X).right) ⋯)
          Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun X =>
            CategoryTheory.Comma.isoMk (CategoryTheory.Iso.refl ((CategoryTheory.Comma.preRight L F R).obj X).left)
              (CategoryTheory.Iso.refl ((CategoryTheory.Comma.preRight L F R).obj X).right) ⋯)
          X).hom
      ((CategoryTheory.Comma.map (CategoryTheory.CategoryStruct.comp L.leftUnitor.hom L.rightUnitor.inv)
            (F.comp R).rightUnitor.hom).map
        f)