I don't think the statement that you linked in your revised question needs a reference, or even an explicit proof. The fact that comodule structures can be pushed forward along coalgebra homomorphisms is sufficiently clear that you should be able to get away with stating a precise claim. Similarly, I think the statement that the structure of a $G \times H$-module is equivalent to commuting $G$-module and $H$-module structures is also straightforward enough that you can state it without proof or reference. (Others may disagree, but I think I'm on the majority side in this particular case.) A common way to deal with straightforward facts that are often used later in a paper is to write the claim as a lemma, followed by: > **Proof:** Omitted. If the proof is not entirely obvious, it may help to write a sentence or two on how to get through the tricky part.