Proof that $|HK|=|H||K|/|H \cap K|$ for $H,K,HK$ subgroups of $G$ I've found this problem in a book and devised my own proof.
(took me like 5 hours and it seems trivial - just build a bijection).
I am not sure that I haven't made any errors though.
Perhaps some other proof would be simpler.
Statement:
$G$ is a group and $H,K,HK \subseteq G$
Prove that $|HK|=\frac{|H||K|}{|H \cap K|}$
Proof:
The statement above is equivalent to:
$\frac{|HK|}{|K|}=\frac{|H|}{|H \cap K|}$
So now we look at the cosets of $K$ in $HK$ - ie. the elements of $HK/K$.
They are exactly $\frac{|HK|}{|K|}$ because of Lagrange's theorem.
Then we look at the cosets of $H \cap K$ in $H$ - ie. the elements of $H/H \cap K$.
They are exactly $\frac{|H|}{|H \cap K|}$ because of Lagrange's theorem.
So if we could find a bijection from $HK/K$ to $H/H \cap K$, we are done.
So let's look at the elements of $HK/K$, they are cosets of the form: $h_1k_1K$,
but $k_1K=K$, so we get $h_1K$.
Then lets look at the elements of $H/H \cap K$,
they are cosets of the form: $h_1H \cap K$.
So let's define $f: HK/K \to H/H \cap K$, $f(hK)=hH \cap K$.
To see that it's a function we need to show that it's well defined.
Let $h_1K=h_2K$, ie. $h_2^{-1}h_1 \in K$ which also implies  $h_2^{-1}h_1 \in H \cap K$
Then we need to show that $f(h_1K)=f(h_2K)$.
So $f(h_1K)=h_1H \cap K$ and $f(h_2K)=h_2H \cap K$
To prove that $h_1H \cap K = h_2H \cap K$
we need $h_2^{-1}h_1 \in H \cap K$.
But we've already shown that.
Hence f is well defined.
Now we need to show that it's injective.
Suppose $f(h_1K)=f(h_2K)$, but $h1K \neq h2K$.
Ie. $h_1H \cap K = h_2H \cap K$ but $h_1K \neq h_2K$.
$h_1K \neq h_2K$ implies $h_2^{-1}h_1 \notin K$ which implies $h_2^{-1}h_1 \notin H \cap K$.
Hence $h_1H \cap K \neq h_2H \cap K$.
So we know f is injective.
Now to check for surjectivity:
Since $H/H \cap K$ has elements of the form $h_1H \cap K$, for each of them we have,
$f(h_1K)=h_1H \cap K$.
QED
 A: The best and standard way to prove it is to consider the map from $H\times K$ to $HK$ which sends $(h,k)$ to $hk$ and look at the equivalence classes of pairs mapped to the same element of $HK$. That is for every $(h,k)$ count pairs $(h',k')$ such that $hk=h'k'$.
Edit To make it complete, $hk=h'k'$ is equivalent to $h^{-1}h'=k'k^{-1}$. The LHS is in $H$, the RHS is in $K$, so both are in $K\cap H$. So the number of pairs $(h',k')$ such that $hk=h'k'$ is the same as the number of elements in $h(H\cap K)$ which is $|H\cap K|$.
A: The equivalence relation $(h,k)\sim (h',k')\stackrel{(def.)}{\iff} hk=h'k'$ induces a partition of $H\times K$ into equivalence classes each of cardinality $|H\cap K|$, and the quotient set $(H\times K)/\sim$ has cardinality $|HK|$. Therefore, if $H$ and $K$ are finite (in particular if they are subgroups of a finite group), we get: $|H\times K|=|H||K|=|H\cap K| |HK|$, whence the formula in the OP. Hereafter the details.
(The formula holds irrespective of $HK$ being a subgroup.)

Let's define in $H\times K$ the equivalence relation: $(h,k)\sim (h',k')\stackrel{(def.)}{\iff} hk=h'k'$. The equivalence class of $(h,k)$ is given by:
$$[(h,k)]_\sim=\{(h',k')\in H\times K\mid h'k'=hk\} \tag 1$$
Now define the following map from any equivalence class:
\begin{alignat*}{1}
  f_{(h,k)}:[(h,k)]_\sim &\longrightarrow&  H\cap K \\
  (h',k')&\longmapsto& f_{(h,k)}((h',k')):=k'k^{-1} \\
\tag 2
 \end{alignat*}
Note that $k'k^{-1}\in K$ by closure of $K$, and $k'k^{-1}\in H$ because $k'k^{-1}=h'^{-1}h$ (being $(h',k')\in [(h,k)]_\sim$) and by closure of $H$. Therefore, indeed $k'k^{-1}\in H\cap K$.
Lemma 1. $f_{(h,k)}$ is bijective.
Proof.
\begin{alignat}{2}
f_{(h,k)}((h',k'))=f_{(h,k)}((h'',k'')) &\space\space\space\Longrightarrow &&k'k^{-1}=k''k^{-1} \\
&\space\space\space\Longrightarrow &&k'=k'' \\
&\stackrel{h'k'=h''k''}{\Longrightarrow} &&h'=h'' \\
&\space\space\space\Longrightarrow &&(h',k')=(h'',k'') \\
\end{alignat}
and the map is injective. Then, for every $a\in H\cap K$, we  get $ak\in K$ and $a=f_{(h,k)}((h',ak))$, and the map is surjective. $\space\space\Box$
Now define the following map from the quotient set:
\begin{alignat}{1}
  f:(H\times K)/\sim &\longrightarrow&  HK \\
  [(h,k)]_\sim &\longmapsto& f([(h,k)]_\sim):=hk \\
\tag 3
 \end{alignat}
Lemma 2. $f$ is well-defined and bijective.
Proof.

*

*Good definition: $(h',k')\in [(h,k)]_\sim \Rightarrow f([(h',k')]_\sim)=h'k'=hk=f([(h,k)]_\sim)$;

*Injectivity: $f([(h',k')]_\sim)=f([(h,k)]_\sim) \Rightarrow h'k'=hk \Rightarrow (h',k')\in [(h,k)]_\sim \Rightarrow [(h',k')]_\sim=[(h,k)]_\sim$;

*Surjectivity: for every $ab\in HK$ , we get $ab=f([(a,b)]_\sim)$. $\space\space\Box$
Finally, the formula holds irrespective of $HK$ being a subgroup, which was never used in the proof.
A: There is a quite easy way to prove this problem. If you understand chinese, there is a classic proof on Yang Zixu's 'Abstract Algebra'. Here is the proof:
Since $H\cap K\le H$, let $|H|/|H\cap K|=m$ and
$H = h_1(H\cap K)\cup h_2(H\cap K)\cup \cdots \cup h_m(H\cap K),$
here $h_i\in H, h_i^{-1} h_j \notin K,i\neq j.$
Clearly,
$HK=h_1K\cup h_2K\cup\cdots\cup h_m K,$
while
$h_iK\cap h_jK = \varnothing,i\neq j,$
thus
$|HK|=m|K|,$
which means
$|HK|=|H||K|/|H\cap K|.$
QED
It is an application of coset decomposition theory. There is no need of considering the bijection or maps etc.
A: In the case that$H\triangleleft G$, this follows immediately from the second isomorphism theorem.
But, actually your result is well known, and called the product formula.  Neither $H$ nor $K$ is required to be normal.  See "Product of group subsets - Wikipedia" https://en.m.wikipedia.org/wiki/Product_of_group_subsets
