[proofplan] The strategy is to compute $\langle \operatorname{Res}^G_H \pi_{\mathrm{reg}}, \psi \rangle_H$ in two ways, where $\pi_{\mathrm{reg}}$ is the regular character of $G$. On one hand, the restriction of $\pi_{\mathrm{reg}}$ to $H$ vanishes off the identity (since $\pi_{\mathrm{reg}}(g) = 0$ for $g \neq 1$ and $\pi_{\mathrm{reg}}(1) = |G|$), reducing the inner product to a single term equal to $\frac{|G|}{|H|}\psi(1) > 0$. On the other hand, decomposing $\pi_{\mathrm{reg}} = \sum_i (\deg \chi_i)\chi_i$ over the irreducibles of $G$ and using linearity of restriction, the inner product expands as $\sum_i (\deg \chi_i)\langle \operatorname{Res}^G_H \chi_i, \psi \rangle_H$. Since the total is nonzero, at least one summand is nonzero, giving an irreducible $\chi_i$ of $G$ with $\psi$ as a constituent of $\operatorname{Res}^G_H \chi_i$. [/proofplan] [step:Recall the regular character and its decomposition into irreducibles of $G$] The regular representation of $G$ is the action of $G$ on the group algebra $\mathbb{C}[G]$ by left multiplication. Its character $\pi_{\mathrm{reg}}: G \to \mathbb{C}$ is computed as follows: for $g \in G$, the map $L_g: \mathbb{C}[G] \to \mathbb{C}[G]$, $h \mapsto gh$ permutes the basis $\{h : h \in G\}$ of $\mathbb{C}[G]$, and its trace counts the basis vectors fixed by $L_g$, i.e., the $h \in G$ with $gh = h$. For $g = 1$, every basis vector is fixed: $\pi_{\mathrm{reg}}(1) = |G|$. For $g \neq 1$, no basis vector is fixed (left multiplication by $g \neq 1$ sends each $h$ to $gh \neq h$): $\pi_{\mathrm{reg}}(g) = 0$. So \begin{align*} \pi_{\mathrm{reg}}(g) = \begin{cases} |G| & \text{if } g = 1, \\ 0 & \text{if } g \neq 1. \end{cases} \end{align*} The decomposition of the regular character into irreducibles is the classical formula \begin{align*} \pi_{\mathrm{reg}} = \sum_{i=1}^{k} (\deg \chi_i)\, \chi_i, \end{align*} where $\chi_1, \ldots, \chi_k$ are the irreducible characters of $G$ and $\deg \chi_i := \chi_i(1)$. (This follows from [Multiplicity Formula](/theorems/2420): the multiplicity of $\chi_i$ in $\pi_{\mathrm{reg}}$ is $\langle \pi_{\mathrm{reg}}, \chi_i \rangle_G = \frac{1}{|G|} \cdot |G| \cdot \overline{\chi_i(1)} = \chi_i(1) = \deg \chi_i$, using $\pi_{\mathrm{reg}}(g) = 0$ for $g \neq 1$ and that irreducible characters take real values at $1$.) [/step] [step:Compute $\langle \operatorname{Res}^G_H \pi_{\mathrm{reg}}, \psi \rangle_H = \frac{|G|}{|H|}\psi(1)$ from the support of $\pi_{\mathrm{reg}}$] The restriction $\operatorname{Res}^G_H \pi_{\mathrm{reg}}: H \to \mathbb{C}$ is the function $\pi_{\mathrm{reg}}\big|_H$, that is, \begin{align*} (\operatorname{Res}^G_H \pi_{\mathrm{reg}})(h) = \begin{cases} |G| & \text{if } h = 1, \\ 0 & \text{if } h \in H \setminus \{1\}. \end{cases} \end{align*} The $H$-inner product is \begin{align*} \langle \operatorname{Res}^G_H \pi_{\mathrm{reg}}, \psi \rangle_H = \frac{1}{|H|} \sum_{h \in H} (\operatorname{Res}^G_H \pi_{\mathrm{reg}})(h)\, \overline{\psi(h)}. \end{align*} All terms with $h \neq 1$ vanish, leaving the single term at $h = 1$: \begin{align*} \langle \operatorname{Res}^G_H \pi_{\mathrm{reg}}, \psi \rangle_H = \frac{1}{|H|} \cdot |G| \cdot \overline{\psi(1)} = \frac{|G|}{|H|}\, \psi(1). \end{align*} The last equality uses $\psi(1) = \dim W \in \mathbb{N}$, which is real, so $\overline{\psi(1)} = \psi(1)$. By hypothesis $\psi$ is a nonzero irreducible character of $H$, so $\psi(1) = \dim W \geq 1$. Hence \begin{align*} \langle \operatorname{Res}^G_H \pi_{\mathrm{reg}}, \psi \rangle_H = \frac{|G|}{|H|}\, \psi(1) > 0. \end{align*} [/step] [step:Expand the same inner product via the decomposition $\pi_{\mathrm{reg}} = \sum_i (\deg \chi_i) \chi_i$] Restriction $\operatorname{Res}^G_H: \mathcal{C}(G) \to \mathcal{C}(H)$ is $\mathbb{C}$-linear, since it is just the linear map $f \mapsto f\big|_H$. The $H$-inner product is sesquilinear, hence linear in the first argument. Combining, \begin{align*} \langle \operatorname{Res}^G_H \pi_{\mathrm{reg}}, \psi \rangle_H &= \biggl\langle \operatorname{Res}^G_H \biggl(\sum_{i=1}^{k} (\deg \chi_i)\, \chi_i\biggr), \psi \biggr\rangle_H \\ &= \biggl\langle \sum_{i=1}^{k} (\deg \chi_i)\, \operatorname{Res}^G_H \chi_i, \psi \biggr\rangle_H \\ &= \sum_{i=1}^{k} (\deg \chi_i)\, \langle \operatorname{Res}^G_H \chi_i, \psi \rangle_H. \end{align*} The first equality uses the decomposition from Step 1. The second uses linearity of restriction. The third uses linearity of the inner product in the first argument (the coefficients $\deg \chi_i$ are real, so no conjugation is needed). [/step] [step:Combine the two computations to extract a nonzero summand] From Steps 2 and 3, \begin{align*} \sum_{i=1}^{k} (\deg \chi_i)\, \langle \operatorname{Res}^G_H \chi_i, \psi \rangle_H = \frac{|G|}{|H|}\, \psi(1) > 0. \end{align*} The left-hand side is a sum of finitely many terms whose total is strictly positive. Therefore at least one summand $(\deg \chi_i)\, \langle \operatorname{Res}^G_H \chi_i, \psi \rangle_H$ is nonzero. Since $\deg \chi_i = \chi_i(1) \geq 1$ for every irreducible character of $G$, the factor $\deg \chi_i$ never vanishes, so the inner product itself is nonzero: \begin{align*} \langle \operatorname{Res}^G_H \chi_i, \psi \rangle_H \neq 0 \quad \text{for at least one } i. \end{align*} Setting $\chi := \chi_i$ for such an $i$, we have an irreducible character $\chi$ of $G$ with $\psi$ as a constituent of $\operatorname{Res}^G_H \chi$. This completes the proof. [guided] The argument is a two-way computation of the same quantity, $\langle \operatorname{Res}^G_H \pi_{\mathrm{reg}}, \psi \rangle_H$, using the regular character $\pi_{\mathrm{reg}}$ as a probe. The regular character is the universal device for "every irreducible appears with positive multiplicity" arguments, because its decomposition $\pi_{\mathrm{reg}} = \sum_i (\deg \chi_i) \chi_i$ involves every irreducible of $G$ with positive multiplicity equal to its degree. **The lower bound side.** Restricting $\pi_{\mathrm{reg}}$ to $H$ gives a function on $H$ supported only at $1$ (since $\pi_{\mathrm{reg}}$ is supported only at $1 \in G$, and $1 \in H$). The $H$-inner product collapses to a single term: \begin{align*} \langle \operatorname{Res}^G_H \pi_{\mathrm{reg}}, \psi \rangle_H = \frac{1}{|H|} \cdot |G| \cdot \psi(1) = \frac{|G|}{|H|}\psi(1) > 0, \end{align*} strictly positive because $\psi$ is nonzero (so $\psi(1) = \dim W \geq 1$) and $H$ is a subgroup so $|G|/|H|$ is a positive integer (Lagrange). The point: this single number is **forced to be nonzero** by the support structure of $\pi_{\mathrm{reg}}$. **The expansion side.** Using $\pi_{\mathrm{reg}} = \sum_i (\deg \chi_i) \chi_i$ and linearity of restriction and inner product: \begin{align*} \langle \operatorname{Res}^G_H \pi_{\mathrm{reg}}, \psi \rangle_H = \sum_{i=1}^k (\deg \chi_i)\, \langle \operatorname{Res}^G_H \chi_i, \psi \rangle_H. \end{align*} This is a non-negative-coefficient sum: $\deg \chi_i = \chi_i(1) \geq 1$, and $\langle \operatorname{Res}^G_H \chi_i, \psi \rangle_H = $ (multiplicity of $\psi$ in $\operatorname{Res}^G_H \chi_i$) is a non-negative integer. **Combining.** A non-negative sum equal to a strictly positive number must have at least one strictly positive summand. Since $\deg \chi_i \geq 1$ never vanishes, the strictly positive summand has $\langle \operatorname{Res}^G_H \chi_i, \psi \rangle_H \geq 1$, so $\psi$ is a constituent of $\operatorname{Res}^G_H \chi_i$. That $\chi_i$ is the desired $\chi$. **Why the regular character?** The argument works because $\pi_{\mathrm{reg}}$ has two complementary properties: (a) its decomposition involves every irreducible of $G$ with positive multiplicity (so a nonzero contribution to $\langle \operatorname{Res} \pi_{\mathrm{reg}}, \psi \rangle$ propagates to **some** $\chi_i$), and (b) its restriction to any subgroup containing $1$ has nonzero inner product with any nonzero character of that subgroup. No smaller character of $G$ has property (a). This is why $\pi_{\mathrm{reg}}$ is the right probe. [/guided] [/step]