Solution (source code)

= Solution

Since the <strongly inaccessible cardinal> $\lambda$ is inaccessible, $(V_\lambda,\in)$ is a <model of a first-order theory>[model] of ZFC. The <Downward Lowenheim-Skolem theorem> gives an <elementary substructure>
$$
X\prec V_\lambda
$$
of <cardinal number>[cardinality] $\kappa$ such that
$$
V_\kappa\cup\{\kappa,U\}\subseteq X.
$$
One may obtain $X$ concretely as the <Skolem hull> of this set; its cardinality remains $\kappa$ because the language of set theory is countable and $|V_\kappa|=\kappa$.

Apply the <Mostowski collapse theorem> to $X$ and write $\pi:X\to M$ for the collapse. Then $M$ is a <transitive set>, $|M|=\kappa$, and $\pi$ fixes $V_\kappa$ pointwise. It also fixes $\kappa$, because it fixes every ordinal below $\kappa$. By <elementary substructure>[elementarity], $X$ satisfies ZFC and regards $U$ as a <kappa-complete filter> that is a <nonprincipal ultrafilter> on $\kappa$. Therefore, with $\bar U=\pi(U)$,
$$
(M,\in)\models\mathrm{ZFC}+\text{“$\kappa$ is a measurable cardinal, witnessed by $\bar U$.”}
$$
The internal ultrafilter $\bar U$ need not equal the original $U$.