\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} {Z : Ω → S} {Y : Ω' → G} {W : Ω' → T}
    [IsProbabilityMeasure μ] [IsProbabilityMeasure μ']
    (hX : Measurable X) (hZ : Measurable Z) (hY : Measurable Y) (hW : Measurable W)
    [FiniteRange X] [FiniteRange Z] [FiniteRange Y] [FiniteRange W] :
      d[X | Z ; μ # Y|W ; μ'] ≤ d[X ; μ # Y ; μ'] + I[X : Z ; μ]/2 + I[Y : W ; μ']/2 := by
  have hXZ : Measurable (⟨X, Z⟩ : Ω → G × S):= hX.prodMk hZ
  have hYW : Measurable (⟨Y, W⟩ : Ω' → G × T):= hY.prodMk hW
  obtain ⟨ν, XZ', YW', _, hXZ', hYW', hind, hIdXZ, hIdYW, _, _⟩ :=
    independent_copies_finiteRange hXZ hYW μ μ'
  let X' := Prod.fst ∘ XZ'
  let Z' := Prod.snd ∘ XZ'
  let Y' := Prod.fst ∘ YW'
  let W' := Prod.snd ∘ YW'
  have hX' : Measurable X' := hXZ'.fst
  have hZ' : Measurable Z' := hXZ'.snd
  have hY' : Measurable Y' := hYW'.fst
  have hW' : Measurable W' := hYW'.snd
  have : FiniteRange W' := instFiniteRangeComp ..
  have : FiniteRange X' := instFiniteRangeComp ..
  have : FiniteRange Y' := instFiniteRangeComp ..
  have : FiniteRange Z' := instFiniteRangeComp ..
  have hind' : IndepFun X' Y' ν := hind.comp measurable_fst measurable_fst
  rw [show XZ' = ⟨X', Z'⟩ by rfl] at hIdXZ hind
  rw [show YW' = ⟨Y', W'⟩ by rfl] at hIdYW hind
  rw [← condRuzsaDist_of_copy hX' hZ' hY' hW' hX hZ hY hW hIdXZ hIdYW,
    condRuzsaDist_of_indep hX' hZ' hY' hW' _ hind]
  have hIdX : IdentDistrib X X' μ ν := hIdXZ.symm.comp measurable_fst
  have hIdY : IdentDistrib Y Y' μ' ν := hIdYW.symm.comp measurable_fst
  rw [hIdX.rdist_eq hIdY, hIdXZ.symm.mutualInfo_eq, hIdYW.symm.mutualInfo_eq,
    hind'.rdist_eq hX' hY', mutualInfo_eq_entropy_sub_condEntropy hX' hZ',
    mutualInfo_eq_entropy_sub_condEntropy hY' hW']
  have h := condEntropy_le_entropy ν (X := X' - Y') (hX'.sub hY') (hZ'.prodMk hW')
  linarith [h, entropy_nonneg Z' ν, entropy_nonneg W' ν]

variable (μ μ') in