\begin{lemma}\label{rho-increase}\lean{condRho_sum_le}\leanok
  For independent random variables $Y_1,Y_2,Y_3,Y_4$ over $G$, define $S:=Y_1+Y_2+Y_3+Y_4$, $T_1:=Y_1+Y_2$, $T_2:=Y_1+Y_3$. Then
  $$\rho(T_1|T_2,S)+\rho(T_2|T_1,S) - \frac{1}{2}\sum_{i} \rho(Y_i)\le \frac{1}{2}(d[Y_1;Y_2]+d[Y_3;Y_4]+d[Y_1;Y_3]+d[Y_2;Y_4]).$$
\end{lemma}
\begin{proof}\leanok\uses{rho-sums-sym, rho-cond, rho-cond-sym, rho-cond-relabeled, cor-fibre}
  Let $T_1':=Y_3+Y_4$, $T_2':=Y_2+Y_4$.
  First note that
  \begin{align*}
    \rho(T_1|T_2,S)
    &\le \rho(T_1|S) + \frac{1}{2}\bbI(T_1:T_2\mid S)  \\
    &\le \frac{1}{2}(\rho(T_1)+\rho(T_1'))+\frac{1}{2}(d[T_1;T_1']+\bbI(T_1:T_2\mid S)) \\
    &\le \frac{1}{4} \sum_{i} \rho(Y_i) +\frac{1}{4}(d[Y_1;Y_2]+d[Y_3;Y_4]) + \frac{1}{2}(d[T_1;T_1']+\bbI(T_1:T_2\mid S)).
  \end{align*}
  by \Cref{rho-cond}, \Cref{rho-cond-sym}, \Cref{rho-sums-sym} respectively.
  On the other hand, observe that
  \begin{align*}
    \rho(T_1|T_2,S)
    &=\rho(Y_1+Y_2|T_2,T_2') \\
    &\le \frac{1}{2}(\rho(Y_1|T_2)+\rho(Y_2|T_2'))+\frac{1}{2}(d[Y_1|T_2;Y_2|T_2'])  \\
    &\le \frac{1}{4} \sum_{i} \rho(Y_i) +\frac{1}{4}(d[Y_1;Y_3]+d[Y_2;Y_4]) + \frac{1}{2}(d[Y_1|T_2;Y_2|T_2']).
  \end{align*}
  by \Cref{rho-cond-relabeled}, \Cref{rho-sums-sym}, \Cref{rho-cond-sym} respectively.
  By replacing $(Y_1,Y_2,Y_3,Y_4)$ with $(Y_1,Y_3,Y_2,Y_4)$ in the above inequalities, one has
  $$\rho(T_2|T_1,S) \le \frac{1}{4} \sum_{i} \rho(Y_i) +\frac{1}{4}(d[Y_1;Y_3]+d[Y_2;Y_4]) + \frac{1}{2}(d[T_2;T_2']+\bbI(T_1:T_2\mid S))$$
  and
  $$\rho(T_2|T_1,S) \le \frac{1}{4} \sum_{i} \rho(Y_i) +\frac{1}{4}(d[Y_1;Y_2]+d[Y_3;Y_4]) + \frac{1}{2}(d[Y_1|T_1;Y_3|T_1']).$$
  Finally, take the sum of all four inequalities, apply \Cref{cor-fibre} on $(Y_1,Y_2,Y_3,Y_4)$ and $(Y_1,Y_3,Y_2,Y_4)$ to rewrite the sum of last terms in the four inequalities, and divide the result by $2$.
\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) :
    ρ[Y₁ + Y₂ | ⟨Y₁ + Y₃, Y₁ + Y₂ + Y₃ + Y₄⟩ # A] + ρ[Y₁ + Y₃ | ⟨Y₁ + Y₂, Y₁ + Y₂ + Y₃ + Y₄⟩ # A] -
      (ρ[Y₁ # A] + ρ[Y₂ # A] + ρ[Y₃ # A] + ρ[Y₄ # A]) / 2 ≤
        (d[Y₁ # Y₂] + d[Y₃ # Y₄] + d[Y₁ # Y₃] + d[Y₂ # Y₄]) / 2 := by
  set S := Y₁ + Y₂ + Y₃ + Y₄
  set T₁ := Y₁ + Y₂
  set T₂ := Y₁ + Y₃
  set T₁' := Y₃ + Y₄
  set T₂' := Y₂ + Y₄
  have J : ρ[T₁ | ⟨T₂, S⟩ # A] ≤
    (ρ[Y₁ # A] + ρ[Y₂ # A] + ρ[Y₃ # A] + ρ[Y₄ # A]) / 4
      + (d[Y₁ # Y₂] + d[Y₃ # Y₄] + d[Y₁ # Y₃] + d[Y₂ # Y₄]) / 8 + (d[Y₁ + Y₂ # Y₃ + Y₄]
        + I[Y₁ + Y₂ : Y₁ + Y₃ | Y₁ + Y₂ + Y₃ + Y₄] + d[Y₁ | Y₁ + Y₃ # Y₂ | Y₂ + Y₄]) / 4 :=
    new_gen_ineq hY₁ hY₂ hY₃ hY₄ h_indep hA
  have J' : ρ[T₂ | ⟨T₁, Y₁ + Y₃ + Y₂ + Y₄⟩ # A] ≤
    (ρ[Y₁ # A] + ρ[Y₃ # A] + ρ[Y₂ # A] + ρ[Y₄ # A]) / 4
      + (d[Y₁ # Y₃] + d[Y₂ # Y₄] + d[Y₁ # Y₂] + d[Y₃ # Y₄]) / 8 + (d[Y₁ + Y₃ # Y₂ + Y₄]
        + I[Y₁ + Y₃ : Y₁ + Y₂|Y₁ + Y₃ + Y₂ + Y₄] + d[Y₁ | Y₁ + Y₂ # Y₃ | Y₃ + Y₄]) / 4 :=
    new_gen_ineq hY₁ hY₃ hY₂ hY₄ h_indep.reindex_four_acbd hA
  have : Y₁ + Y₃ + Y₂ + Y₄ = S := by simp only [S]; abel
  rw [this] at J'
  have : d[Y₁ + Y₂ # Y₃ + Y₄] + I[Y₁ + Y₂ : Y₁ + Y₃ | Y₁ + Y₂ + Y₃ + Y₄]
    + d[Y₁ | Y₁ + Y₃ # Y₂ | Y₂ + Y₄] + d[Y₁ + Y₃ # Y₂ + Y₄]
    + I[Y₁ + Y₃ : Y₁ + Y₂|S] + d[Y₁ | Y₁ + Y₂ # Y₃ | Y₃ + Y₄]
      = (d[Y₁ # Y₂] + d[Y₃ # Y₄]) + (d[Y₁ # Y₃] + d[Y₂ # Y₄]) := by
    have K : Y₁ + Y₃ + Y₂ + Y₄ = S := by simp only [S]; abel
    have K' : I[Y₁ + Y₃ : Y₁ + Y₂|Y₁ + Y₂ + Y₃ + Y₄] = I[Y₁ + Y₃ : Y₃ + Y₄|Y₁ + Y₂ + Y₃ + Y₄] := by
      have : Measurable (Y₁ + Y₃) := by fun_prop
      rw [condMutualInfo_comm this (by fun_prop), condMutualInfo_comm this (by fun_prop)]
      have B := condMutualInfo_of_inj_map (X := Y₃ + Y₄) (Y := Y₁ + Y₃) (Z := Y₁ + Y₂ + Y₃ + Y₄)
        (by fun_prop) (by fun_prop) (by fun_prop) (fun a b ↦ a - b) (fun a ↦ sub_right_injective)
        (μ := ℙ)
      convert B with g
      simp
    have K'' : I[Y₁ + Y₂ : Y₁ + Y₃|Y₁ + Y₂ + Y₃ + Y₄] = I[Y₁ + Y₂ : Y₂ + Y₄|Y₁ + Y₂ + Y₃ + Y₄] := by
      have : Measurable (Y₁ + Y₂) := by fun_prop
      rw [condMutualInfo_comm this (by fun_prop), condMutualInfo_comm this (by fun_prop)]
      have B := condMutualInfo_of_inj_map (X := Y₂ + Y₄) (Y := Y₁ + Y₂) (Z := Y₁ + Y₂ + Y₃ + Y₄)
        (by fun_prop) (by fun_prop) (by fun_prop) (fun a b ↦ a - b) (fun a ↦ sub_right_injective)
        (μ := ℙ)
      convert B with g
      simp
      abel
    rw [sum_of_rdist_eq_char_2' Y₁ Y₂ Y₃ Y₄ h_indep hY₁ hY₂ hY₃ hY₄,
      sum_of_rdist_eq_char_2' Y₁ Y₃ Y₂ Y₄ h_indep.reindex_four_acbd hY₁ hY₃ hY₂ hY₄, K, K', K'']
    abel
  linarith

/-- 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]$$ -/