∀ {J : Type u_1} {K : Type u_2} (X : CategoryTheory.Discrete J × CategoryTheory.Discrete K),
  CategoryTheory.Discrete.productEquiv.counitIso.hom.app X =
    CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1) (CategoryTheory.CategoryStruct.id X.2)