∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {J : Type u_3} [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) [inst_3 : SuccOrder J] (j : J)
  (sq' : (CategoryTheory.HasLiftingProperty.transfiniteComposition.sqFunctor c p f g).obj (Opposite.op j))
  (this :
    ∀
      (sq :
        CategoryTheory.CommSq sq'.f' (F.map (CategoryTheory.homOfLE ⋯)) p
          (CategoryTheory.CategoryStruct.comp (c.ι.app (Order.succ j)) g)),
      sq.HasLift),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.homOfLE ⋯)) ⋯.lift = f