\begin{lemma}[Multidistance of copy]\label{multidist-copy}\lean{multiDist_copy}\leanok  If $X_{[m]} = (X_i)_{1 \leq i \leq m}$ and $Y_{[m]} = (Y_i)_{1 \leq i \leq m}$ are such that $X_i$ and $Y_i$ have the same distribution for each $i$, then $D[X_{[m]}] = D[Y_{[m]}]$.
\end{lemma}
\begin{proof}\uses{multidist-def}\leanok Clear from Lemma \ref{copy-ent}.
\end{proof}
/-- If `X_i` has the same distribution as `Y_i` for each `i`, then `D[X_[m]] = D[Y_[m]]`. -/
lemma multiDist_copy {m : ℕ} {Ω : Fin m → Type*} {Ω' : Fin m → Type*}
    (hΩ : ∀ i, MeasureSpace (Ω i)) (hΩ': ∀ i, MeasureSpace (Ω' i))
    (X : ∀ i, (Ω i) → G) (X' : ∀ i, (Ω' i) → G)
    (hident : ∀ i, IdentDistrib (X i) (X' i)) :
    D[X ; hΩ] = D[X' ; hΩ'] := by
  simp_rw [multiDist, IdentDistrib.entropy_eq (hident _), (hident _).map_eq]