Does the existence of a minimal cover for a subset of reals need some form of choice? In Kanamori's book, "The Higher Infinite" p. 376, he defines a minimal cover of some $A \subseteq \omega^\omega$, to be any $B \subseteq \omega^\omega$, such that $A\subseteq B$ and that $B$ is Lebesgue measurable and if $Z \subseteq B-A$ is Lebesgue measurable, then $m_L(Z) = 0$. And he claims that picking some $B$ with $A\subseteq B$ and $m_L(B)$ minimal, does the job. [Here $m_L$ denotes the Lebesgue measure.]
Now here is my problem. The whole premise of this chapter is that we don't want to use choice to do these things. But any way I try to construct such a $B$, I inevitably use some form of choice. The best I can do is $\mathsf{AC}_\omega(\omega^\omega)$. Is there some choice-free way to do this?

A sketch of a proof with $\mathsf{AC}_\omega(\omega^\omega)$: Let $x = \inf\{m_L(B): A\subseteq B \text{ and } B \text{ is Lebesgue measurable}\}$. By $\mathsf{AC}_\omega(\omega^\omega)$, let $\langle B_n: n<\omega\rangle$ be a sequence such that $A\subseteq B_n$ and $m_L(B_n) \rightarrow x$ as $n \rightarrow \infty$. Now $B = \bigcap_n B_n$ is the desired minimal cover. $\square$

This is in fact a theorem of ZF. The Caratheodory construction of Lebesgue measure works in ZF, though without choice it need not be $\sigma$-additive. Every Borel codable set of reals is measurable but not necessarily every Borel set. See the paper cited below.
Let $U_i$ enumerate the basic open sets of $\omega^{\omega}.$ By (finite) subadditivity of $\lambda^*$ and adjusting the proof of the Lebesgue density theorem, we have that for any $X$ with $\lambda^*(X)>0$ and $\epsilon >0,$ there is $U_i$ such that $\lambda^*(X \cap U_i) > (1-\epsilon) \lambda(U_i).$
Define $S_n$ recursively by having $i \in S_n$ if $\lambda^*(A \cap U_i \setminus \bigcup_{j<i, j \in S_n} U_j)>\frac{n-1}{n} \lambda(U_i).$ Let $V_n = \bigcup_{i \in S_n} U_i$ and $V = \bigcap_{n<\omega} V_n.$
By our density lemma, each $A \setminus V_n$ is null. Since $\lambda^*$ is additive among subsets of disjoint measurable sets, we have
$$\lambda(V_n) - \frac{1}{n} \le
\frac{n-1}{n}\lambda(V_n) \le \sum_{i \in S_n} \lambda^*\left (A \cap U_i \setminus \bigcup_{j<i, j \in S_n} U_j \right ) \le \lambda^*(A) \le \lambda^*(A \cup V_n) =\lambda(V_n).$$
We compute
$$\lambda^*(A \setminus V) \le \inf_{n<\omega} \left ( \lambda^*\left (\bigcap_{i<n} V_n \setminus V \right ) + \lambda^*\left (A \setminus \bigcap_{i<n} V_n \right ) \right ) =0.$$
Therefore, $B := A \cup V$ is measurable, with
$$\lambda^*(A) \le \lambda(B) = \lambda(V) \le \inf_{n<\omega} \lambda(V_n)
\le \inf_{n<\omega} \left (\lambda^*(A) + \frac{1}{n} \right) = \lambda^*(A).$$
So $B$ is as desired.
Foreman, Matthew; Wehrung, Friedrich, The Hahn-Banach theorem implies the existence of a non-Lebesgue measurable set, Fundam. Math. 138, No. 1, 13-19 (1991). ZBL0792.28005.
