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?
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$.