\begin{proposition}[General fibring identity]\label{fibring-ident}
  \lean{rdist_of_indep_eq_sum_fibre, rdist_le_sum_fibre}\leanok
  Let $\pi : H \to H'$ be a homomorphism additive groups, and let $Z_1,Z_2$ be $H$-valued random variables. Then we have
  \[
    d[Z_1; Z_2] \geq d[\pi(Z_1);\pi(Z_2)] + d[Z_1|\pi(Z_1); Z_2 |\pi(Z_2)].
  \]
  Moreover, if $Z_1,Z_2$ are taken to be independent, then the difference between the two sides is
$$I( Z_1 - Z_2 : (\pi(Z_1), \pi(Z_2))  |  \pi(Z_1 - Z_2) ).$$
\end{proposition}
\begin{proof}\uses{ruz-copy, independent-exist, submodularity,conditional-mutual-alt,chain-rule,relabeled-entropy, cond-dist-alt}\leanok
  Let $Z_1,Z_2$ be independent throughout (this is possible by \Cref{ruz-copy} and \Cref{independent-exist}).  By \Cref{cond-dist-alt}, We have
  \begin{align*}
    & d[Z_1  |\pi(Z_1); Z_2 |\pi(Z_2)] \\
    & = \bbH[Z_1 - Z_2 | \pi(Z_1),\pi(Z_2)] - \tfrac{1}{2} \bbH[Z_1 | \pi(Z_1)] - \tfrac{1}{2} \bbH[Z_2 | \pi(Z_2)] \\
    & \leq  \bbH[Z_1 - Z_2 | \pi(Z_1+Z_2)]  - \tfrac{1}{2} \bbH[Z_1 | \pi(Z_1)] - \tfrac{1}{2}H[Z_2 | \pi(Z_2)] \\
    & = d[Z_1;Z_2] - d[\pi(Z_1);\pi(Z_2)].
  \end{align*}
  In the middle step, we used \Cref{submodularity}, and in the last step we used the fact that
  \[\bbH[Z_1 - Z_2 |  \pi(Z_1-Z_2)] = \bbH[Z_1 - Z_2] - \bbH[\pi(Z_1-Z_2)]\]
  (thanks to \Cref{chain-rule} and \Cref{relabeled-entropy}) and that
  \[\bbH[Z_i| \pi(Z_i)] = \bbH[Z_i] - \bbH[\pi(Z_i)]\] (since $Z_i$ determines $\pi(Z_i)$).
  This gives the claimed inequality. The difference between the two sides is precisely
  \[\bbH[Z_1 - Z_2  | \pi(Z_1 - Z_2)] - \bbH[Z_1 - Z_2  | \pi(Z_1),\pi(Z_2)].\]
  To rewrite this in terms of (conditional) mutual information, we use the identity
  \[\bbH[A|B] - \bbH[A | B,C] = \bbI[A : C | B],\]
  (which follows \Cref{conditional-mutual-alt})
  taking
  $A := Z_1 - Z_2$, $B := \pi(Z_1 - Z_2)$ and $C := (\pi(Z_1),\pi(Z_{2}))$, and noting that in this case $\bbH[A | B,C] = \bbH[A | C]$ since $C$ uniquely determines $B$ (this may require another helper lemma about entropy).
  This completes the proof.
\end{proof}
lemma rdist_le_sum_fibre {Z_1 : Ω → H} {Z_2 : Ω' → H}
  (h1 : Measurable Z_1) (h2 : Measurable Z_2) [FiniteRange Z_1] [FiniteRange Z_2] :
  d[π ∘ Z_1; μ # π ∘ Z_2; μ'] + d[Z_1|π∘Z_1; μ # Z_2|π∘Z_2; μ'] ≤ d[Z_1; μ # Z_2; μ']:= by
  obtain ⟨ν, W_1, W_2, hν, m1, m2, hi, hi1, hi2, _, _⟩ := ProbabilityTheory.independent_copies_finiteRange h1 h2 μ μ'
  have hπ : Measurable π := .of_discrete
  have hφ : Measurable (fun x ↦ (x, π x)) := .of_discrete
  have hπ1 : IdentDistrib (⟨Z_1, π ∘ Z_1⟩) (⟨W_1, π ∘ W_1⟩) μ ν := hi1.symm.comp hφ
  have hπ2 : IdentDistrib (⟨Z_2, π ∘ Z_2⟩) (⟨W_2, π ∘ W_2⟩) μ' ν := hi2.symm.comp hφ
  rw [← hi1.rdist_eq hi2, ← (hi1.comp hπ).rdist_eq (hi2.comp hπ),
    rdist_of_indep_eq_sum_fibre π hi m1 m2,
    condRuzsaDist_of_copy h1 (hπ.comp h1) h2 (hπ.comp h2) m1 (hπ.comp m1) m2 (hπ.comp m2) hπ1 hπ2]
  exact le_add_of_nonneg_right (condMutualInfo_nonneg (by fun_prop) (by fun_prop))