∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} {X Y : C} {p : X ⟶ Y} {f : F.obj ⊥ ⟶ X}
  {g : c.pt ⟶ Y} {j : J} (self : CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct c p f g j),
  CategoryTheory.CategoryStruct.comp self.f' p = CategoryTheory.CategoryStruct.comp (c.ι.app j) g