∀ {R : Type u_1} [inst : CommRing R] (x : ModuleCat R),
  ModuleCat.equivalenceSemimoduleCat.functor.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor x).hom =
    (((CategoryTheory.Iso.refl
              (CategoryTheory.MonoidalCategoryStruct.tensorObj
                (ModuleCat.equivalenceSemimoduleCat.functor.obj
                  (CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat R)))
                (ModuleCat.equivalenceSemimoduleCat.functor.obj x))).symm ≪≫
          CategoryTheory.MonoidalCategory.tensorIso
            (CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategoryStruct.tensorUnit (SemimoduleCat R))).symm
            (CategoryTheory.Iso.refl (ModuleCat.equivalenceSemimoduleCat.functor.obj x))) ≪≫
        CategoryTheory.MonoidalCategoryStruct.leftUnitor (ModuleCat.equivalenceSemimoduleCat.functor.obj x)).hom