∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {U V : C} (f₁ f₂ : U ⟶ V) {Y Z : C} {f : Y ⟶ U},
  CategoryTheory.CategoryStruct.comp f f₁ = CategoryTheory.CategoryStruct.comp f f₂ →
    ∀ (g : Z ⟶ Y),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp g f) f₁ =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp g f) f₂