∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {D : Type u_6}
  [inst_1 : CategoryTheory.Category.{u_3, u_6} D] {E : Type u_5} [inst_2 : CategoryTheory.Category.{u_4, u_5} E]
  (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) {X Y Z : CategoryTheory.Comma L R} (f : X ⟶ Y)
  (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      { base := (CategoryTheory.CategoryStruct.comp f g).right,
          fiber := CategoryTheory.CostructuredArrow.homMk (CategoryTheory.CategoryStruct.comp f g).left ⋯ }.fiber =
    (CategoryTheory.CategoryStruct.comp { base := f.right, fiber := CategoryTheory.CostructuredArrow.homMk f.left ⋯ }
        { base := g.right, fiber := CategoryTheory.CostructuredArrow.homMk g.left ⋯ }).fiber