∀ {C : Type u_3} {inst : CategoryTheory.Category.{u_2, u_3} C} {J : Type u_1} {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}
  (motive : CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct c p f g j → Prop)
  (h : CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct c p f g j),
  (∀ (f' : F.obj j ⟶ X)
      (w₁ :
        autoParam (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.homOfLE ⋯)) f' = f)
          CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₁._autoParam)
      (w₂ :
        autoParam (CategoryTheory.CategoryStruct.comp f' p = CategoryTheory.CategoryStruct.comp (c.ι.app j) g)
          CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₂._autoParam),
      motive { f' := f', w₁ := w₁, w₂ := w₂ }) →
    motive h