∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {Y X : C} (f : Y ≅ X) {Y_1 Z : CategoryTheory.Over X}
  (g : Y_1 ⟶ Z),
  CategoryTheory.CategoryStruct.comp g.left
      (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.comp Z.hom f.inv)).hom =
    (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.comp Y_1.hom f.inv)).hom