∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} {f f_1 : A ⟶ X} (e_f : f = f_1)
  {i i_1 : A ⟶ B} (e_i : i = i_1) {p p_1 : X ⟶ Y} (e_p : p = p_1) {g g_1 : B ⟶ Y} (e_g : g = g_1)
  (sq : CategoryTheory.CommSq f i p g), sq.HasLift = ⋯.HasLift