\begin{lemma}[Upper bound on conditioned Ruzsa distance]\label{cond-dist-fact}
  \uses{cond-dist-def, information-def}
  \lean{condRuzsaDist_le, condRuzsaDist_le'}\leanok
  Suppose that $(X, Z)$ and $(Y, W)$ are random variables, where $X, Y$ take values in an abelian group. Then
  \[   d[X  | Z;Y | W] \leq d[X ; Y] + \tfrac{1}{2}  \bbI[X : Z] + \tfrac{1}{2}  \bbI[Y : W].\]
  In particular,
  \[   d[X ;Y | W] \leq d[X ; Y] + \tfrac{1}{2}  \bbI[Y : W].\]
\end{lemma}
\begin{proof}
\uses{cond-dist-alt, independent-exist, cond-reduce}\leanok
Using \Cref{cond-dist-alt} and \Cref{independent-exist}, if $(X',Z'), (Y',W')$ are independent copies of the variables $(X,Z)$, $(Y,W)$, we have
\begin{align*}
  d[X  | Z; Y | W]&= \bbH[X'-Y'|Z',W'] - \tfrac{1}{2} \bbH[X'|Z'] - \tfrac{1}{2}H[Y'|W'] \\
                       &\le \bbH[X'-Y']- \tfrac{1}{2} \bbH[X'|Z'] - \tfrac{1}{2}H[Y'|W'] \\
                       &= d[X';Y'] + \tfrac{1}{2}  \bbI[X' : Z'] + \tfrac{1}{2}  \bbI[Y' : W'].
\end{align*}
Here, in the middle step we used \Cref{cond-reduce}, and in the last step we used \Cref{ruz-dist-def} and \Cref{information-def}.
\end{proof}
lemma condRuzsaDist_le' [Countable T] {X : Ω → G} {Y : Ω' → G} {W : Ω' → T}
    [IsProbabilityMeasure μ] [IsProbabilityMeasure μ']
    (hX : Measurable X) (hY : Measurable Y) (hW : Measurable W)
    [FiniteRange X] [FiniteRange Y] [FiniteRange W] :
    d[X ; μ # Y|W ; μ'] ≤ d[X ; μ # Y ; μ'] + I[Y : W ; μ']/2 := by
  rw [← condRuzsaDist_of_const hX _ _ (0 : Fin 1)]
  refine (condRuzsaDist_le μ μ' hX measurable_const hY hW).trans ?_
  simp [mutualInfo_const hX (0 : Fin 1)]

variable (μ μ') in