Is the axiom of choice needed to prove $|G/H| \times |H| = |G|$ (Lagrange's Theorem)?

Question

Consider the following sequence of assertions, each of which implies the next. Nothing below has any topology, we just have sets and discrete groups.

1. If $F \hookrightarrow E \twoheadrightarrow B$ is fibre bundle of sets (this just means every fibre has the same cardinality), then $|E| = |F \times B|$
2. If $H \hookrightarrow E \twoheadrightarrow B$ is a principal bundle, then $|E| = |H \times B|$
3. If $H$ is a subgroup of $G$, then $|G| = |H \times G/H|$
4. If $H$ is a normal subgroup of $G$, then $|G| = |H \times G/H$|

Question: Do all these assertions fail without the axiom of choice? Or, which of them hold? I actually only care about (3), but for some reason I thought adding these extra statements might somehow clarify things.

Answer 1

Yes, the axiom of choice is needed, to some extent.

As bof mentions in the comments, it is always the case that $\Bbb{ Q\hookrightarrow R\twoheadrightarrow R/Q}$. However, as explained by Andrés E. Caicedo on MathOverflow, it is consistent that $\Bbb{R/Q}$ cannot be linearly ordered, as a set. In that case, it is impossible that $\Bbb{|R|=|Q\times R/Q|}$, as that would imply that you can linearly order $\Bbb{R/Q}$.

This should be a counterexample for all the cases.

If you are in the situation where all the equivalence classes in $G/H$ have the same cardinality as $H$ (e.g. like in the $\Bbb{R/Q}$ case), then as explained in the second part of this answer on MathOverflow, you can get the equality from the assumption that "cardinal multiplication is just 'repeated summation'", which is equivalent to the Partition Principle. However, it is still open if the Partition Principle is equivalent to the axiom of choice.

So it might be the case that having $|G|=|H\times G/H|$ implies the axiom of choice, even just from this equality in the Abelian case.