Does $G\times K\cong H\times K$ imply $G\cong H$?

Vipul Naik found an elementary proof:

For any finite groups $L$ and $G$, let $h(L,G)$ denote the number of homomorphisms from $L$ to $G$ and $i(L,G)$ denote the number of monomorphisms from $L$ to $G$. Notice that $$h(L,G)= \sum\limits_{N \lhd L} i(L/N,G) \hspace{1cm} (1)$$

Let $G,H,K$ be three finite groups such that $G \times H \simeq G \times K$. Then \begin{gather}h(L,G \times H)=h(L,G \times K) \\ h(L,G)h(L,H)=h(L,G)h(L,K) \\ h(L,H)=h(L,K)\end{gather} for any finite group $L$, since $h(L,G) \neq 0$. Using $(1)$, it is easy to deduce that $i(L,H)=i(L,K)$ for any finite group $L$ by induction on the cardinality of $L$. Hence $$i(H,K)=i(H,H) \neq 0.$$

Therefore, there exists a monomorphism from $H$ to $K$. Since $H$ and $K$ have the same cardinality, we deduce that $H$ and $K$ are in fact isomorphic.

Yes. In fact you only need to assume that $K$ is finite; that is, finite groups are cancellable. This is a theorem due to Hirshon.