Why is $|HK| = \frac{|H||K|}{|H \cap K|}$?

Question

Let $G$ be a finite group, and $H$,$K$ be subgroups. Then we can form the set $$HK = \{hk: h \in H, k \in K\}$$ It is well known that $HK$ is a subgroup of $G$ if and only if $HK=KH$. If $H \cap K = \{e\}$, then we clearly have $|HK| = |H||K|$ (indeed, the group multiplication $H \times K \to HK$ is a bijection). On the other extreme, if $H \subset K$ then $|HK| = |K|$. In general we have the formula $$|HK| = \frac{|H||K|}{|H \cap K|}$$ which quantifies the idea that we "$HK$ collapses in proportion to how many elements $H,K$ share". I'm trying to get a bit more intuition for this fact.
I've seen an argument by which we establish a bijection between the sets of cosets $HK/K$ and $H/(H\cap K)$, but it wasn't "manual" enough for me (that is to say, I'm willing to believe that it's an enlightening proof, to someone who is more savvy with cosets).

One idea for an argument I had was counting: if we seek to prove $|HK||H \cap K| = |H||K|$ then it's attractive to try to show that every distinct element of $HK$ obtained by writing $g = hk$ is multiply counted $|H \cap K|$ times. Indeed, suppose that $h_{1}k_{1} = h_{2}k_{2}$. Then we obtain the element $h_{1}^{-1}h_{2} = k_{1}k_{2}^{-1} \in H \cap K$. Then I get a bit stuck, because I want to show the duplicate elements biject with $H \cap K$ but I can't tell how. Of course, it might not be possible, but my intuition says maybe.

Any of the following would constitute a helpful answer (and be greatly appreciated!):

1. A bit of exposition into why the coset-based argument is an intuitive one to make (especially without knowing the answer in advance)
2. Some help finishing off the argument I've tried to start
3. A oonvincing reason the argument I've started is hopeless

Answer 1

This is a way to formalize the argument given in "Order of a product of subgroups". Let $f: H \times K \rightarrow HK$ be multiplication. Now since $f$ is surjective, $|HK|$ is the number of fibres of $f$. Now, a more formal way to say 'one product in $HK$ can be written in exactly $|H \cap K|$ ways' is 'every fibre of $f$ has $|H \cap K|$ elements'. This is true because if $h_0 \in H$ and $k_0 \in K$ are fixed then $$f^{-1}(\{h_0k_0\})=\{(h, k) \in H \times K \ : \ hk=h_0k_0 \ \}=\{(h_0t, t^{-1}k_0) \ : \ t \in H \cap K \ \},$$ the latter being of cardinality $H \cap K$. The argument to prove the equality above is given in "Order of a product of subgroups", albeit in other language. Now we have, since we found all fibres have the same cardinality, $$|H \times K |= \text{number of fibres} \times \text{number of elements in one fibre}= |HK| \times |H \cap K|.$$

Answer 2

Suppose $G$ is abelian. We can have a simple explanation in this case: consider the sequence of groups and homomorphisms: \begin{alignat}5 1\longrightarrow H\cap K&\longrightarrow& H\times K&\longrightarrow HK\longrightarrow 1\\ h&\longmapsto& (x,x)&\\ &&(h,k)&\longmapsto hk^{-1} \end{alignat} This is an exact sequence of groups, so that $$|\mkern1mu H\times K\mkern1mu|=|\mkern1muH\cap K\mkern1mu|\cdot|\mkern1muHK\mkern1mu|.$$

If $G$ is not abelian, the map $H\times K\longrightarrow HK$ is no more a homomorphism, but it remains a surjection. Furthermore $(h,k)$ and $(h',k')$ map onto the same element of $HK$ if and only if there exists an element $\ell\in H\cap K$ such that $h'=h\ell$ and $k'=k\ell$. Thus for each element in $HK$, its inverse image in $H\times K$ is in bijection with $H\cap K$, and we can apply the Shepherds' principle.