\begin{lemma}[General inequality]\label{gen-ineq}\lean{gen_ineq_00} \leanok
Let $X_1, X_2, X_3, X_4$ be independent $G$-valued random variables, and let $Y$ be another $G$-valued random variable.  Set $S := X_1+X_2+X_3+X_4$. Then
  \begin{align*}
    &  d[Y; X_1+X_2|X_1 + X_3, S] - d[Y; X_1] \\
    &\quad \leq \tfrac{1}{4} (d[X_1;X_2] + 2d[X_1;X_3] + d[X_2;X_4])\\
    &\qquad \qquad + \tfrac{1}{4} (d[X_1|X_1+X_3;X_2|X_2+X_4] - d[X_3|X_3+X_4; X_1|X_1+X_2])\\
    &\qquad \qquad + \tfrac{1}{8} (\bbH[X_1+X_2] - \bbH[X_3+X_4] + \bbH[X_2] - \bbH[X_3]\\
    &\qquad \qquad \qquad + \bbH[X_2|X_2+X_4] - \bbH[X_1|X_1+X_3]).
\end{align*}
\end{lemma}
\begin{proof}\uses{cond-dist-fact, first-useful, cor-fibre}\leanok
  On the one hand, by \Cref{cond-dist-fact} and two applications of \Cref{first-useful} we have
  \begin{align*}
  &d[Y;X_1+X_2|X_1 + X_3, S] \\
  &\quad \leq d[Y;X_1+X_2|S] + \tfrac{1}{2} \bbI[X_1 + X_2 : X_1 + X_3|S] \\
  &\quad \leq d[Y;X_1+X_2]\\
  &\qquad + \tfrac{1}{2} (d[X_1+X_2;X_3+X_4] + \bbI[X_1 + X_2 : X_1 + X_3|S])\\
  &\qquad + \tfrac{1}{4} (\bbH[X_1+X_2] - \bbH[X_3+X_4])\\
  &\quad \leq d[Y;X_1] \\
  &\qquad + \tfrac{1}{2} (d[X_1;X_2] + d[X_1+X_2;X_3+X_4] + \bbI[X_1 + X_2 : X_1 + X_3|S])\\
  &\qquad + \tfrac{1}{4} (\bbH[X_1+X_2] - \bbH[X_3+X_4] + \bbH[X_2] - \bbH[X_1]).
  \end{align*}
  From \Cref{cor-fibre} (with $Y_1,Y_2,Y_3,Y_4$ set equal to $X_3, X_1, X_4, X_2$ respectively) one has
  $$ d[X_3+X_4; X_1+X_2] + d[X_3|X_3+X_4; X_1|X_1+X_2] $$
  $$ + \bbI[X_3 + X_1 : X_1 + X_2|S] = d[X_3;X_1] + d[X_4;X_2].$$
Rearranging the mutual information and Ruzsa distances slightly, we conclude that
\begin{align*}
  &d[Y;X_1+X_2|X_1 + X_3, S] \\
  &\quad \leq d[Y;X_1] \\
  &\qquad + \tfrac{1}{2} (d[X_1;X_2] + d[X_1;X_3] + d[X_2;X_4] - d[X_3|X_3+X_4; X_1|X_1+X_2])\\
  &\qquad + \tfrac{1}{4} (\bbH[X_1+X_2] - \bbH[X_3+X_4] + \bbH[X_2] - \bbH[X_1]).
  \end{align*}



  On the other hand, $(X_1+X_2|X_1 + X_3, S)$ has an identical distribution to the independent sum of $(X_1|X_1+X_3)$ and $(X_2|X_2+X_4)$.  We may therefore apply \Cref{first-useful} to conditioned variables $(X_1|X_1+X_3=s)$ and $(X_2|X_2+X_4=t)$ and average in $s,t$ to
  obtain the alternative bound
  \begin{align*}
  &  d[Y;X_1+X_2|X_1 + X_3, S] \\
  &\quad \leq d[Y;X_1|X_1+X_3] + \tfrac{1}{2} d[X_1|X_1+X_3; X_2|X_2+X_4] \\
  &\qquad + \tfrac{1}{4} (\bbH[X_2|X_2+X_4] - \bbH[X_1|X_1+X_3]) \\
  &\quad  \leq d[Y;X_1] \\
  &\qquad + \tfrac{1}{2} (d[X_1;X_3] + d[X_1|X_1+X_3;X_2|X_2+X_4])\\
  &\qquad + \tfrac{1}{4} (\bbH[X_2|X_2+X_4] - \bbH[X_1|X_1+X_3] + \bbH[X_1] - \bbH[X_3]).
  \end{align*}
  If one takes the arithmetic mean of these two bounds and simplifies using \Cref{cor-fibre}, one obtains the claim.
\end{proof}
lemma gen_ineq_00 : d[Y # Z₁ + Z₂ | ⟨Z₁ + Z₃, Sum⟩] - d[Y # Z₁] ≤
    (d[Z₁ # Z₂] + 2 * d[Z₁ # Z₃] + d[Z₂ # Z₄]) / 4
    + (d[Z₁ | Z₁ + Z₃ # Z₂ | Z₂ + Z₄] - d[Z₁ | Z₁ + Z₂ # Z₃ | Z₃ + Z₄]) / 4
    + (H[Z₁ + Z₂] - H[Z₃ + Z₄] + H[Z₂] - H[Z₃] + H[Z₂ | Z₂ + Z₄] - H[Z₁ | Z₁ + Z₃]) / 8 := by
  have I1 := gen_ineq_aux1 Y hY Z₁ Z₂ Z₃ Z₄ hZ₁ hZ₂ hZ₃ hZ₄ h_indep
  have I2 := gen_ineq_aux2 Y hY Z₁ Z₂ Z₃ Z₄ hZ₁ hZ₂ hZ₃ hZ₄ h_indep
  linarith

include hY hZ₁ hZ₂ hZ₃ hZ₄ h_indep in