∀ {C : Type u_3} {D : Type u_4} {H : Type u_6} [inst : CategoryTheory.Category.{u_1, u_3} C]
  [inst_1 : CategoryTheory.Category.{u_2, u_4} D] [inst_2 : CategoryTheory.Category.{u_5, u_6} H]
  (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor D H) (α : L.comp G ⟶ F)
  (Y : D) ⦃X Y_1 : CategoryTheory.StructuredArrow Y L⦄ (f : X ⟶ Y_1),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Functor.const (CategoryTheory.StructuredArrow Y L)).obj (G.obj Y)).map f)
      (CategoryTheory.CategoryStruct.comp (G.map Y_1.hom) (α.app Y_1.right)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (G.map X.hom) (α.app X.right))
      (((CategoryTheory.StructuredArrow.proj Y L).comp F).map f)