Lemma used to prove $\left|HK\right|=\frac{\left|H\right|\left|K\right|}{\left|H \cap K\right|}$ Given a group $G$ and $H,K \le G$,then :
$$\left|HK\right|=\frac{\left|H\right|\left|K\right|}{\left|H \cap K\right|}$$
Where $HK:=\left\{hk:h \in H ,k \in K\right\}$

Lemma:
For $h_1,h_2 \in H$
$$hK=h'K \iff h(H \cap K)=h'(H \cap K)$$
We have:
$$HK=\bigcup_{h \in H}hK$$
Not every such left cosets of $K$ in $H$ are distinct, on the other hand the function $\phi:hK \to K$ with $hk \mapsto k$ is a bijection, so the number of elements in $hK$ is the same as that $K$'s  I showed that the set of left cosets (equivalently right cosets) partitions the group.
By this we see that :$$\left|HK\right|=\left|\color{blue}{\text{the set consiting of all distinct left cosets }}hK\right|\left|K\right|$$
One concludes from the lemma that the number of such distinct left cosets is the same as $\left|H: H \cap K\right|$ but I don't know how such a conclusion is possible, how the lemma helps us?
It looks that $hK \ne h^{'} K$ iff $h(H \cap K) \ne h^{'}(H \cap K)$ and the order of the set of all such distinct $h(H \cap K)$ for $h \in H$  is $\left|H: H \cap K\right|$...
Also, it would be appreciated if someone gives me an example where such left cosets $hk$ are identical.
 A: Consider the map $\varphi: H/H\cap K\longrightarrow HK/K$ by $h(H\cap K)\mapsto hK$.

*

*This is a well defined map by your lemma $\impliedby$.


*This map is injective by your lemma $\implies$.


*This map is surjective by definition of $HK$.
Therefore this is a natural one-to-one correspondence between these cosets, and the Product Formula follows immediately.
I happen to have written about this yesterday, so here's a link for you https://ml868.user.srcf.net/ExpositoryWritings/Groups3.pdf. There are a few typos I haven't fixed but I hope it is readable and somewhat inspiring.
A: You noted that in the union $\bigcup_{h \in H} hK$, some cosets appear more than once. If you are able to show that each distinct coset appears $|H \cap K|$ times in the union, then you can arrive at the desired conclusion.
The lemma implies that the only way $hK=h'K$ can happen (for $h,h' \in H$) is if $h' = gh$ for some $g \in H \cap K$. In particular, for a given coset $hK$, it appears in the union $|H \cap K|$ times as $(gh)K$ for each $g \in H \cap K$.
A: For simplicity:
$$I=\{hK|h\in H\}$$
$$J=\{h(H\cap K)|h\in H\}$$
Notice that:
$$|J|=|H:(H\cap K)|$$
And we have simply to prove that $|I|=|J|$
Thanks to the lemma the application:
$$\omega: I \to  J $$
$$\ \ \ \ \  \ \      \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  \ \ \ hK \mapsto h(H\cap K)$$
Is a bijection, in fact firstly the application is well defined since:
$$hK=h'K \Rightarrow^{\text{Lemma}} h(H\cap K)=h'(H\cap K)\Rightarrow \omega(hK)=\omega(h'K)$$
The application is also injective:
$$\omega(hK)=\omega(h'K)\Rightarrow  h(H\cap K)=h'(H\cap K)\Rightarrow^{\text{Lemma}} hK=h'K $$
And it's clearly surjective because for every $h(H\cap K)\in J, \omega (hK)=h(H\cap K)$
It follows $|I|=|J|$.
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, $|H\times K|=|H||K|=|H\cap K| |HK|$, whence (if $H$ and $K$ are finite, in particular if they are subgroups of a finite group) the formula in the OP. Hereafter the details.
(Note that 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.
