\begin{lemma}[Comparing sums]\label{compare-sums}\lean{ent_of_sum_le_ent_of_sum}\leanok  Let $(X_i)_{1 \leq i \leq m}$ and $(Y_j)_{1 \leq j \leq l}$ be tuples of jointly independent random variables (so the $X$'s and $Y$'s are also independent of each other), and let $f: \{1,\dots,l\} \to \{1,\dots,m\}$ be a function, then
  $$ \bbH[\sum_{j=1}^l Y_j] \leq \bbH[ \sum_{i=1}^m X_i ] + \sum_{j=1}^l (\bbH[ Y_j - X_{f(j)}] - \bbH[X_{f(j)}]).$$
\end{lemma}
\begin{proof}\uses{klm-1, kv, neg-ent, sumset-lower}  Write $W := \sum_{i=1}^m X_i$.  From \Cref{sumset-lower} we have
$$ \bbH[\sum_{j=1}^l Y_j]  \leq \bbH[-W + \sum_{j=1}^l Y_j]$$
while from \Cref{klm-1} one has
$$ \bbH[-W + \sum_{j=1}^l Y_j] \leq \bbH[-W] + \sum_{j=1}^l \bbH[-W + Y_j] - \bbH[-W].$$
From \Cref{kv} one has
$$ \bbH[-W + Y_j] - \bbH[-W] \leq \bbH[-X_{f(j)} + Y_j] - \bbH[-X_{f(j)}].$$
The claim now follows from \Cref{neg-ent} and some elementary algebra.
\end{proof}
lemma ent_of_sum_le_ent_of_sum [IsProbabilityMeasure μ] {I : Type*} {s t : Finset I} (hdisj : Disjoint s t)
    (hs : Finset.Nonempty s) (ht : Finset.Nonempty t) (X : I → Ω → G) (hX : (i : I) → Measurable (X i))
    (hX' : (i : I) → FiniteRange (X i)) (h_indep : iIndepFun X μ) (f : I → I)
    (hf : Finset.image f t ⊆ s) :
    H[∑ i ∈ t, X i; μ] ≤ H[∑ i ∈ s, X i; μ] + ∑ i ∈ t, (H[X i - X (f i); μ] - H[X (f i); μ]) := by
  sorry

/-- Let `X,Y,X'` be independent `G`-valued random variables, with `X'` a copy of `X`,
and let `a` be an integer. Then `H[X - (a+1)Y] ≤ H[X - aY] + H[X - Y - X'] - H[X]` -/