This argument is, in spirit, closely related to the Third (or Second, depending how you number them) Isomorphism Theorem.
Theorem. $(H:H\cap K)\leq (G:K)$, in the sense of cardinality, with equality if $G=HK$. In the case where $(G:K)$ is finite, equality holds if and only if $HK=G$.
Proof. I claim that $h_1(H\cap K) = h_2(H\cap K)$ if and only if $h_1K = h_2K$. Indeed:
$$\begin{align*}
h_1K = h_2K &\iff h_2^{-1}h_1\in K\\
&\iff h_2^{-1}h_1\in H\cap K\\
&\iff h_1(H\cap K) = h_2(H\cap K).
\end{align*}$$
Thus, the map from $\{h(H\cap K)\mid h\in H\}$ to $\{gK\mid g\in G\}$ given by sending $h(H\cap K)$ to $hK$ is both well-defined and one-to-one. Thus, $(H:H\cap K)\leq (G:K)$ (in the sense of cardinality).
If $HK=G$, then every element of $\{gK\mid g\in G\}$ can be written as $hkK=hK$ for some $h\in H$, and thus the map above is a bijection, yielding equality. If $(G:K)$ is finite and we have equality, the injection above must be a bijection, and so every coset $gK$ is of the form $hK$ for some $h\in H$. Thus, given $g\in G$, there exists $h\in H$ and $k\in K$ such that $g=hk\in hK$, hence $G\subseteq HK$, which implies the equality. $\Box$
Corollary. $(G:H\cap K)\leq (G:H)(G:K)$ in the sense of cardinality.
Proof. $(G:H\cap K)= (G:H)(H:H\cap K) \leq (G:H)(G:K)$, in the sense or cardinality. $\Box$
Corollary. If $H$ and $K$ have finite index in $G$, then $H\cap K$ has finite index in $G$, and moreover $(G:H\cap K)\leq (G:H)(G:K)$, with equality if and only if $G=HK$.
Proof. The inequality was already proven. We get equality if and only if $(H:H\cap K)=(G:K)$, which holds in this situation if and only if $G=HK$. $\Box$
Why do I say it is related in spirit to the Third Isomorphism Theorem? That's the one that says that if $K$ is normal, then $HK/K$ is isomorphic to $H/H\cap K$. The bijection between these two is precisely the one that sends $h(H\cap K)$ to $hK$. If we knew $HK$ is a subgroup, we could show that $(HK:K)=(H:H\cap K)$, and then use that $HK\leq G$ to get $(H:H\cap K)\leq (G:K)$.
Best Answer
Consider the family $\{g_1 H,\ldots, g_m H\}$ of all cosets of $G/H$, and the family $\{h_1 K,\ldots, h_n K\}$ of all cosets of $H/K$. What he observes is that each $g_i H$ contains all the cosets $g_i(h_j K)$. In particular, if $i\neq j$, then the families $\{g_i(h_1 K),\ldots, g_i(h_n K)\}$ and $\{g_j(h_1 K),\ldots, g_j(h_n K)\}$ are disjoint. Each of these families have $[H: K]$ elements and we have in total $[G: H]$ such families. So the union of these families has $[G: H][H: K]$ elements.
Finally, it's clear that the union of all these families is precisely $G/K$, so it has in total $[G: K]$ elements and we obtain the desired relation.