Choosing a "good" partition given that non-null measurable sets have a "good" subset with positive measure I came up with this lemma when solving some other problem:

Given a measure space $(X, \mu)$ with $\mu(X) < +\infty$. There is a collection $\mathcal G \subseteq 2^X$ of "good" subsets, which all have positive measure. For every set $A \subseteq X$ with positive measure, there is a good subset $G \subseteq A$. Then we can partition $X$ into countably many good sets, and one set with measure zero.

Proof: If we consider all sets of non-intersecting good subsets, then they form a partial order under inclusion. And given a chain in this partial order, taking the union givens a upper bound. And therefore there must be some maximal set of non-intersecting good subsets $\mathcal A$. This must be a countable set, and $X \setminus \bigcup \mathcal A$ must be zero.
This uses the axiom of choice, and I wonder exactly which version of choice is needed. Dependent choice is not enough because after $\omega$ steps the chosen good subsets might have total measure converging to a number less than $\mu(X)$. Therefore it seems like there should be a version of "transfinite dependent choice" up to $\omega_1$ in my intuition. Does this make sense? If so, what is such a choice principle called?
 A: Let me give you an alternative proof that only uses DC. I see mihaild had the same idea in the comments.
For each natural number $n\geq 1$, let $\mathcal{G}_n = \{G\in \mathcal{G}\mid \mu(G)>\frac{1}{n}\}$. Then $\mathcal{G}_n\subseteq \mathcal{G}_{n+1}$ for all $n$, and $\bigcup_{n\geq 1}\mathcal{G}_n = \mathcal{G}$. Since $\mu(X)$ is finite, a family of pairwise disjoint sets in $\mathcal{G}_n$ is finite, with size less than $n\mu(X)$. It follows that any family of pairwise disjoint sets in $\mathcal{G}_n$ can be extended to a maximal such family (and we do not need any choice to prove this).
Now, using DC, pick a maximal family $F_n$ of pairwise  disjoint sets in $\mathcal{G}_n$ such that $F_n\subseteq F_{n+1}$ for all $n\geq 1$. Let $F = \bigcup_{n\geq 1} F_n$. Then $F$ is a family of pairwise disjoint sets in $\mathcal{G}$. I claim that $X\setminus \bigcup F$ has measure $0$. If not, we can find some good set $G\subseteq X\setminus \bigcup F$, and $G\in \mathcal{G}_n$ for some $n$. Then $F_n\cup \{G\}$ is a family of pairwise disjoint sets in $\mathcal{G}_n$, contradicting maximality of $F_n$.
A: In addition to Alex's answer, lower bound of how much choice we need is at least axiom of countable choice for finite sets. Still interesting question what do we have between this and DC.
Let $S_n$ be a countable family of finite sets such that $\cup S_n$ is not countable.
Let $X = \cup_n S_n$, all subsets been measurable and $\mu(Y) = \sum \{2^{-n - |S_n|} | y \in Y, y \in S_n\}$ - each point in $S_n$ has measure $2^{-n - |S_n|}$, and then continue by additivity. Note that only empty set has zero measure, and measure of the entire $X$ is $1$.
Say that singletons are good subsets. Every set of positive measure has a singleton subset. But $X$ is uncountable, thus not a countable union of singleton sets.
