\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_of_indep_eq_sum_fibre {Z_1 Z_2 : Ω → H} (h : IndepFun Z_1 Z_2 μ)
    (h1 : Measurable Z_1) (h2 : Measurable Z_2) [FiniteRange Z_1] [FiniteRange Z_2]:
    d[Z_1; μ # Z_2; μ] = d[π ∘ Z_1; μ # π ∘ Z_2; μ] + d[Z_1|π∘Z_1; μ # Z_2|π∘Z_2; μ] + I[Z_1-Z_2 : ⟨π∘Z_1, π∘Z_2⟩ | π∘(Z_1 - Z_2); μ] := by
  have hπ : Measurable π := .of_discrete
  have step1 : d[Z_1; μ # Z_2; μ] = d[π ∘ Z_1; μ # π ∘ Z_2; μ] +
      H[(Z_1 - Z_2)| π ∘ (Z_1 - Z_2); μ] - H[Z_1 | π ∘ Z_1; μ] / 2 - H[Z_2 | π ∘ Z_2; μ] / 2 := by
    have hsub : H[(Z_1 - Z_2)| π ∘ (Z_1 - Z_2); μ] = H[(Z_1 - Z_2); μ] - H[π ∘ (Z_1 - Z_2); μ] :=
      condEntropy_comp_self (by fun_prop) hπ
    rw [h.rdist_eq h1 h2, (h.comp hπ hπ).rdist_eq (hπ.comp h1) (hπ.comp h2),
      condEntropy_comp_self h1 hπ, condEntropy_comp_self h2 hπ, hsub, map_comp_sub π]
    ring_nf
  have m0 : Measurable (fun x ↦ (x, π x)) := .of_discrete
  have h' : IndepFun (⟨Z_1, π ∘ Z_1⟩) (⟨Z_2, π ∘ Z_2⟩) μ := h.comp m0 m0
  have m1 : Measurable (Z_1 - Z_2) := h1.sub h2
  have m2 : Measurable (⟨↑π ∘ Z_1, ↑π ∘ Z_2⟩) := (hπ.comp h1).prodMk (hπ.comp h2)
  have m3 : Measurable (↑π ∘ (Z_1 - Z_2)) := hπ.comp m1
  have entroplem : H[Z_1 - Z_2|⟨⟨↑π ∘ Z_1, ↑π ∘ Z_2⟩, ↑π ∘ (Z_1 - Z_2)⟩; μ]
      = H[Z_1 - Z_2|⟨↑π ∘ Z_1, ↑π ∘ Z_2⟩; μ] := by
    rw [map_comp_sub π]
    let f : H' × H' → (H' × H') × H' := fun (x,y) ↦ ((x,y), x - y)
    have hf : Injective f := fun _ _ h ↦ (Prod.ext_iff.1 h).1
    have mf : Measurable f := measurable_id.prodMk measurable_sub
    refine condEntropy_of_injective' μ m1 m2 f hf (mf.comp m2)
  rw [step1, condMutualInfo_eq' m1 m2 m3, entroplem,
    condRuzsaDist_of_indep h1 (hπ.comp h1) h2 (hπ.comp h2) μ h']
  ring_nf