\begin{lemma}\label{rho-increase-symmetrized}\lean{condRho_sum_le'}\leanok
  For independent random variables $Y_1,Y_2,Y_3,Y_4$ over $G$, define $T_1:=Y_1+Y_2,T_2:=Y_1+Y_3,T_3:=Y_2+Y_3$ and $S:=Y_1+Y_2+Y_3+Y_4$. Then
  $$\sum_{1 \leq i<j \leq 3} (\rho(T_i|T_j,S) + \rho(T_j|T_i,S) -  \frac{1}{2}\sum_{i} \rho(Y_i))\le \sum_{1\leq i < j \leq 4}d[Y_i;Y_j]$$
\end{lemma}
\begin{proof}\uses{rho-increase}\leanok
  Apply Lemma \ref{rho-increase} on $(Y_i,Y_j,Y_k,Y_4)$ for $(i,j,k)=(1,2,3),(2,3,1),(1,3,2)$, and take the sum.
\end{proof}
lemma condRho_sum_le' {Y₁ Y₂ Y₃ Y₄ : Ω → G}
      (hY₁ : Measurable Y₁) (hY₂ : Measurable Y₂) (hY₃ : Measurable Y₃) (hY₄ : Measurable Y₄)
      (h_indep : iIndepFun ![Y₁, Y₂, Y₃, Y₄]) (hA : A.Nonempty) :
    let S := Y₁ + Y₂ + Y₃ + Y₄
    let T₁ := Y₁ + Y₂
    let T₂ := Y₁ + Y₃
    let T₃ := Y₂ + Y₃
    ρ[T₁ | ⟨T₂, S⟩ # A] + ρ[T₂ | ⟨T₁, S⟩ # A] + ρ[T₁ | ⟨T₃, S⟩ # A] + ρ[T₃ | ⟨T₁, S⟩ # A]
      + ρ[T₂ | ⟨T₃, S⟩ # A] + ρ[T₃ | ⟨T₂, S⟩ # A]
      - 3 * (ρ[Y₁ # A] + ρ[Y₂ # A] + ρ[Y₃ # A] + ρ[Y₄ # A]) / 2 ≤
    d[Y₁ # Y₂] + d[Y₁ # Y₃] + d[Y₁ # Y₄] + d[Y₂ # Y₃] + d[Y₂ # Y₄] + d[Y₃ # Y₄] := by
  have K₁ := condRho_sum_le hY₁ hY₂ hY₃ hY₄ h_indep hA
  have K₂ := condRho_sum_le hY₂ hY₁ hY₃ hY₄ h_indep.reindex_four_bacd hA
  have Y₂₁ : Y₂ + Y₁ = Y₁ + Y₂ := by abel
  have dY₂₁ : d[Y₂ # Y₁] = d[Y₁ # Y₂] := rdist_symm
  rw [Y₂₁, dY₂₁] at K₂
  have K₃ := condRho_sum_le hY₃ hY₁ hY₂ hY₄ h_indep.reindex_four_cabd hA
  have Y₃₁ : Y₃ + Y₁ = Y₁ + Y₃ := by abel
  have Y₃₂ : Y₃ + Y₂ = Y₂ + Y₃ := by abel
  have S₃ : Y₁ + Y₃ + Y₂ + Y₄ = Y₁ + Y₂ + Y₃ + Y₄ := by abel
  have dY₃₁ : d[Y₃ # Y₁] = d[Y₁ # Y₃] := rdist_symm
  have dY₃₂ : d[Y₃ # Y₂] = d[Y₂ # Y₃] := rdist_symm
  rw [Y₃₁, Y₃₂, S₃, dY₃₁, dY₃₂] at K₃
  linarith

include hX₁ hX₂ hX₁' hX₂' h₁ h₂ h_indep h_min hη in