∀ (R : Type u_1) [inst : CommRing R] (X : CoalgCat R),
  (TensorProduct.mk R ↑X.toModuleCat
          ↑(CategoryTheory.MonoidalCategoryStruct.tensorUnit (CoalgCat R)).toModuleCat).compr₂ₛₗ
      (ModuleCat.Hom.hom
        ((CategoryTheory.forget₂ (CoalgCat R) (ModuleCat R)).map
          (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom)) =
    (TensorProduct.mk R ↑X.toModuleCat
          ↑(CategoryTheory.MonoidalCategoryStruct.tensorUnit (CoalgCat R)).toModuleCat).compr₂ₛₗ
      (ModuleCat.Hom.hom
        (((CategoryTheory.Iso.refl
                  (CategoryTheory.MonoidalCategoryStruct.tensorObj
                    ((CategoryTheory.forget₂ (CoalgCat R) (ModuleCat R)).obj X)
                    ((CategoryTheory.forget₂ (CoalgCat R) (ModuleCat R)).obj
                      (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CoalgCat R))))).symm ≪≫
              CategoryTheory.MonoidalCategory.tensorIso
                (CategoryTheory.Iso.refl ((CategoryTheory.forget₂ (CoalgCat R) (ModuleCat R)).obj X))
                (CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat R))).symm) ≪≫
            CategoryTheory.MonoidalCategoryStruct.rightUnitor
              ((CategoryTheory.forget₂ (CoalgCat R) (ModuleCat R)).obj X)).hom)