\begin{lemma}[Rho and conditioning]\label{rho-cond}\lean{condRhoMinus_le, condRhoPlus_le, condRho_le}\leanok  If $X,Z$ are defined on the same space, one has
  $$ \rho^-(X|Z) \leq \rho^-(X) + \bbH[X] - \bbH[X|Z]$$
  $$ \rho^+(X|Z) \leq \rho^+(X)$$
and
  $$ \rho(X|Z) \leq \rho(X) + \frac{1}{2}( \bbH[X] - \bbH[X|Z] ).$$
\end{lemma}
\begin{proof}\leanok
  \uses{kl-cond}
  The first inequality follows from \Cref{kl-cond}. The second and third inequalities are direct corollaries of the first.
\end{proof}
/-- $$ \rho^+(X|Z) \leq \rho^+(X)$$ -/
lemma condRhoPlus_le [IsProbabilityMeasure μ] {S : Type*} [MeasurableSpace S]
    [Fintype S] [MeasurableSingletonClass S]
    {Z : Ω → S} (hX : Measurable X) (hZ : Measurable Z) (hA : A.Nonempty) :
    ρ⁺[X | Z ; μ # A] ≤ ρ⁺[X ; μ # A] := by
  have : IsProbabilityMeasure (Measure.map Z μ) := isProbabilityMeasure_map hZ.aemeasurable
  have I₁ := condRhoMinus_le hX hZ hA (μ := μ)
  simp_rw [condRhoPlus, rhoPlus, tsum_fintype]
  simp only [Nat.card_eq_fintype_card, Fintype.card_coe, mul_sub, mul_add, Finset.sum_sub_distrib,
    Finset.sum_add_distrib, tsub_le_iff_right]
  rw [← Finset.sum_mul, ← tsum_fintype, ← condRhoMinus, ← condEntropy_eq_sum_fintype _ _ _ hZ]
  simp_rw [← Measure.map_apply hZ (measurableSet_singleton _)]
  simp only [Finset.sum_toReal_measure_singleton, Finset.coe_univ, measure_univ, ENNReal.one_toReal,
    one_mul, sub_add_cancel, ge_iff_le]
  linarith

omit [Fintype G] [DiscreteMeasurableSpace G] in