∀ (R : Type u_3) {ι : Type u_2} [inst : Ring R] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (i : ι) (X : ModuleCat R),
  CategoryTheory.CategoryStruct.comp ((ModuleCat.toMatrixModCat R ι).map ((MatrixModCat.unitIso R i).symm.hom.app X))
      ((MatrixModCat.counitIso R i).hom.app ((ModuleCat.toMatrixModCat R ι).obj X)) =
    CategoryTheory.CategoryStruct.id ((ModuleCat.toMatrixModCat R ι).obj X)