[proofplan]
We write the atoms of the finer partition $\alpha$ in groups according to the atom of $\beta$ that contains them modulo null sets. The entropy of each $\beta$-atom is then compared with the total entropy of the $\alpha$-atoms lying inside it. The difference is a non-negative conditional entropy term, so summing over all atoms of $\beta$ gives the desired monotonicity.
[/proofplan]
[step:Group the atoms of $\alpha$ according to the atoms of $\beta$]
Let $I$ and $J$ be finite index sets such that
\begin{align*}
\alpha=\{A_i : i \in I\}
\end{align*}
and
\begin{align*}
\beta=\{B_j : j \in J\}.
\end{align*}
Define the mass functions $p:I \to [0,1]$ and $q:J \to [0,1]$ by
\begin{align*}
p(i)=\mu(A_i)
\end{align*}
and
\begin{align*}
q(j)=\mu(B_j).
\end{align*}
For each $j \in J$, let $I_j \subset I$ be the set of indices whose atoms of $\alpha$ occur in the chosen subfamily representing $B_j$ modulo null sets. Thus
\begin{align*}
\mu\left(B_j \triangle \bigcup_{i \in I_j} A_i\right)=0.
\end{align*}
Because the atoms of $\alpha$ are pairwise disjoint and the index set $I_j$ is finite, finite additivity of $\mu$ gives
\begin{align*}
q(j)=\mu(B_j)=\sum_{i \in I_j} p(i).
\end{align*}
The sets $I_j$ are pairwise disjoint and their union is $I$, up to indices $i$ with $p(i)=0$; such indices do not affect entropy because $0\log 0$ is interpreted as $0$.
[/step]
[step:Compute the entropy gain inside one atom of $\beta$]
Define $\eta:[0,1]\to[0,\infty)$ by
\begin{align*}
\eta(t)= -t\log t \quad \text{for } t>0
\end{align*}
and $\eta(0)=0$. Then
\begin{align*}
H_\mu(\alpha)=\sum_{i \in I}\eta(p(i))
\end{align*}
and
\begin{align*}
H_\mu(\beta)=\sum_{j \in J}\eta(q(j)).
\end{align*}
Fix $j \in J$. If $q(j)=0$, then $p(i)=0$ for every $i \in I_j$, so
\begin{align*}
\sum_{i \in I_j}\eta(p(i))=\eta(q(j))=0.
\end{align*}
Now assume $q(j)>0$. Define the conditional mass function $r_j:I_j\to[0,1]$ by
\begin{align*}
r_j(i)=\frac{p(i)}{q(j)}.
\end{align*}
Since $q(j)=\sum_{i \in I_j}p(i)$, we have
\begin{align*}
\sum_{i \in I_j} r_j(i)=1.
\end{align*}
For each $i \in I_j$ with $p(i)>0$,
\begin{align*}
-\ p(i)\log p(i)= -\ p(i)\log q(j)-p(i)\log r_j(i).
\end{align*}
The same identity remains valid for $p(i)=0$ by the convention $\eta(0)=0$. Summing over $i \in I_j$ gives
\begin{align*}
\sum_{i \in I_j}\eta(p(i))=\eta(q(j))+q(j)\sum_{i \in I_j}\eta(r_j(i)).
\end{align*}
Since $0\le r_j(i)\le 1$ for every $i \in I_j$, each term $\eta(r_j(i))$ is non-negative. Hence
\begin{align*}
\sum_{i \in I_j}\eta(p(i))\ge \eta(q(j)).
\end{align*}
[guided]
The purpose of this step is to measure exactly what happens when one atom $B_j$ of the coarse partition is split into the atoms $A_i$ of the finer partition lying inside it. The total mass of $B_j$ is
\begin{align*}
q(j)=\mu(B_j)=\sum_{i \in I_j}p(i).
\end{align*}
If $q(j)=0$, then every $p(i)$ with $i \in I_j$ is also $0$, because the summands are non-negative. Therefore the entropy contribution on both sides is $0$:
\begin{align*}
\sum_{i \in I_j}\eta(p(i))=\eta(q(j))=0.
\end{align*}
Suppose now that $q(j)>0$. We normalize the masses inside $B_j$ by defining $r_j:I_j\to[0,1]$ as
\begin{align*}
r_j(i)=\frac{p(i)}{q(j)}.
\end{align*}
This is a probability distribution on the finite set $I_j$, because
\begin{align*}
\sum_{i \in I_j}r_j(i)=\frac{1}{q(j)}\sum_{i \in I_j}p(i)=1.
\end{align*}
For $i \in I_j$, the identity $p(i)=q(j)r_j(i)$ separates the coarse mass $q(j)$ from the conditional mass $r_j(i)$. Using $\log(ab)=\log a+\log b$ when $p(i)>0$, we get
\begin{align*}
-\ p(i)\log p(i)= -\ p(i)\log q(j)-p(i)\log r_j(i).
\end{align*}
When $p(i)=0$, both sides are interpreted as $0$, so the identity is still valid under the entropy convention. Summing over all $i \in I_j$ gives
\begin{align*}
\sum_{i \in I_j}\eta(p(i))= -\left(\sum_{i \in I_j}p(i)\right)\log q(j)+q(j)\sum_{i \in I_j}\eta(r_j(i)).
\end{align*}
Since $\sum_{i \in I_j}p(i)=q(j)$, this becomes
\begin{align*}
\sum_{i \in I_j}\eta(p(i))=\eta(q(j))+q(j)\sum_{i \in I_j}\eta(r_j(i)).
\end{align*}
The second term is non-negative because $q(j)>0$ and $\eta(t)\ge 0$ for every $t\in[0,1]$. Therefore
\begin{align*}
\sum_{i \in I_j}\eta(p(i))\ge \eta(q(j)).
\end{align*}
This is the whole monotonicity mechanism: splitting a mass cannot decrease entropy.
[/guided]
[/step]
[step:Sum the non-negative entropy gains over all atoms of $\beta$]
Using the disjoint grouping of the $\alpha$-atoms by the sets $I_j$, and ignoring only zero-mass atoms which contribute $0$ to entropy, we obtain
\begin{align*}
H_\mu(\alpha)=\sum_{j \in J}\sum_{i \in I_j}\eta(p(i)).
\end{align*}
By the one-atom estimate proved above,
\begin{align*}
\sum_{j \in J}\sum_{i \in I_j}\eta(p(i))\ge \sum_{j \in J}\eta(q(j)).
\end{align*}
The right-hand side is precisely $H_\mu(\beta)$. Therefore
\begin{align*}
H_\mu(\alpha)\ge H_\mu(\beta).
\end{align*}
This proves that entropy is monotone under finite measurable refinement.
[/step]
