\begin{lemma}\label{rho-BSG-triplet-symmetrized}\lean{dist_le_of_sum_zero'}\leanok
  If $G$-valued random variables $T_1,T_2,T_3$ satisfy $T_1+T_2+T_3=0$, then
  $$d[X_1;X_2] \leq  \sum_{1 \leq i<j \leq 3} \bbI[T_i:T_j] + \frac{\eta}{3}   \sum_{1 \leq i<j \leq 3} (\rho(T_i|T_j) + \rho(T_j|T_i) -\rho(X_1)-\rho(X_2))$$
\end{lemma}
\begin{proof}\leanok\uses{rho-BSG-triplet}
  Take the average of \Cref{rho-BSG-triplet} over all $6$ permutations of $T_1,T_2,T_3$.
\end{proof}
lemma dist_le_of_sum_zero' {Ω' : Type*} [MeasureSpace Ω']
    [IsProbabilityMeasure (ℙ : Measure Ω')] {T₁ T₂ T₃ : Ω' → G} (hsum : T₁ + T₂ + T₃ = 0)
    (hT₁ : Measurable T₁) (hT₂ : Measurable T₂) (hT₃ : Measurable T₃) :
    k ≤ I[T₁ : T₂] + I[T₁ : T₃] + I[T₂ : T₃]
      + (η / 3) * ((ρ[T₁ | T₂ # A] + ρ[T₂ | T₁ # A] - ρ[X₁ # A] - ρ[X₂ # A])
                 + (ρ[T₁ | T₃ # A] + ρ[T₃ | T₁ # A] - ρ[X₁ # A] - ρ[X₂ # A])
                 + (ρ[T₂ | T₃ # A] + ρ[T₃ | T₂ # A] - ρ[X₁ # A] - ρ[X₂ # A])) := by
  have := dist_le_of_sum_zero h_min hsum hT₁ hT₂ hT₃ (μ := ℙ)
  have : T₁ + T₃ + T₂ = 0 := by convert hsum using 1; abel
  have := dist_le_of_sum_zero h_min this hT₁ hT₃ hT₂ (μ := ℙ)
  have : T₂ + T₃ + T₁ = 0 := by convert hsum using 1; abel
  have := dist_le_of_sum_zero h_min this hT₂ hT₃ hT₁ (μ := ℙ)
  linarith

include h_min in
omit [IsProbabilityMeasure (ℙ : Measure Ω)] in
/-- If $G$-valued random variables $T_1,T_2,T_3$ satisfy $T_1+T_2+T_3=0$, then
  $$d[X_1;X_2] \leq \sum_{1 \leq i < j \leq 3} \bbI[T_i:T_j]
  + \frac{\eta}{3} \sum_{1 \leq i < j \leq 3} (\rho(T_i|T_j) + \rho(T_j|T_i) -\rho(X_1)-\rho(X_2))$$
-/