\begin{lemma}[Multidistance chain rule]\label{multidist-chain-rule}\lean{multiDist_chainRule}\uses{multidist-def}\leanok  Let $\pi \colon G \to H$ be a homomorphism of abelian groups and let $X_{[m]}$ be a tuple of jointly independent $G$-valued random variables.  Then $D[X_{[m]}]$ is equal to
  \begin{equation}
      D[ X_{[m]} | \pi(X_{[m]}) ]  +D[ \pi(X_{[m]}) ]  + \bbI[ \sum_{i=1}^m X_i  : \pi(X_{[m]}) \; \big| \; \pi\bigl(\sum_{i=1}^m X_i\bigr) ]
    \label{chain-eq}
  \end{equation}
  where $\pi(X_{[m]}) := (\pi(X_i))_{1 \leq i \leq m}$.
  \end{lemma}
\begin{proof}\uses{conditional-mutual-alt, relabeled-entropy, chain-rule}\leanok For notational brevity during this proof, write $S := \sum_{i=1}^m X_i$.

    From \Cref{conditional-mutual-alt} and \Cref{relabeled-entropy}, noting that $\pi(S)$ is determined both by $S$ and by $\pi(X_{[m]})$, we have
  \begin{equation*}
   \bbI[S:\pi(X_{[m]})|\pi(S)] = \bbH[S]+\bbH[\pi(X_{[m]})]-\bbH[S,\pi(X_{[m]})]-\bbH[\pi(S)],
  \end{equation*}
  and by \Cref{chain-rule} the right-hand side is equal to
  \begin{equation*}
  \bbH[S]-\bbH[S|\pi(X_{[m]})]-\bbH[\pi(S)].
  \end{equation*}
  Therefore,
  \begin{equation}\label{chain-1}
  \bbH[S]=\bbH[S|\pi(X_{[m]})]+\bbH[\pi(S)]+\bbI[S:\pi(X_{[m]})|\pi(S)]. \end{equation}
  From a further application of \Cref{chain-rule} and \Cref{relabeled-entropy} we have
  \begin{equation}\label{chain-2}
    \bbH[X_i] = \bbH[X_i \, | \, \pi(X_i)] + \bbH[\pi(X_i)]
  \end{equation}
  for all $1 \leq i \leq m$.  Averaging~\eqref{chain-2} in $i$ and subtracting this from~\eqref{chain-1}, we obtain the claim from \Cref{multidist-def}.
  \end{proof}
lemma multiDist_chainRule {G H : Type*} [hG : MeasurableSpace G] [MeasurableSingletonClass G]
    [AddCommGroup G] [Fintype G] [hH : MeasurableSpace H]
    [MeasurableSingletonClass H] [AddCommGroup H]
    [Fintype H] (π : G →+ H) {m : ℕ} {Ω : Type*} (hΩ : MeasureSpace Ω)
    {X : Fin m → Ω → G} (hmes : ∀ i, Measurable (X i))
    (h_indep : iIndepFun X) :
    D[X; fun _ ↦ hΩ] = D[X | fun i ↦ π ∘ X i; fun _ ↦ hΩ]
      + D[fun i ↦ π ∘ X i; fun _ ↦ hΩ]
      + I[∑ i, X i : fun ω ↦ (fun i ↦ π (X i ω)) | π ∘ (∑ i, X i)] := by
  have : IsProbabilityMeasure (ℙ : Measure Ω) := h_indep.isProbabilityMeasure
  set S := ∑ i, X i
  set piX := fun ω ↦ (fun i ↦ π (X i ω))
  set avg_HX := (∑ i, H[X i]) / m
  set avg_HpiX := (∑ i, H[π ∘ X i])/m
  set avg_HXpiX := (∑ i, H[X i | π ∘ X i])/m
  have hSmes : Measurable S := by fun_prop
  have hpiXmes : Measurable piX := by
    rw [measurable_pi_iff]
    intro i
    exact Measurable.comp .of_discrete (hmes i)

  have eq1 : I[S : piX | π ∘ S] = H[S | π ∘ S] + H[piX | π ∘ S] - H[⟨S, piX⟩ | π ∘ S] := by
    rw [condMutualInfo_eq hSmes hpiXmes (Measurable.comp .of_discrete hSmes)]

  have eq1a : H[S | π ∘ S] = H[S] - H[π ∘ S] :=
    condEntropy_comp_self hSmes .of_discrete

  have eq1b : H[piX | π ∘ S] = H[piX] - H[π ∘ S] := by
    set g := fun (y : Fin m → H) ↦ ∑ i, y i
    have : π ∘ S = g ∘ piX := by
      ext x
      simp only [comp_apply, Finset.sum_apply, _root_.map_sum, S, g, piX]
    rw [this]
    exact condEntropy_comp_self hpiXmes .of_discrete

  have eq1c : H[⟨S, piX⟩ | π ∘ S] = H[⟨S, piX⟩] - H[π ∘ S] := by
    set g := fun (x : G × (Fin m → H)) ↦ π x.1
    have : π ∘ S = g ∘ ⟨S, piX⟩ := by
      ext x
      simp only [comp_apply, Finset.sum_apply, _root_.map_sum, S, g, piX]
    rw [this]
    apply condEntropy_comp_self (Measurable.prodMk hSmes hpiXmes) .of_discrete

  have eq2 : H[⟨S, piX⟩] = H[piX] + H[S | piX] := chain_rule _ hSmes hpiXmes

  have eq3 : D[X; fun _ ↦ hΩ] = H[S] - avg_HX := multiDist_indep _ _ h_indep

  have eq4 : D[X | fun i ↦ π ∘ X i; fun _ ↦ hΩ] = H[S | piX] - avg_HXpiX := by
    dsimp [S, piX]
    convert condMultiDist_eq (S := H) hmes _ _
    . exact Fintype.sum_apply _ _
    . intro i
      exact Measurable.comp .of_discrete (hmes i)
    set g : G → G × H := fun x ↦ ⟨x, π x⟩
    change iIndepFun (fun i ↦ g ∘ X i) ℙ
    exact h_indep.comp _ fun _ ↦ .of_discrete

  have eq5: D[fun i ↦ π ∘ X i; fun _ ↦ hΩ] = H[π ∘ S] - avg_HpiX := by
    convert multiDist_indep _ (fun i ↦ π ∘ X i) _
    . ext _
      simp only [comp_apply, Finset.sum_apply, _root_.map_sum, S]
    apply iIndepFun.comp h_indep
    exact fun _ ↦ .of_discrete

  have eq6: avg_HX = avg_HpiX + avg_HXpiX := by
    dsimp [avg_HX, avg_HpiX, avg_HXpiX]
    rw [← add_div, ← Finset.sum_add_distrib]
    congr with i
    rw [condEntropy_comp_self (hmes i) .of_discrete]
    abel

  linarith only [eq1, eq1a, eq1b, eq1c, eq2, eq3, eq4, eq5, eq6]

/-- Let `π : G → H` be a homomorphism of abelian groups. Let `I` be a finite index set and let
`X_[m]` be a tuple of `G`-valued random variables. Let `Y_[m]` be another tuple of random variables
(not necessarily `G`-valued). Suppose that the pairs `(X_i, Y_i)` are jointly independent of one
another (but `X_i` need not be independent of `Y_i`). Then
`D[X_[m] | Y_[m]] = D[X_[m] ,|, π(X_[m]), Y_[m]] + D[π(X_[m]) ,| , Y_[m]]`
`+ I[∑ i, X_i : π(X_[m]) ; | ; π(∑ i, X_i), Y_[m]]`. -/