\begin{lemma}[Conditional rho and translation]\label{rho-cond-invariant}\lean{condRho_of_translate}\leanok
  For any $s\in G$, $\rho(X+s|Y)=\rho(X|Y)$.
\end{lemma}
\begin{proof}
  \uses{rho-cond-def,rho-invariant}\leanok
  Direct corollary of \Cref{rho-invariant}.
\end{proof}
/-- For any $s\in G$, $\rho(X+s|Y)=\rho(X|Y)$. -/
lemma condRho_of_translate {S : Type*}
    {Y : Ω → S} (hX : Measurable X) (hA : A.Nonempty) (s : G) :
    ρ[fun ω ↦ X ω + s | Y ; μ # A] = ρ[X | Y ; μ # A] := by
  simp [condRho, rho_of_translate hX hA]

omit [Fintype G] [DiscreteMeasurableSpace G] in
variable (X) in