\begin{corollary}\label{fibring-ineq}
 \lean{rdist_of_hom_le} \leanok
If $\pi:G\to H$ is a homomorphism of additive groups and $X,Y$ are $G$-valued random variables then
\[d[X;Y]\geq d[\pi(X);\pi(Y)].\]
\end{corollary}
\begin{proof}
\uses{fibring-ident, ruzsa-nonneg}\leanok
By \Cref{fibring-ident} and the nonnegativity of conditional Ruzsa distance (from \Cref{ruzsa-nonneg}) we have
\[d[X;Y]\geq d[\pi(X);\pi(Y)]+d[X\mid \pi(X);Y\mid \pi(Y)].\]
The inequality follows from $d[X\mid \pi(X);Y\mid \pi(Y)]\geq 0$ (\Cref{ruzsa-nonneg}).
\end{proof}
/-- \[d[X;Y]\geq d[\pi(X);\pi(Y)].\] -/
lemma rdist_of_hom_le {Z_1 : Ω → H} {Z_2 : Ω' → H}
    (h1 : Measurable Z_1) (h2 : Measurable Z_2) [FiniteRange Z_1] [FiniteRange Z_2] :
    d[π ∘ Z_1; μ # π ∘ Z_2; μ'] ≤ d[Z_1; μ # Z_2; μ'] := by
  apply le_trans _ (rdist_le_sum_fibre π h1 h2 (μ := μ) (μ' := μ'))
  rw [le_add_iff_nonneg_right]
  exact condRuzsaDist_nonneg h1 (by fun_prop) h2 (by fun_prop)

end GeneralFibring

variable {G : Type*} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G]
  [MeasurableSingletonClass G]
variable {Ω : Type*} [mΩ : MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]