\begin{lemma}\label{rho-BSG-triplet}\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]\le 3\bbI[T_1:T_2] + (2\bbH[T_3]-\bbH[T_1]-\bbH[T_2])+ \eta(\rho(T_1|T_3)+\rho(T_2|T_3)-\rho(X_1)-\rho(X_2)).$$
\end{lemma}
\begin{proof}\leanok\uses{entropic-bsg,phi-min-def}
  Conditioned on every $T_3=t$, $d[X_1;X_2]\le d[T_1|T_3=t;T_2|T_3=t]+\eta(\rho(T_1|T_3=t)+\rho(T_2|T_3=t)-\rho(X_1)-\rho(X_2))$ by \Cref{phi-min-def}. Then take the weighted average with weight $\mathbf{P}(T_3=t)$ and then apply \Cref{entropic-bsg} to bound the RHS.
\end{proof}
lemma dist_le_of_sum_zero {Ω' : Type*} [MeasurableSpace Ω'] {μ : Measure Ω'}
    [IsProbabilityMeasure μ] {T₁ T₂ T₃ : Ω' → G}
    (hsum : T₁ + T₂ + T₃ = 0) (hT₁ : Measurable T₁) (hT₂ : Measurable T₂) (hT₃ : Measurable T₃) :
    k ≤ 3 * I[T₁ : T₂ ; μ] + (2 * H[T₃ ; μ] - H[T₁ ; μ] - H[T₂ ; μ])
      + η * (ρ[T₁ | T₃ ; μ # A] + ρ[T₂ | T₃ ; μ #  A] - ρ[X₁ # A] - ρ[X₂ # A]) := by
  let _ : MeasureSpace Ω' := ⟨μ⟩
  have : μ = ℙ := rfl
  simp only [this]
  have : ∑ t, (ℙ (T₃ ⁻¹' {t})).toReal * d[ X₁ # X₂ ] ≤ ∑ t, (ℙ (T₃ ⁻¹' {t})).toReal *
      (d[T₁ ; ℙ[|T₃ ← t] # T₂ ; ℙ[|T₃ ← t]]
        + η * (ρ[T₁ ; ℙ[|T₃ ← t] # A] - ρ[X₁ # A]) + η * (ρ[T₂ ; ℙ[|T₃ ← t] # A] - ρ[X₂ # A])) := by
    apply Finset.sum_le_sum (fun t ht ↦ ?_)
    rcases eq_or_ne (ℙ (T₃ ⁻¹' {t})) 0 with h't | h't
    · simp [h't]
    have : IsProbabilityMeasure (ℙ[|T₃ ← t]) := cond_isProbabilityMeasure h't
    gcongr
    exact le_rdist_of_phiMinimizes' h_min hT₁ hT₂
  have : k ≤ ∑ x : G, (ℙ (T₃ ⁻¹' {x})).toReal * d[T₁ ; ℙ[|T₃ ← x] # T₂ ; ℙ[|T₃ ← x]] +
      η * (ρ[T₁ | T₃ # A] - ρ[X₁ # A]) + η * (ρ[T₂ | T₃ # A] - ρ[X₂ # A]) := by
    have S : ∑ i : G, (ℙ (T₃ ⁻¹' {i})).toReal = 1 := by
      have : IsProbabilityMeasure (Measure.map T₃ ℙ) := isProbabilityMeasure_map hT₃.aemeasurable
      simp [← Measure.map_apply hT₃ (measurableSet_singleton _)]
    simp_rw [← Finset.sum_mul, S, mul_add, Finset.sum_add_distrib, ← mul_assoc, mul_comm _ η,
      mul_assoc, ← Finset.mul_sum, mul_sub, Finset.sum_sub_distrib, mul_sub,
      ← Finset.sum_mul, S] at this
    simpa [mul_sub, condRho, tsum_fintype] using this
  have J : ∑ x : G, (ℙ (T₃ ⁻¹' {x})).toReal * d[T₁ ; ℙ[|T₃ ← x] # T₂ ; ℙ[|T₃ ← x]]
      ≤ 3 * I[T₁ : T₂] + 2 * H[T₃] - H[T₁] - H[T₂] := by
    have h2T₃ : T₃ = T₁ + T₂ :=
      calc T₃ = T₁ + T₂ + T₃ - T₃ := by rw [hsum, _root_.zero_sub]; simp [ZModModule.neg_eq_self]
        _ = T₁ + T₂ := by rw [add_sub_cancel_right]
    subst h2T₃
    have := ent_bsg hT₁ hT₂ (μ := ℙ)
    simp_rw [integral_fintype _ Integrable.of_finite,
      Measure.map_apply hT₃ (measurableSet_singleton _)] at this
    exact this
  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]\le 3\bbI[T_1:T_2\mid T_3] + (2\bbH[T_3]-\bbH[T_1]-\bbH[T_2])+ \eta(\rho(T_1|T_3)+\rho(T_2|T_3)-\rho(X_1)-\rho(X_2)).$$ -/