∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {A B X Y : C} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y}
  {g : B ⟶ Y} {sq : CategoryTheory.CommSq f i p g} {l : B ⟶ X}
  {fac_left :
    autoParam (CategoryTheory.CategoryStruct.comp i l = f) CategoryTheory.CommSq.LiftStruct.fac_left._autoParam}
  {fac_right :
    autoParam (CategoryTheory.CategoryStruct.comp l p = g) CategoryTheory.CommSq.LiftStruct.fac_right._autoParam}
  {l_1 : B ⟶ X}
  {fac_left_1 :
    autoParam (CategoryTheory.CategoryStruct.comp i l_1 = f) CategoryTheory.CommSq.LiftStruct.fac_left._autoParam}
  {fac_right_1 :
    autoParam (CategoryTheory.CategoryStruct.comp l_1 p = g) CategoryTheory.CommSq.LiftStruct.fac_right._autoParam},
  { l := l, fac_left := fac_left, fac_right := fac_right } =
      { l := l_1, fac_left := fac_left_1, fac_right := fac_right_1 } →
    l = l_1