In a comment for this old question, it was said that

> There is a theorem that Hopf modules are (up to isomorphism) the tensor products of their coinvariants with H. (This theorem is usually worded in terms of a category equivalence. I don't know a good reference.)

I'm guessing that this means that given a (right) $H$-comodule $V$, for $H$ a Hopf algebra, equipped with a right $H$ action for which $\Delta_R(vh) = v_{(0)} g_{(0)} \otimes v_{(1)}g_{(1)}$, we have an isomorphism $$ V \simeq V_{\text{inv}} \otimes H $$ Now it's easy to see that we have a surjective map $$ V_{\text{inv}} \otimes H \to V, ~~~ v \otimes h \mapsto vh. $$ How does one show that this is an isomorphism?

EDIT: Wait, I think this is actually obvious: The map $$ V \to V_{\text{inv}} \otimes H, ~~~~~ v \mapsto v_{(0)} S(v_{(1)}) \otimes v_{(2)}, $$ seems to have the multiplication map as its inverse. So this gives us the isomorphism. Yes?