Is Lagrange's Theorem equivalent to AC? Lagrange's Theorem is most often stated for finite groups, but it has a natural formation for infinite groups too: if $G$ is a group and $H$ a subgroup of $G$, then $|G| = |G:H| \times |H|$.
If we assume AC, the we get a fairly straightforward proof (pick a representative of each coset, and then let your map $(G : H) \times H \to G$ be $(gH, h) \mapsto gh$).
However, somebody told me someone told them that the converse is true too, i.e. Lagrange's Theorem gives us AC. (Indeed, the wikipedia page for LT offhandedly mentions they're equivalent without a reference). Does anybody have a proof (or alternatively a proof AC is stronger than LT)?
 A: Lagrange's Theorem does not follow from ZF. In fact, the following weaker statement also does not follow:
$\sf LT^{-}$: Let $H$ be a subgroup of $G$. Then $|H|$ divides $|G|$, i.e. there exists a set $A$ s.t. $|H| \times |A| = |G|$.
(The name LT$^{-}$ is not standard, but in the vein of the name LT$^{+}$.)
I stumbled upon the paper The Construction of Groups in models of set theory that fail the Axiom of Choice (Hickman, 1976) where he constructs a model of ZF with an amorphous group (a group whose carrier set is amorphous, i.e. an infinite set that isn't the disjoint union of two infinite sets).
He then goes on to prove several properties about amorphous groups, including the following:

Suppose $G$ is an amorphous group, and $H \leq G$ a finite non-trivial subgroup. (Such a subgroup always exists: every element in $G$ has finite order as $G$ has no $\aleph_0$ subset.)
Suppose that there was a set $A$ and a bijection $f \colon H \times A \to G$. As $H$ is finite, $A$ must be infinite. But then for any $h_1 \neq h_2 \in H$, $f(\{h_1\} \times A)$ and $f(\{h_2\} \times A)$ are infinite disjoint subsets of $G$, contradicting $G$ being amorphous.

So we need some 'choice' (i.e. a statement along the lines of 'no amorphous sets exist' or 'every infinite set is Dedekind-infinite') at the very least to have LT. How much is still unclear.
A: The following version of Lagrange's theorem is equivalent to AC: 
LT+: Let $H$ be a subgroup of the group $G$. Then there is a bijection $k: (G:H)\times H\to G$ such that for each $(\tilde{g},h)\in (G:H)\times H$, the image $k((\tilde{g},h))$ is in $\tilde{g}$.
That AC implies LT+ was already shown in the question. To show that LT+ implies AC, the additive notation seems easier.
Let $P\subseteq X\times Y$ be sets such that $\forall x\in X\exists y\in Y[(x,y)\in P]$. We wish to derive from LT+ the existence of an $f\subseteq P$ such that $\forall x\in X\exists! y\in Y[(x,y)\in f]$.
For this we construct a group $G$ as follows. First, let $L$ be the free non-abelian group on $X$ [as specified at the bottom of this answer], and $M$ the free non-abelian group on $P$. Then let $G$ be the `diagonal' subgroup of the group $L\times M$ generated by $\{(x,(x,a))\mid (x,a)\in P\}$. Let $H$ be the subgroup of G generated by $\{(\mathbf{0},(x,a)-(x,b))\mid (x,a), (x,b)\in P\}$. 
Taking right cosets $H/G$ amounts to identifying $(x,(x,a))$ with $(x,(x,b))$, for $x$ and $a,b$ such that both $(x,a),(x,b)\in P$. More precisely, the right $H$-coset of $(x,(x,a))$ is independent of $a$:
$\tilde{x}:=\{(x, \Sigma_{i<n}((z_i,w_i)-(z_i,v_i))+(x,a))\mid n\in \mathbb{N},(z_i,w_i), (z_i,v_i)\in P, (x,a)\in P\}$ 
$\tilde{x}$ contains $(x, (x,b))$ for all $b$ such that $(x,b)\in P$. But more importantly, every element of $\tilde{x}$ pinpoints a single $c$ such that $(x,c)\in P$. Because in $M$ there is only one interpretation of the expression $\Sigma_{i<n}((z_i,w_i)-(z_i,v_i))+(x,a)$, and this is a finite sequence in $(P\times\{-1,1\})^*$ [see below]. Every element of $\tilde{x}$ is derived from an $M$-sum in the second coordinate, such as $(x,\Sigma_{i<n}((z_i,w_i)-(z_i,v_i))+(x,a))$, and in this $M$-sum there is always a term $(x,c)$ for some $c$. So we can look for the first occurrence (smallest index) of such a term $(x,c)$, and this is canonical (no choice). Therefore there is a function $s: \bigcup\{\tilde{x}\mid x\in X\}\to Y$ such that for all $u\in\tilde{x}$ we have that $(x,s(u))\in P$.
By LT+ there is a bijection $k: (G:H)\times H\to G$ such that for each $(\tilde{g},h)\in (G:H)\times H$, the image $k((\tilde{g},h))$ is in $\tilde{g}$.
We now define the desired $f$ as follows:
$f(x):= s(k(\tilde{x},\mathbf{0}_G))$
[This is an edited answer after Emil pointed out the fallacies in the original answer which used the free abelian group construction. To understand the comments, the original answer can be refound by replacing non-abelian with abelian.]
For a set $W$, form a `free' non-abelian group $F(W)$ as follows. First, giving each element $w$ of $W$ an inverse $-w$, we come to consider $K=W\times\{-1,1\}$, and write $w$ for $(w,1)$ and $-w$ for $(w,-1)$, and sometimes as abbreviation $-(-w)$ for $w$. To avoid having to quotient/project/select, we look at finite sums of these elements, that is finite sequences $(k_1,...,k_n)$ in $K^*=\bigcup \{K^n\mid n\in\mathbb{N}\}$ in which we have already removed the partial sums that yield $0$. In other words, there is no $i<n$ such that $k_i = z$ and $k_{i+1}=-z$. So put $F(W)=\{(k_1,...,k_n)\in K^*\mid \forall i<n [k_i \neq -k_{i+1}], n\in\mathbb{N}\}$. With the empty sequence as $0$, this yields a non-abelian group structure on $F(W)$ by putting $(k_1,...,k_n)+(l_1,...,l_m):= (k_1,...,k_n,l_1,...,l_m)$ if $k_n\neq -l_1$, and $(k_1,...,k_n)+(l_1,...,l_m):= (k_1,...,k_{n-1})+(l_2,...,l_m)$ if $k_n = -l_1$. ($k_n = -l_1$ is an abbreviation of two different cases, and the definition is inductive in the length $n$, meaning that we cancel out neighboring opposite terms in the sequence $(k_1,...,k_n,l_1,...,l_m)$ one after the other, as far as possible).
The nice thing about $F(W)$ is that all its elements are unique representations of finite sums. For elements $s_0,...,s_{n-1}$ in $F(W)$ we write $\Sigma_{i< n}s_i$ to denote the element $s_0+s_1+...+s_{n-1}$.
