Solution (source code)

= Solution

Choose a locally finite cover $(U_\alpha)$ such that on every chart meeting $Y$ there is a smooth defining function $f_\alpha$ with
$$
Y\cap U_\alpha=f_\alpha^{-1}(0),
\qquad df_\alpha|_Y\ne0,
$$
and take $f_\alpha=1$ on charts disjoint from $Y$. On an overlap, the supplied division lemma extends
$$
g_{\alpha\beta}=\frac{f_\alpha}{f_\beta}
$$
smoothly across $Y$. After shrinking the charts, this extension is nowhere zero. The identities $g_{\alpha\beta}g_{\beta\gamma}=g_{\alpha\gamma}$ make these functions transition functions for a <real line bundle> $L\to X$.

Choose local frames $e_\alpha$ with $e_\beta=g_{\alpha\beta}e_\alpha$. Then the local sections
$$
s|_{U_\alpha}=f_\alpha e_\alpha
$$
agree on overlaps and define a global section. Its zero set is exactly $Y$. Along $Y$, its vertical derivative is represented by the nonzero covector $df_\alpha$, so $s$ is transverse to the zero section, as in the <transverse intersection theorem>. This is the <defining line bundle of a properly embedded hypersurface>.