[proofplan]
Fix a left transversal $\mathcal{T}$ of $H$ in $G$, so that $V := \operatorname{Ind}_H^G W = \bigoplus_{t \in \mathcal{T}} t \otimes W$ as vector spaces. The double cosets $\{KgH : g \in \mathcal{S}\}$ partition $G$, hence the transversal $\mathcal{T}$ partitions accordingly into pieces $\mathcal{T}_g := \mathcal{T} \cap KgH$. We show that the subspace $V(g) := \bigoplus_{t \in \mathcal{T}_g} t \otimes W$ is $K$-stable, that $\operatorname{Res}_K^G V = \bigoplus_g V(g)$ as $K$-representations, and that $V(g) \cong \operatorname{Ind}_{H_g}^K W_g$ via the $K$-equivariant map $k \otimes w \mapsto kg \otimes w$ on a transversal of $H_g = gHg^{-1} \cap K$ in $K$. Combining these gives the Mackey decomposition.
[/proofplan]
[step:Set up the induced module $V = \operatorname{Ind}_H^G W$ on a left transversal of $H$ in $G$]
Let $\mathcal{T} \subseteq G$ be a fixed left transversal of $H$ in $G$, i.e., a set of coset representatives so that $G = \bigsqcup_{t \in \mathcal{T}} tH$. By the construction of the induced representation,
\begin{align*}
V := \operatorname{Ind}_H^G W = \bigoplus_{t \in \mathcal{T}} t \otimes W
\end{align*}
as a complex vector space, where $t \otimes W$ denotes the copy of $W$ indexed by $t$. The $G$-action is given as follows: for $x \in G$ and $t \in \mathcal{T}$, write $xt = t' h$ with $t' \in \mathcal{T}$ and $h \in H$ uniquely determined by the coset decomposition. Then
\begin{align*}
x \cdot (t \otimes w) = t' \otimes \rho(h)w.
\end{align*}
We will analyse the restriction of this action to the subgroup $K$.
[/step]
[step:Partition the transversal $\mathcal{T}$ according to the double coset of each representative]
Since $G = \bigsqcup_{g \in \mathcal{S}} KgH$ is a disjoint union of double cosets, every $t \in \mathcal{T}$ lies in a unique double coset $KgH$ for some $g \in \mathcal{S}$. Define
\begin{align*}
\mathcal{T}_g := \mathcal{T} \cap KgH, \qquad V(g) := \bigoplus_{t \in \mathcal{T}_g} t \otimes W.
\end{align*}
Then $\mathcal{T} = \bigsqcup_{g \in \mathcal{S}} \mathcal{T}_g$, and as a vector space,
\begin{align*}
V = \bigoplus_{g \in \mathcal{S}} V(g).
\end{align*}
We now verify that each $V(g)$ is $K$-stable. Let $k \in K$ and $t \in \mathcal{T}_g$, so $t \in KgH$. Then $kt \in KgH$ as well, since $KgH$ is closed under left multiplication by elements of $K$. Writing $kt = t' h$ with $t' \in \mathcal{T}$, $h \in H$, the coset $t'H = ktH \subseteq KgH$ forces $t' \in \mathcal{T} \cap KgH = \mathcal{T}_g$. Hence
\begin{align*}
k \cdot (t \otimes w) = t' \otimes \rho(h)w \in V(g).
\end{align*}
Therefore $V(g)$ is a $K$-subrepresentation of $\operatorname{Res}_K^G V$, and
\begin{align*}
\operatorname{Res}_K^G V = \bigoplus_{g \in \mathcal{S}} V(g)
\end{align*}
as $K$-representations.
[/step]
[step:Choose a transversal of $H_g$ in $K$ to parametrise $\mathcal{T}_g$]
Fix $g \in \mathcal{S}$. We claim the map
\begin{align*}
\Phi_g: K/H_g &\to (KgH)/H, \\
k H_g &\mapsto kgH
\end{align*}
is a well-defined bijection. Recall $H_g = gHg^{-1} \cap K$.
**Well-defined.** Suppose $k_1 H_g = k_2 H_g$, so $k_2 = k_1 z$ for some $z \in H_g = gHg^{-1} \cap K$. Write $z = g h_0 g^{-1}$ with $h_0 \in H$. Then
\begin{align*}
k_2 g = k_1 z g = k_1 g h_0 g^{-1} g = k_1 g h_0,
\end{align*}
so $k_2 g H = k_1 g H$.
**Injective.** Suppose $k_1 g H = k_2 g H$, so $k_2 g = k_1 g h$ for some $h \in H$. Then $k_1^{-1} k_2 = g h g^{-1} \in g H g^{-1}$, and also $k_1^{-1} k_2 \in K$, so $k_1^{-1} k_2 \in g H g^{-1} \cap K = H_g$. Hence $k_1 H_g = k_2 H_g$.
**Surjective.** Every left $H$-coset inside $KgH$ has the form $kgH$ for some $k \in K$ by definition of the double coset $KgH = \{kgh : k \in K, h \in H\}$.
So $\Phi_g$ is a bijection. Choose a left transversal $\mathcal{U}_g \subseteq K$ of $H_g$ in $K$ — i.e., $K = \bigsqcup_{u \in \mathcal{U}_g} u H_g$. Then $\{ugH : u \in \mathcal{U}_g\}$ enumerates without repetition the left $H$-cosets contained in $KgH$. Equivalently, $\mathcal{T}_g = \mathcal{T} \cap KgH$ is in bijection with $\mathcal{U}_g$ via the unique-coset-representative map: for each $u \in \mathcal{U}_g$, there is a unique $t = t(u) \in \mathcal{T}$ with $tH = ugH$, and $u \mapsto t(u)$ is a bijection $\mathcal{U}_g \to \mathcal{T}_g$.
Without loss of generality (by replacing $\mathcal{T}_g$ with $\{ug : u \in \mathcal{U}_g\}$, which is also a transversal of the cosets in $KgH$ since each $ugH$ is a distinct coset and these exhaust the cosets in $KgH$), we may assume $\mathcal{T}_g = \{ug : u \in \mathcal{U}_g\}$. Then
\begin{align*}
V(g) = \bigoplus_{u \in \mathcal{U}_g} (ug) \otimes W.
\end{align*}
[guided]
The structural fact behind this step is that the left $H$-cosets contained in the double coset $KgH$ are in bijection with the left $H_g$-cosets in $K$. This is a standard but essential lemma. Why $H_g$ in particular? Because two elements $k_1 g, k_2 g \in Kg$ lie in the same $H$-coset (i.e., $k_2 g = k_1 g h$) precisely when $k_1^{-1} k_2 = g h g^{-1}$, which lives in $K$ (since both $k_i$ are) and in $g H g^{-1}$ — exactly the intersection that defines $H_g$.
We then choose a transversal $\mathcal{U}_g$ of $H_g$ in $K$ (possible since $H_g \le K$), and the elements $\{ug : u \in \mathcal{U}_g\}$ form a complete set of left $H$-coset representatives for the cosets inside $KgH$. We are free to take $\mathcal{T}_g$ to be this specific set: this is allowed because the induced module $\operatorname{Ind}_H^G W$ does not depend on the choice of transversal (different choices give canonically isomorphic modules). The benefit is concrete: every element of $V(g)$ now has the form $ug \otimes w$ with $u \in \mathcal{U}_g$, which is exactly the form needed to compare with $\operatorname{Ind}_{H_g}^K W_g$.
[/guided]
[/step]
[step:Define the $K$-equivariant isomorphism $\operatorname{Ind}_{H_g}^K W_g \to V(g)$]
Recall that the conjugate representation $(\rho_g, W_g)$ has underlying vector space $W_g = W$ and $H_g$-action
\begin{align*}
\rho_g: H_g &\to \operatorname{GL}(W), \\
z &\mapsto \rho(g^{-1} z g),
\end{align*}
which is well-defined because $z \in H_g \subseteq gHg^{-1}$ implies $g^{-1} z g \in H$. With $\mathcal{U}_g$ as the chosen transversal of $H_g$ in $K$,
\begin{align*}
\operatorname{Ind}_{H_g}^K W_g = \bigoplus_{u \in \mathcal{U}_g} u \otimes W_g.
\end{align*}
Define the linear map
\begin{align*}
\Psi_g: \operatorname{Ind}_{H_g}^K W_g &\to V(g), \\
u \otimes w &\mapsto ug \otimes w \qquad (u \in \mathcal{U}_g, w \in W).
\end{align*}
Since both sides are direct sums indexed by $\mathcal{U}_g$ with $|W|$-dimensional summands, $\Psi_g$ is a vector-space isomorphism.
**Verification of $K$-equivariance.** Fix $x \in K$ and $u \in \mathcal{U}_g$. We must show
\begin{align*}
\Psi_g(x \cdot (u \otimes w)) = x \cdot \Psi_g(u \otimes w).
\end{align*}
*Left-hand side.* In $\operatorname{Ind}_{H_g}^K W_g$, write $xu = u' z$ uniquely with $u' \in \mathcal{U}_g$ and $z \in H_g$. Then
\begin{align*}
x \cdot (u \otimes w) = u' \otimes \rho_g(z) w = u' \otimes \rho(g^{-1} z g) w,
\end{align*}
using the definition of $\rho_g$. Applying $\Psi_g$,
\begin{align*}
\Psi_g(x \cdot (u \otimes w)) = u' g \otimes \rho(g^{-1} z g) w.
\end{align*}
*Right-hand side.* In $V(g)$, the transversal element representing $u$ is $ug \in \mathcal{T}_g$. We compute $x \cdot (ug \otimes w)$ by writing
\begin{align*}
x (ug) = (x u) g = (u' z) g = u' g \cdot (g^{-1} z g).
\end{align*}
Set $h := g^{-1} z g$. Since $z \in H_g \subseteq gHg^{-1}$, we have $h \in H$. So $x(ug) = (u'g) h$ with $u'g \in \mathcal{T}_g$ and $h \in H$ — this is the unique decomposition since $\mathcal{T}_g$ is a transversal of $H$-cosets in $KgH$. Therefore
\begin{align*}
x \cdot (ug \otimes w) = u'g \otimes \rho(h) w = u'g \otimes \rho(g^{-1} z g) w.
\end{align*}
The two expressions agree. Hence $\Psi_g$ is a $K$-equivariant isomorphism:
\begin{align*}
\operatorname{Ind}_{H_g}^K W_g \cong V(g).
\end{align*}
[guided]
The map $\Psi_g(u \otimes w) = ug \otimes w$ is forced by the parametrisation we set up in Step 3: elements of $V(g)$ have the canonical form $ug \otimes w$, and the natural way to match these with the basis $\{u \otimes w\}$ of $\operatorname{Ind}_{H_g}^K W_g$ is to right-multiply by $g$.
The non-trivial verification is $K$-equivariance. The conjugate action $\rho_g(z) = \rho(g^{-1} z g)$ on the source side must match the action on $V(g)$ inherited from $\operatorname{Ind}_H^G W$. The matching happens via the calculation $x(ug) = (u' z) g = (u'g)(g^{-1} z g)$: the element $z \in H_g$ "becomes" the element $g^{-1} z g \in H$ when we slide $g$ past $z$. This is precisely the conjugation that defines $\rho_g$ — so the two actions agree by construction.
What would fail without the hypothesis that $\mathcal{U}_g$ is a transversal of $H_g$ in $K$? The expression $xu = u' z$ might not have a unique $u' \in \mathcal{U}_g$ with $z \in H_g$. We need exactly one such decomposition for the action to be well-defined.
[/guided]
[/step]
[step:Combine the pieces to obtain the Mackey decomposition]
From Step 2,
\begin{align*}
\operatorname{Res}_K^G V = \bigoplus_{g \in \mathcal{S}} V(g)
\end{align*}
as $K$-representations. From Step 4, $V(g) \cong \operatorname{Ind}_{H_g}^K W_g$ as $K$-representations for each $g \in \mathcal{S}$. Substituting,
\begin{align*}
\operatorname{Res}_K^G \operatorname{Ind}_H^G W \cong \bigoplus_{g \in \mathcal{S}} \operatorname{Ind}_{H_g}^K W_g,
\end{align*}
which is the Mackey restriction formula.
[/step]
