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 answer is purely a compilation of the ideas in the comments, given by Asaf Karagila and Noah Schweber. I have also made this a "Community Wiki", so I won't gain any reputation from any upvotes.

The thing is that in choiceless setting, most of our definitions in measure theory either don't make sense, or have different non-equivalent forms. To see an example look here. And also in certain cases we fail to have a measure on the Borel sets. For example in the Feferman–Levy model every set of reals is a countable union of countable sets and so it is not possible to have a measure on the Borel sets which is both countably additive and non-trivial. This is why some level of choice is required to even get started. And so the use of $\mathsf{AC}_\omega(\omega^\omega)$ in the above proof is justified.
