\begin{lemma}\label{torsion-dist-shrinking}\lean{torsion_dist_shrinking}\leanok
If $G$ is a torsion-free group and $X,Y$ are $G$-valued random variables and $\phi:G\to \mathbb{F}_2^d$ is a homomorphism then
\[\mathbb{H}(\phi(X))\leq 10d[X;Y].\]
\end{lemma}
\begin{proof}
\uses{fibring-ineq, torsion-free-doubling, dist-zero}\leanok
By \Cref{fibring-ineq} and \Cref{torsion-free-doubling} we have
\[d[\phi(X);\phi(2Y)]\leq d[X;2Y]\leq 5d[X;Y]\]
and $\phi(2Y)=2\phi(Y)\equiv 0$ so the left-hand side is equal to $d[\phi(X);0]=\mathbb{H}(\phi(X))/2$ (using \Cref{dist-zero}).
\end{proof}
lemma torsion_dist_shrinking {H : Type*} [FiniteRange X] [FiniteRange Y] (hX : Measurable X)
    (hY : Measurable Y) [AddCommGroup H] [Module (ZMod 2) H]
    [MeasurableSpace H] [MeasurableSingletonClass H] [Countable H]
    (hG : AddMonoid.IsTorsionFree G) (φ : G →+ H) :
    H[φ ∘ X ; μ] ≤ 10 * d[X ; μ # Y ; μ'] :=
  calc
    H[φ ∘ X ; μ] = 2 * d[φ ∘ X ; μ # φ ∘ (Y + Y) ; μ'] := by
      rw [map_comp_add, ZModModule.add_self, Pi.zero_def, rdist_zero_eq_half_ent, mul_div_cancel₀]
      exact two_ne_zero
    _ ≤ 2 * d[X ; μ # Y + Y ; μ'] := by gcongr; exact rdist_of_hom_le φ hX (hY.add hY)
    _ ≤ 2 * (5 * d[X ; μ # Y ; μ']) := by gcongr; exact torsion_free_doubling X Y μ μ' hX hY hG
    _ = 10 * d[X ; μ # Y ; μ'] := by ring

end Torsion