∀ {A : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} A} {B : Type u_2}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} B} {T : Type u_3} {inst_2 : CategoryTheory.Category.{v_3, u_3} T}
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B}
  {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W}
  {toCommaMorphism : CategoryTheory.CommaMorphism X.toComma Y.toComma} {prop_hom_left : Q toCommaMorphism.left}
  {prop_hom_right : W toCommaMorphism.right} {toCommaMorphism_1 : CategoryTheory.CommaMorphism X.toComma Y.toComma}
  {prop_hom_left_1 : Q toCommaMorphism_1.left} {prop_hom_right_1 : W toCommaMorphism_1.right},
  { toCommaMorphism := toCommaMorphism, prop_hom_left := prop_hom_left, prop_hom_right := prop_hom_right } =
      { toCommaMorphism := toCommaMorphism_1, prop_hom_left := prop_hom_left_1, prop_hom_right := prop_hom_right_1 } →
    toCommaMorphism = toCommaMorphism_1