\begin{lemma}[Application of BSG]
  \label{lem:get-better}\lean{dist_of_U_add_le}\leanok
  Let $G$ be an abelian group, let $(T_1,T_2,T_3)$ be a $G^3$-valued random variable such that $T_1+T_2+T_3=0$ holds identically, and write
  \[
    \delta := \bbI[T_1 : T_2] + \bbI[T_1 : T_3] + \bbI[T_2 : T_3].
  \]
  Let $Y_1,\dots,Y_n$ be some further $G$-valued random variables and let $\alpha>0$ be a constant.
  Then there exists a random variable $U$ such that
  \begin{equation}
    \label{eq:get-better}
    d[U;U] + \alpha \sum_{i=1}^n d[Y_i;U] \leq \Bigl(2 + \frac{\alpha n}{2} \Bigr) \delta + \alpha \sum_{i=1}^n d[Y_i;T_2].
  \end{equation}
\end{lemma}
\begin{proof}\uses{entropic-bsg, relabeled-entropy, first-useful}
  We apply \Cref{entropic-bsg} with $X=T_1$ and $Y=T_2$.
  Since $T_1+T_2=-T_3$, we find that
  \begin{align}\nonumber
    \sum_{z} p_{T_3}(z) & d[T_1 \,|\, T_3 \mathop{=} z;T_2 \,|\, T_3 \mathop{=} z] \\ \nonumber
    &\leq  3 \bbI[T_1 : T_2] + 2 \bbH[T_3] - \bbH[T_1] - \bbH[T_2] \\
    &\ = \bbI[T_1 : T_2] + \bbI[T_1 : T_3] + \bbI[T_2 : T_3]
    = \delta,\label{514a}
  \end{align}
  where the last line follows from \Cref{relabeled-entropy} by observing
  \[
    \bbH[T_1,T_2] = \bbH[T_1,T_3] = \bbH[T_2,T_3] = \bbH[T_1,T_2,T_3]
  \]
  since any two of $T_1,T_2,T_3$ determine the third.

  By~\eqref{514a} and the triangle inequality,
  \[
    \sum_z p_{T_3}(z) d[T_2 \,|\, T_3 \mathop{=} z; T_2 \,|\, T_3\mathop{=}z] \leq 2 \delta
  \]
  and by \Cref{first-useful}, for each $Y_i$,
  \begin{align*}
    &\sum_z p_{T_3}(z) d[Y_i; T_2 \,|\, T_3 \mathop{=} z] \\
    &\qquad= d[Y_i; T_2 \,|\, T_3]
                                    \leq d[Y_i;T_2] + \frac12 \bbI[T_2 : T_3]
                                    \leq d[Y_i;T_2] + \frac{\delta}{2}.
  \end{align*}
  Hence,
  \begin{align*}
    &\sum_z p_{T_3}(z) \bigg( d[T_2 \,|\, T_3 \mathop{=} z; T_2 \,|\, T_3 \mathop{=} z] + \alpha \sum_{i=1}^n d[Y_i;T_2 \,|\, T_3 \mathop{=} z] \bigg) \\
    &\qquad \leq
    \Bigl(2 + \frac{\alpha n}{2} \Bigr) \delta + \alpha \sum_{i=1}^n d[Y_i; T_2],
  \end{align*}
  and the result follows by setting $U=(T_2 \,|\, T_3 \mathop{=} z)$ for some $z$ such that the quantity in parentheses on the left-hand side is at most the weighted average value.
\end{proof}
lemma dist_of_U_add_le {G: Type*} [MeasureableFinGroup G] {Ω: Type*} [MeasureSpace Ω] (T₁ T₂ T₃ : Ω → G) (hsum: T₁ + T₂ + T₃ = 0) (n:ℕ) {Ω': Fin n → Type*} (hΩ': ∀ i, MeasureSpace (Ω' i)) (Y: ∀ i, (Ω' i) → G) {α:ℝ} (hα: α > 0): ∃ (Ω'':Type*) (hΩ'': MeasureSpace Ω'') (U: Ω'' → G), d[U # U] + α * ∑ i, d[Y i # U] ≤ (2 + α * n / 2) * (I[T₁ : T₂] + I[T₁ : T₃] + I[T₂ : T₃]) + α * ∑ i, d[Y i # T₂] := sorry