Showing that $\lvert H K\rvert = \frac{| H\| K|}{ |H\cap K|}$
$H\times K$ acts on $G$ (on the right) via $g\cdot(h,k)=h^{-1}gk$. Then $HK$ is the orbit of the identity element $e$, and so its size is $|H\times K|/|S_e|$ where $S_e$ is the stabiliser of $e$. Then $S_e=\{(h,h):k\in H\cap K\}$.
This method can also count the general double coset $HxK$.
Lemma: $\color{blue}{ H\times K/\mathcal R}$ has $n$ elements that is, $\color{blue}{n= |H\times K/\mathcal R| }$ and we have, $$ \color{blue}{|HK|= |H\times K/\mathcal R| =\frac{|H\|K|}{|H\cap K|}} $$ This is a consequence of $E_1$ and $E_2$ see below for all the details.
Consider the map \begin{split} \phi :&& H\times K\to HK\\ && (h,k)\mapsto hk \end{split} Clearly, $\phi $ is onto (surjective ). Now we consider the relation,
$$\color{red}{(h,k)\mathcal R(h',k')\Longleftrightarrow hk=h'k'\Longleftrightarrow \phi(h,k)=\phi(h',k')}$$ It is easy to check that $\mathcal R$ is an equivalent relation on $H\times K$.
Fact.I. Let denote by $[h,k]_\mathcal R$ the class of an element $(h,k) \in H\times K.$
Let $n\in \mathbb N$ be the number of classes of $ H\times K$ with respect to $\mathcal R.$ Also we denote by $\color{blue}{ H\times K/\mathcal R}$ the set of class. Precisely we have, $$\color{blue}{ H\times K/\mathcal R= \{[h_1,k_1]_\mathcal R, [h_2,k_2]_\mathcal R\cdots, [h_n,k_n]_\mathcal R\}} $$ Where, $(h_j,k_j)_j$ is a set of representative class of $H\times K/\mathcal R $.
First Equality: We consider the $\overline{\phi}$ the quotient map of $\phi$ w.r.t $\mathcal R.$ defines as follows:
\begin{split} \overline{\phi} :&& H\times K/\mathcal R \to HK\\ && [h,k]_\mathcal R \mapsto \phi(h,k) = hk \end{split}
- $\overline{\phi} $ is well define since from the red line above we have,
$$\color{red}{(h',k') \in [h,k]_\mathcal R\Longleftrightarrow (h,k)\mathcal R(h',k')\\\Longleftrightarrow hk=h'k'\Longleftrightarrow \overline{\phi}([h,k]_\mathcal R)=\overline{\phi}([h',k']_\mathcal R)}\tag{Eq}.$$ - It is also easy to check that $\overline{\phi}$ is one-to-one(injective) and Hence bijective since $\phi$ is onto. $$\color{red}{[h',k']_\mathcal R = [h,k]_\mathcal R\Longleftrightarrow (h',k') \in [h,k]_\mathcal R \Longleftrightarrow \overline{\phi}([h,k]_\mathcal R)=\overline{\phi}([h',k']_\mathcal R)}$$
conclusion $\overline{\phi}$ is a bijection and therfore, $$\color{blue}{n=|H\times K/\mathcal R| = |HK|}\tag{$E_1$} $$
we are jumping to the second equality, starting from the following observation.
Fact. II Since $\mathcal R$ is an equivalent relation, we know that $\color{red}{([h_j,k_j]_\mathcal R)_{1\le j\le n}}$ is a partition of $H\times K$ that is, $$\color{red}{ |H\times K| = \sum_{j=1}^{n} |[h_j,k_j]_\mathcal R| }$$ Claim:(see the proof Below) $$\color{red}{|[h_j,k_j]_\mathcal R| = |H\cap K|}$$
Second Equality: Since for any finte sets A and B we have $|A\times B| =|A|\times|B|,$ using the claim and the foregoing relations, we get that $$\color{blue}{|H|\times|K| = |H\times K| = \sum_{j=1}^{n} |[h_j,k_j]_\mathcal R| = \sum_{j=1}^{n} |H\cap K| =|H\times K/\mathcal R||H\cap K|}$$
Then $$ \color{blue}{n= |H\times K/\mathcal R| =\frac{|H\|K|}{|H\cap K|}}\tag{$E_2$} $$
Proof of the claim: Now we would like to investigate $|[h,k]_\mathcal R|$.
$$\color{blue}{(h',k')\in [h,k]_\mathcal R \Longleftrightarrow hk=h'k'\Longleftrightarrow h'^{-1}h=k'k^{-1}\in H\cap K .}$$
Consider the map \begin{split} f :&& [h,k]_\mathcal R \to H\cap K\\ && (h',k')\mapsto h'^{-1}h=k'k^{-1} \end{split} The above relation shows that $f$ is well defined as a map. We will show that $f$ is a bijective map to conclude.
- $f$ is onto(surjective): Let $s\in H\cap K $. If we let $ k' = h s^{-1}~~~\text{and}~~~ k'=sk$ then $\color{red}{h'k' = hs^{-1} sk =hk\Longleftrightarrow (h',k')\mathcal R (h,k) \implies (h',k') \in [h,k]_\mathcal R}$ and hence $$\color{red}{f(h',k')= f(hs^{-1}, sk)} = s.$$
this prove that $f$ is onto.
- $f$ is one-to-one(injective): let, $(a,b), (x,y)\in [h,k]_\mathcal R $ such that $f(a,b)=f(x,y)$. We have $f(a,b) =a^{-1}h =bk^{-1} ~~~~\text{and}~~~f(x,y) =x^{-1}h =yk^{-1}$
then, \begin{split} f(a,b)=f(x,y)&\implies& \color{blue}{a^{-1}h =bk^{-1}} =\color{red}{x^{-1}h =yk^{-1}}\\ &\implies& \color{blue}{a^{-1}h =x^{-1}h} ~~~~\text{and}~~~~\color{red}{ bk^{-1}=yk^{-1}}\\ &\implies& \color{red}{a =x} ~~~~\text{and}~~~~\color{red}{ b=y}\\ \end{split}
This proves that $f$ is bijective,s then the claim follows