Induced modules from finite-dimensional B-modules have type their weights

Given: The Axiom of Choice, a finite-dimensional $\mathfrak{h}$-semisimple $\mathfrak{b}$-module $N$ with weight multiset $\mathrm{Wt}N$.

Lie's theorem: a finite-dimensional representation of the solvable Lie algebra $\mathfrak{b}$ has a $\mathfrak{b}$-stable flag $0=N_0\subset N_1\subset \cdots \subset N_n=N$ with one-dimensional quotients; because $\mathfrak{h}$ acts semisimply these can be chosen compatibly with the weight decomposition, and since $[\mathfrak{b},\mathfrak{b}]={\mathfrak{n}}^{+}$ acts by zero on a one-dimensional module, each quotient is the Borel module ${\mathbb{C}}_{{\mu }_j}$ of The one-dimensional Borel module of weight lambda for a weight ${\mu }_j$ of $N$ (Finite Lie triangularization and rank-one complete reducibility, The one-dimensional Borel module of weight lambda).

$U(\mathfrak{g})$ is free as a right $U(\mathfrak{b})$-module: the PBW monomials with negative-root factors before the Borel factors form a $U(\mathfrak{b})$-basis (PBW gives an ordered monomial basis for the enveloping algebra). Hence $U(\mathfrak{g}){\otimes }_{U(\mathfrak{b})}(-)$ is an exact functor.

$U(\mathfrak{g}){\otimes }_{U(\mathfrak{b})}{\mathbb{C}}_{\mu }\cong M(\mu )$ is the Verma module, and the isomorphisms are compatible with the universal property of Verma modules (The universal property of Verma modules, Type of a module with a Verma filtration).