∀ {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} [inst_3 : F.IsWellOrderContinuous] {j : J} (hj : Order.IsSuccLimit j)
  (s : ↑(⋯.functor.op.comp (CategoryTheory.HasLiftingProperty.transfiniteComposition.sqFunctor c p f g)).sections)
  {i : J} (hij : i < j),
  CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.map
      (CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.lift hj s)
      (CategoryTheory.homOfLE ⋯) =
    ↑s (Opposite.op ⟨i, hij⟩)