Prove $[G:H]=[G':H']$ where $H$ and $H'$ are corresponding subgroups preferably without product or quotient groups. For a surjective homomorphism $\varphi: G \to G'$ where $\ker \varphi \subseteq H$, $H$ is a subgroup of $G$ that corresponds to $H'$, a subgroup of $G'$, the correspondence theorem implies $$\varphi(H)=H',$$ $$\varphi^{-1}(H')=H,$$ $$|H|=|H'| |\ker(\varphi)|,$$ $$\varphi(G)=G'$$ From counting formula, $$|H|=[H: \ker \varphi]|\ker \varphi|,$$ $$|G|=[G: \ker \varphi]|\ker \varphi|,$$ $$|G|=[G: H]|H|,$$ $$|G'|=[G': H]|H'|$$
Additionally, from $\varphi: G \to G'$ and from $\varphi|_H : H \to H'$,  $$[G:\ker \varphi] = |\varphi(G)|=|G'|,$$ $$[H:\ker (\varphi|_H)] = [H:\ker \varphi \cap H]$$$$ = [H:\ker \varphi] = |\varphi|_H(H)|=|\varphi(H)|=|H'|$$
Proving $[G:H]=[G':H']$ is easy if I can divide (Blake Griffith of Github proves like this):
$$[G:H]=\frac{|G|}{|H|}=\frac{|G|}{|H'||\ker \varphi|}$$$$=\frac{[G:\ker \varphi]|\ker \varphi|}{|H'||\ker \varphi|}$$$$=\frac{[G:\ker \varphi]}{|H'|}=\frac{|G'|}{|H'|}=[G':H']$$
But if I can't, what can I do? From
$$|G'| = [G':H']|H'| = [G:H]|H'|$$


*

*If $|G'| < \infty$, then $|H'| < \infty$ and then there is no problem.

*If both $[G:H] = [G':H'] = \infty$ then there is no problem. 

*If $|G'| = \infty$, then ($[G':H'] = \infty$ or $|H'| = \infty$) and ($[G:H] = \infty$ or $|H'| = \infty$).

*If $|G'| = \infty$ and we don't have that both $[G:H] = [G':H'] = \infty$, then we are left with 5 cases, and each case assumes $|H'| = \infty$.
Let $b':=[G':H'],b:=[G:H]$.


*

*$b < b' < \infty$

*$b' < b < \infty$

*$b<\infty=b'$

*$b'<\infty=b$

*$b = b' < \infty$
For 1 and 3, I can derive a contradiction: Let $G$ be partitioned $$G=\bigcup_{i=1}^{n}z_iH \implies G' = \varphi(G) = \bigcup_{i=1}^{n}\varphi(z_iH) = \bigcup_{i=1}^{n}\varphi(z_i)H' \implies b'=b<\infty$$
For 2 and 4, I am stuck: Let $G'$ be partitioned $$G'=\bigcup_{j=1}^{m}w_jH' \implies G = \varphi^{-1}(G') = \bigcup_{j=1}^{m}\varphi^{-1}(w_jH') = \bigcup_{j=1}^{m}\varphi^{-1}(w_j)H$$
where
$$\varphi^{-1}(w_j)H := \{u_jh \mid \varphi(u_j)=w_j, h \in H\}$$
I don't know how to derive cosets from this since $\varphi$ is not assumed to be injective, a $\varphi^{-1}(w_j)$ might be infinite, and I don't even know if $$\bigcup_{j=1}^{m}\varphi^{-1}(w_jH') = \bigcup_{j=1}^{m}\varphi^{-1}(w_j)H$$ I proved $\supseteq$, but I think $\subseteq$ is not true if not injective.
Finally, I did not use disjointedness in the partitioning. That could be helpful.
 A: First, note that $H$ is a subgroup of $G$ that contains $K:=\ker(\varphi)$.  Therefore, $H/K$ is a subgroup of the factor group $G/K$.  Define
$$f:(G/H)\to \big((G/K)\big/(H/K)\big)\text{ by setting }f(gH):=g(H/K)\text{ for every }g\in G\,.$$
Show that this is a well defined function (and in fact, it is a homomorphism of left $G$-sets).  Furthermore, verify that $f$ is bijective.
Now, the surjective map $\varphi:G\to G'$ induces a function $\Phi:\big((G/K)\big/(H/K)\big)\to (G'/H')$ via
$$\Phi\big(g(H/K)\big):=\varphi(g)\,H'\text{ for each }g\in G\,.$$
(This is again an isomorphism of left $G$-sets, if we equip $G'$ with the left $G$-action from $\varphi$, namely, $g\cdot g':=\varphi(g)\,g'$ for every $g\in G$ and $g'\in G'$.)  The definition of $\Phi$ is inspired the group isomorphism $\phi:(G/K)\to G'$ induced by $\varphi$, which is given by $\phi(gK):=\varphi(g)$ for every $g\in G$.
Consequently, $\psi:=\Phi\circ f:(G/H)\to (G'/H')$ is simply the bijective function
$$\psi(gH)=\varphi(g)\,H'\text{ for all }g\in G\,,\tag{*}$$
which is also an isomorphism of left $G$-sets.  This shows that
$$[G:H]=|G/H|=|G'/H'|=[G':H']\,,$$
which is also equal to $\big[(G/K):(H/K)\big]=\big|(G/K)\big/(H/K)\big|$.
P.S.: You can directly define $\psi$ using (*) and show that it is a bijective function, without defining $f$ and $\Phi$.  In this way, you don't need to deal with factor groups $G/K$ and $H/K$.  However, I think that understanding the correspondence of $G/H$ or $G'/H'$ with $(G/K)\big/(H/K)$ gives you a new perspective.
A: Consider the map
$$\Phi \colon \{ \text{cosets of H} \} \to \{ \text{cosets of H'} \},\ xH \mapsto \phi(x)H'  $$
and show that $\Phi$ is well-defined and bijective.
