\begin{lemma}[Rho and conditioning, symmetrized]\label{rho-cond-sym}\lean{condRho_of_sum_le}\leanok
  If $X,Y$ are independent, then
  $$ \rho(X | X+Y) \leq \frac{1}{2}(\rho(X)+\rho(Y) + d[X;Y]).$$
\end{lemma}
\begin{proof}\leanok
  \uses{rho-invariant,rho-cond}
  First apply \Cref{rho-cond} to get $\rho(X|X+Y)\le \rho(X) + \frac{1}{2}(\bbH[X+Y]-\bbH[Y])$, and $\rho(Y|X+Y)\le \rho(Y)+\frac{1}{2}(\bbH[X+Y]-\bbH[X])$. Then apply \Cref{rho-invariant} to get $\rho(Y|X+Y)=\rho(X|X+Y)$ and take the average of the two inequalities.
\end{proof}
lemma condRho_of_sum_le [IsProbabilityMeasure μ]
    (hX : Measurable X) (hY : Measurable Y) (hA : A.Nonempty) (h_indep : IndepFun X Y μ) :
    ρ[X | X + Y ; μ # A] ≤ (ρ[X ; μ # A] + ρ[Y ; μ # A] + d[ X ; μ # Y ; μ ]) / 2 := by
  have I : ρ[X | X + Y ; μ # A] ≤ ρ[X ; μ # A] + (H[X ; μ] - H[X | X + Y ; μ]) / 2 :=
    condRho_le hX (by fun_prop) hA
  have I' : H[X ; μ] - H[X | X + Y ; μ] = H[X + Y ; μ] - H[Y ; μ] := by
    rw [ProbabilityTheory.chain_rule'' _ hX (by fun_prop), entropy_add_right hX hY,
      IndepFun.entropy_pair_eq_add hX hY h_indep]
    abel
  have J : ρ[Y | Y + X ; μ # A] ≤ ρ[Y ; μ # A] + (H[Y ; μ] - H[Y | Y + X ; μ]) / 2 :=
    condRho_le hY (by fun_prop) hA
  have J' : H[Y ; μ] - H[Y | Y + X ; μ] = H[Y + X ; μ] - H[X ; μ] := by
    rw [ProbabilityTheory.chain_rule'' _ hY (by fun_prop), entropy_add_right hY hX,
      IndepFun.entropy_pair_eq_add hY hX h_indep.symm]
    abel
  have : Y + X = X + Y := by abel
  simp only [this] at J J'
  have : ρ[X | X + Y ; μ # A] = ρ[Y | X + Y ; μ # A] := by
    simp only [condRho]
    congr with s
    congr 1
    have : ρ[X ; μ[|(X + Y) ⁻¹' {s}] # A] = ρ[fun ω ↦ X ω + s ; μ[|(X + Y) ⁻¹' {s}] # A] := by
      rw [rho_of_translate hX hA]
    rw [this]
    apply rho_eq_of_identDistrib
    apply IdentDistrib.of_ae_eq (by fun_prop)
    have : MeasurableSet ((X + Y) ⁻¹' {s}) := by
      have : Measurable (X + Y) := by fun_prop
      exact this (measurableSet_singleton _)
    filter_upwards [ae_cond_mem this] with a ha
    simp only [mem_preimage, Pi.add_apply, mem_singleton_iff] at ha
    rw [← ha]
    nth_rewrite 1 [← ZModModule.neg_eq_self (X a)]
    abel
  have : X - Y = X + Y := ZModModule.sub_eq_add _ _
  rw [h_indep.rdist_eq hX hY, sub_eq_add_neg, this]
  linarith

end