∀ {α : Type u} {β : Type u₂} [inst : CategoryTheory.Category.{v, u} α] [inst_1 : CategoryTheory.Category.{v₂, u₂} β]
  [CategoryTheory.IsGroupoid α] [CategoryTheory.IsGroupoid β], CategoryTheory.IsGroupoid (α × β)