∀ {α : Type u_1} {β : Type u_2} [inst : CategoryTheory.Groupoid α] [inst_1 : CategoryTheory.Groupoid β] {X Y : α × β}
  (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Groupoid.inv f.1, CategoryTheory.Groupoid.inv f.2) f =
    CategoryTheory.CategoryStruct.id Y