If H and K are subgroups of a group G, then $[H:H\cap K]\leq [G:K]$. If $[G:K]$ is finite, then $[H:H\cap K]=[G:K]$ if and only if $G=KH$.
My attempt: Let $C=H\cap K$ and $\{Ca\mid a\in H\}=\{Ca_i\mid i\in I\}$, where $I$ is indexing set. Then $[H:H\cap K]=|I|$. We claim $\{Ka_i\mid i\in I\}$ are pairwise disjoint, that is $Ka_i\cap Ka_j=\emptyset$ if $i\neq j$. Assume towards contradiction, $Ka_i\cap Ka_j\neq \emptyset$. Since two equivalence class are either disjoint or equal, we have $Ka_i= Ka_j$. It’s easy to check, $(H\cap K)a=Ha\cap Ka$ and $Ha=H$, for all $a\in H$. So $$\begin{align} Ca_i\cap Ca_j &= [(H\cap K)a_i]\cap [(H\cap K)a_j]\\ &= (Ha_i\cap Ka_i)\cap (Ha_j\cap Ka_j)\\ &=H\cap Ka_i\cap H\cap Ka_j\\ &=H\cap Ka_i\\ &=(H\cap K)a_i\\ &=\emptyset. \end{align}$$ But $a_i=ea_i\in (H\cap K)a_i$. Thus we reach contradiction. Hence $Ka_i\cap Ka_j=\emptyset$ if $i\neq j$. So $|\{Ka_i\mid i\in I\}|=|I|$. Since $\{Ka_i\mid i\in I\}\subseteq \{Kb\mid b\in G\}$, we have $|I|\leq [G:K]$. That is $[H:H\cap K]\leq [G:K]$.
Suppose $[G:K]=n\in \Bbb{N}$. $(\Rightarrow)$ Let $[H:H\cap K]=[G:K]=n$. Then $H=\bigcup_{i\in J_n}Ca_i$ such that $a_i\in H$ and $Ca_i\cap Ca_j=\emptyset$ if $i\neq j$. So $KH=K(\bigcup_{i\in J_n}Ca_i)$. By theorem 7 section 1.4, $K(\bigcup_{i\in J_n}Ca_i)=\bigcup_{i\in J_n}KCa_i$ and $KC=K$. So $KH=\bigcup_{i\in J_n}Ka_i$. By above claim, $Ka_1,…,Ka_n$ are distinct. Since $[G:K]=n$, we have $\{Kb\mid b\in G\}= \{Ka_1,…,Ka_n\}$. So $G=\bigcup_{i\in J_n}Ka_i$. Thus $KH= \bigcup_{i\in J_n}Ka_i=G$. Hence $G=KH$.
$(\Leftarrow)$ Let $G=KH$. Assume towards contradiction, $[H:H\cap K]\lt [G:K]$. Then $H=\bigcup_{i\in J_m}Ca_i$ such that $m\lt n$, $a_i\in H$ and $Ca_i\cap Ca_j=\emptyset$ if $i\neq j$. So $$G=KH=K(\bigcup_{i\in J_m}Ca_i)=\bigcup_{i\in J_m}KCa_i=\bigcup_{i\in J_m}Ka_i.$$ which contradicts our initial hypothesis of $[G:K]=n$. Hence $[H:H\cap K]=[G:K]$. Is my proof correct?
Hungerford’s proof: Let $A$ be the set of all right cosets of $H\cap K$ in $H$ and $B$ the set of all right cosets of $K$ in G. The map $\varphi : A\to B$ given by $(H\cap K)h\mapsto Kh$ ($h\in H$) is well defined since $(H\cap K)h'=(H\cap K)h$ implies $h'h^{-1}\in H \cap K\subseteq K$ and hence $Kh' = Kh$. Show that $\varphi$ is injective. Then $[H: H\cap K]=|A|\leq |B|= [G:K]$. If $[G:K]$ is finite, then show that $[H:H\cap K]= [G:K]$ if and only if $\varphi$ is surjective and that $\varphi$ is surjective if and only if $G = KH$. Note that for $h\in H$, $k\in K$, $Kkh= Kh$ since $(kh)h^{-1}=k\in K$.
Filling details: $(1)$ Suppose $\varphi [(H\cap K)h’]=\varphi [(H\cap K)h]=Kh’=Kh$, for some $h’,h\in H$. Then $h’h^{-1}\in K$. So $h’h^{-1}\in H\cap K$ and $(H\cap K)h’= (H\cap K)h$. Thus $\varphi$ is injective.
$(2)$ If $\varphi$ is injective and $|A|=|B|\in \Bbb{N}$, then $\varphi$ is surjective. If $\varphi$ is injective and surjective, then $\varphi$ is bijective. So $|A|=|B|$.
$(3)$ Suppose $\varphi$ is surjective. Since $[G:K]=n\in \Bbb{N}$, we have $G=\bigcup_{i\in J_n}Kg_i$ such that $g_i\in G$ and $Kg_i\cap Kg_j=\emptyset$ if $i\neq j$. Let $g\in G$. Then $g\in Kg_j$, for some $j\in J_n$. Since $\varphi$ is surjective, we have $\exists h\in H$ such that $\varphi [(H\cap K)h]=Kg_j=Kh$. So $g\in Kh\subseteq KH$. Thus $G\subseteq KH$. Trivially $G\supseteq KH$. Hence $G=KH$. Conversely, suppose $G=KH$. Let $Kg\in B$, for some $g\in G$. Then $\exists k\in K$, $\exists h\in H$ such that $g=kh$. So $Kg=Kkh=Kh$. Thus $\exists h\in H$ such that $\varphi [(H\cap K)h]=Kh=Kg$. Hence $\varphi$ is surjective.
Your proof is correct, though if one wants to pedantic we should take a moment to verify that the following:
Is really true. This is easy since we have $n$ distinct cosets of $K$ on the RHS and on the LHS there are exactly $n$ cosets in total so there must be equality, the injection $\{a_1,\cdots,a_n\}\to G/K$ must surject.
I would also rewrite things in this order: $$\begin{align}\emptyset&=Ca_i\cap Ca_j\\&= [(H\cap K)a_i]\cap [(H\cap K)a_j]\\ &= (Ha_i\cap Ka_i)\cap (Ha_j\cap Ka_j)\\ &=H\cap Ka_i\cap H\cap Ka_j\\ &=H\cap Ka_i\\ &=(H\cap K)a_i\end{align}$$Or go further to write it like that but from bottom $\to$ top, since you are trying to show $(H\cap K)a_i$ is empty and that follows from the fact that $Ca_i\cap Ca_j$ is empty; in your version we have $Ca_i\cap Ca_j=\cdots=(H\cap K)a_i=\emptyset$ and in the usual mental parsing of expressions the logical order has been subverted. But, that is subjective and it is extremely pedantic of me to mention it ; )
Your verification of the details in Hungerford's proof is also correct.