\begin{corollary}[Specific fibring identity]\label{cor-fibre}
  \lean{sum_of_rdist_eq}\leanok
  Let $Y_1,Y_2,Y_3$ and $Y_4$ be independent $G$-valued random variables.
  Then
\begin{align*}
  & d[Y_1+Y_3; Y_2+Y_4] + d[Y_1|Y_1+Y_3; Y_2|Y_2+Y_4] \\
  &\qquad + \bbI[Y_1+Y_2 : Y_2 + Y_4 | Y_1+Y_2+Y_3+Y_4] = d[Y_1; Y_2] + d[Y_3; Y_4].
\end{align*}
\end{corollary}
\begin{proof}
  \uses{fibring-ident, add-entropy, relabeled-entropy-cond}\leanok
  We apply \Cref{fibring-ident} with $H := G \times G$, $H' := G$, $\pi$ the addition homomorphism $\pi(x,y) := x+y$, and with the random variables $Z_1 := (Y_1,Y_3)$ and $Z_2 := (Y_2,Y_4)$.  Then by independence (\Cref{add-entropy})
\[
  d[Z_1; Z_2] = d[Y_1; Y_2] + d[Y_3; Y_4]
\]
while by definition
\[
  d[\pi(Z_1); \pi(Z_2)] = d[Y_1+Y_3; Y_2+Y_4].
\]
Furthermore,
\[
  d[Z_1|\pi(Z_1); Z_2|\pi(Z_2)] = d[Y_1|Y_1+Y_3;Y_2|Y_2+Y_4],
\]
since $Z_1=(Y_1,Y_3)$ and $Y_1$ are linked by an invertible affine transformation once $\pi(Z_1)=Y_1+Y_3$ is fixed, and similarly for $Z_2$ and $Y_2$.  (This has to do with \Cref{relabeled-entropy-cond})
Finally, we have
\begin{align*}
  &\bbI[Z_1 + Z_2 : (\pi(Z_1),\pi(Z_2)) \,|\, \pi(Z_1) + \pi(Z_2)] \\
  &\ = \bbI[(Y_1+Y_2, Y_3+Y_4) : (Y_1+Y_3, Y_2+Y_4) \,|\, Y_1+Y_2+Y_3+Y_4] \\
  &\ = \bbI[Y_1+Y_2 : Y_2+Y_4 \,|\, Y_1+Y_2+Y_3+Y_4]
\end{align*}
where in the last line we used the fact that $(Y_1+Y_2, Y_1+Y_2+Y_3+Y_4)$ uniquely determine $Y_3+Y_4$ and similarly
$(Y_2+Y_4, Y_1+Y_2+Y_3+Y_4)$ uniquely determine $Y_1+Y_3$.  (This requires another helper lemma about entropy.)
\end{proof}
lemma sum_of_rdist_eq (Y : Fin 4 → Ω → G) (h_indep : iIndepFun Y μ)
  (h_meas : ∀ i, Measurable (Y i)) :
    d[Y 0; μ # Y 1; μ] + d[Y 2; μ # Y 3; μ]
      = d[(Y 0) - (Y 2); μ # (Y 1) - (Y 3); μ]
        + d[Y 0 | (Y 0) - (Y 2); μ # Y 1 | (Y 1) - (Y 3); μ]
        + I[(Y 0) - (Y 1) : (Y 1) - (Y 3) | (Y 0) - (Y 1) - (Y 2) + (Y 3); μ] := by
  let π : G × G →+ G := (AddMonoidHom.fst G G) - (AddMonoidHom.snd G G)
  have hπ {W_1 W_2 : Ω → G} : π ∘ ⟨W_1, W_2⟩ = W_1 - W_2 := rfl
  let Z_1 : Ω → G × G := ⟨Y 0, Y 2⟩
  let Z_2 : Ω → G × G := ⟨Y 1, Y 3⟩
  have hZ : Z_1 - Z_2 = ⟨Y 0 - Y 1, Y 2 - Y 3⟩ := rfl
  have m1 : Measurable Z_1 := (h_meas 0).prodMk (h_meas 2)
  have m2 : Measurable Z_2 := (h_meas 1).prodMk (h_meas 3)
  have h_indep_0 : IndepFun (Y 0) (Y 1) μ := h_indep.indepFun (by decide)
  have h_indep_2 : IndepFun (Y 2) (Y 3) μ := h_indep.indepFun (by decide)
  have h_indep_Z : IndepFun Z_1 Z_2 μ := h_indep.indepFun_prodMk_prodMk h_meas
    0 2 1 3 (by decide) (by decide) (by decide) (by decide)
  have h_indep_sub : IndepFun (Y 0 - Y 1) (Y 2 - Y 3) μ :=
    h_indep.indepFun_sub_sub h_meas 0 1 2 3 (by decide) (by decide) (by decide) (by decide)
  have msub (i j : Fin 4) : Measurable (Y i - Y j) := (h_meas i).sub (h_meas j)
  have h_add : d[Z_1; μ # Z_2; μ] = d[Y 0; μ # Y 1; μ] + d[Y 2; μ # Y 3; μ] := by
    rw [h_indep_0.rdist_eq (h_meas 0) (h_meas 1), h_indep_2.rdist_eq (h_meas 2) (h_meas 3),
      h_indep_Z.rdist_eq m1 m2, hZ,
      (entropy_pair_eq_add (h_meas 0) (h_meas 2)).2 (h_indep.indepFun (by decide)),
      (entropy_pair_eq_add (h_meas 1) (h_meas 3)).2 (h_indep.indepFun (by decide)),
      (entropy_pair_eq_add (msub 0 1) (msub 2 3)).2 h_indep_sub]
    ring_nf
  rw [← h_add, rdist_of_indep_eq_sum_fibre π h_indep_Z m1 m2]
  simp only [hπ, hZ]
  rw [sum_of_rdist_eq_step_condRuzsaDist h_indep h_meas,
    sum_of_rdist_eq_step_condMutualInfo h_meas]

/-- Let $Y_1,Y_2,Y_3$ and $Y_4$ be independent $G$-valued random variables.
  Then
$$d[Y_1+Y_3; Y_2+Y_4] + d[Y_1|Y_1+Y_3; Y_2|Y_2+Y_4] $$
$$ + I[Y_1+Y_2 : Y_2 + Y_4 | Y_1+Y_2+Y_3+Y_4] = d[Y_1; Y_2] + d[Y_3; Y_4].$$
-/