[proofplan] We combine the [Biregular Expansion](/theorems/2582) theorem with [Hall's Marriage Theorem](/theorems/2018). The expansion theorem converts the biregularity hypothesis into the inequality $|\Gamma(A)| \geq (|Y|/|X|)|A|$ for every $A \subseteq X$. Since $|X| \leq |Y|$, the ratio $|Y|/|X| \geq 1$, which gives $|\Gamma(A)| \geq |A|$ for every $A \subseteq X$ — precisely Hall's condition. Hall's theorem then delivers the complete matching. [/proofplan] [step:Apply the biregular expansion bound to every subset of $X$] Let $A \subseteq X$ be an arbitrary subset. Since $G = (X, Y; E)$ is biregular, the [Biregular Expansion](/theorems/2582) theorem applies and gives \begin{align*} \frac{|\Gamma(A)|}{|Y|} \geq \frac{|A|}{|X|}. \end{align*} Rearranging: \begin{align*} |\Gamma(A)| \geq \frac{|Y|}{|X|} |A|. \end{align*} By hypothesis $|X| \leq |Y|$, so $|Y|/|X| \geq 1$. Therefore \begin{align*} |\Gamma(A)| \geq |A| \end{align*} for every $A \subseteq X$. [guided] The goal is to verify Hall's condition, which requires $|\Gamma(A)| \geq |A|$ for every subset $A \subseteq X$. We need a way to convert the structural hypothesis — biregularity — into this neighbourhood-size lower bound. The [Biregular Expansion](/theorems/2582) theorem does exactly this. It applies to any $(k, \ell)$-regular bipartite graph and gives, for every $A \subseteq X$: \begin{align*} \frac{|\Gamma(A)|}{|Y|} \geq \frac{|A|}{|X|}. \end{align*} The hypothesis of the Biregular Expansion theorem is that $G$ is $(k, \ell)$-regular for some $k, \ell \geq 1$. Since $G$ is biregular by assumption, this is satisfied. Rearranging the expansion inequality: \begin{align*} |\Gamma(A)| \geq \frac{|Y|}{|X|} |A|. \end{align*} Now the hypothesis $|X| \leq |Y|$ enters: it ensures $|Y|/|X| \geq 1$, so \begin{align*} |\Gamma(A)| \geq \frac{|Y|}{|X|} |A| \geq 1 \cdot |A| = |A|. \end{align*} This holds for every $A \subseteq X$, which is precisely Hall's condition. Why is the hypothesis $|X| \leq |Y|$ necessary? If $|X| > |Y|$, the ratio $|Y|/|X| < 1$, and the expansion bound only gives $|\Gamma(A)| \geq (|Y|/|X|)|A| < |A|$. In this case, Hall's condition can fail: taking $A = X$ gives $|\Gamma(X)| \leq |Y| < |X| = |A|$. [/guided] [/step] [step:Conclude by Hall's Marriage Theorem] Since $|\Gamma(A)| \geq |A|$ for every $A \subseteq X$, Hall's condition is satisfied. By [Hall's Marriage Theorem](/theorems/2018), there exists a complete matching from $X$ into $Y$. [/step]