If $K \leq H \leq G$, show that $[G:K] = [G:H][H:K]$.

We'll show that there exists a bijection between $(H\backslash G)\times(K\backslash H)$ and $K\backslash G$. Let $(a_i)_{i\in I}$ be a collection of representatives for the elements of $H\backslash G$ and $(b_j)_{j\in J}$ a collection of representatives for the elements of $K\backslash H$. Define $\phi:(H\backslash G)\times(K\backslash H)\to K\backslash G$ by $$ \phi(Ha_i,Kb_j)=Kb_ja_i. $$ Let $Kc\in K\backslash G$. Then $Kc\subset Ha_i$ for some unique $a_i$ since $K\leq H$, so $c=ha_i$ for some (also clearly unique given an $a_i$) $h\in H$. We also have that $Kh=Kb_j$ for some unique $b_j$, so $Kc=Kb_ja_i=\phi(Ha_i,Kb_j)$, and this choice of $(Ha_i,Kb_j)$ is unique for a given $Kc$. Hence, $\phi$ is a bijection and $$ [G:K]=[G:H][H:K]. $$ This proof formalizes Aaron's comment about breaking each coset up into finer cosets.

Definition. Let $G$ is a group and $H\le G$. The set $\{x_i\}_{i\in I}\subseteq G$ is called a left oblique set, if all of the left cosets $x_iH$ are distinct and $G=\bigcup_{i\in I}x_iH$.

Suppose $\{x_i\}_{i\in I}$ is a left oblique set of $K$ in $H$ and $\{y_j\}_{j\in J}$ is a left oblique set of $H$ in $G$. So we have $H=\bigcup_{i\in I}x_iK$ and $G=\bigcup_{j\in J}y_jH$ which implies that $$G=\bigcup_{j\in J}y_jH=\bigcup_{j\in J}y_j\left(\bigcup_{i\in I}x_iK\right)=\bigcup_{j\in J,i\in I}y_jx_iK$$ Therefore $\left\{y_jx_iK\right\}_{i\in I,j\in J}$ is a partition of $G$ to the set of all the left cosets of $K$ in $G$. Now I prove these cosets are distinct. If $y_jx_iK=y_rx_sK$, then $\color{red}{y_jx_i=y_rx_sk}$ for any $k\in K$. Since $K\subseteq H$ so that $k\in H$ and also since $x_i,x_s \in H$, we have $y_r^{-1}y_j=x_skx_i^{-1}\in H$. Now by definition of left oblique set we must have $r=j$ which implies that $\color{red}{x_i=x_sk}$. This implies that $x_s^{-1}x_i\in K$ and once again by definition we have $s=i$. Hence all of $y_jx_i$'s are distinct.

The canonical map $\pi:G\to G/H$ induces a surjection $\overline\pi:G/K\to G/H$; its fiber is given by $$\overline\pi^{-1}(aH)=a\cdot (H/K).$$Since the map $H/K\to a\cdot (H/K), \ hK\mapsto ahK$ is bijective, we conclude that each fiber of $\overline \pi$ has the same cardinality as $H/K$. The claim follows.