∀ {J : Type w} {inst : CategoryTheory.SmallCategory J} {κ : Cardinal.{w}}
  {D : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ} {e : J}
  {prop_id : D.W (CategoryTheory.CategoryStruct.id e)} {lift : {j : J} → D.P j → (j ⟶ e)}
  {hlift : ∀ {j : J} (hj : D.P j), D.W (lift hj)} {uniq : ∀ {j : J} (hj : D.P j) {φ : j ⟶ e}, D.W φ → lift hj = φ}
  {comm : ∀ {i j : J} (f : i ⟶ j) (hf : D.W f), CategoryTheory.CategoryStruct.comp f (lift ⋯) = lift ⋯}
  {prop_id_1 : D.W (CategoryTheory.CategoryStruct.id e)} {lift_1 : {j : J} → D.P j → (j ⟶ e)}
  {hlift_1 : ∀ {j : J} (hj : D.P j), D.W (lift_1 hj)}
  {uniq_1 : ∀ {j : J} (hj : D.P j) {φ : j ⟶ e}, D.W φ → lift_1 hj = φ}
  {comm_1 : ∀ {i j : J} (f : i ⟶ j) (hf : D.W f), CategoryTheory.CategoryStruct.comp f (lift_1 ⋯) = lift_1 ⋯},
  { prop_id := prop_id, lift := lift, hlift := hlift, uniq := uniq, comm := comm } =
      { prop_id := prop_id_1, lift := lift_1, hlift := hlift_1, uniq := uniq_1, comm := comm_1 } →
    lift = lift_1