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}$.

18more comments