\begin{lemma}[Copy preserves Ruzsa distance]\label{ruz-copy}
  \uses{ruz-dist-def}
  \lean{ProbabilityTheory.IdentDistrib.rdist_eq}\leanok
  If $X',Y'$ are copies of $X,Y$ respectively then $d[X';Y']=d[X ;Y]$.
\end{lemma}
\begin{proof} \uses{copy-ent}\leanok Immediate from Definitions \ref{ruz-dist-def} and \Cref{copy-ent}.
\end{proof}
/-- If `X', Y'` are copies of `X, Y` respectively then `d[X' ; Y'] = d[X ; Y]`. -/
lemma ProbabilityTheory.IdentDistrib.rdist_eq {X' : Ω'' → G} {Y' : Ω''' → G}
    (hX : IdentDistrib X X' μ μ'') (hY : IdentDistrib Y Y' μ' μ''') :
    d[X ; μ # Y ; μ'] = d[X' ; μ'' # Y' ; μ'''] := by
  simp [rdist, hX.map_eq, hY.map_eq, hX.entropy_eq, hY.entropy_eq]