\begin{corollary}\label{cor-multid}\lean{cor_multiDist_chainRule}\leanok Let $G$ be an abelian group and let $m \geq 2$.  Suppose that $X_{i,j}$, $1 \leq i, j \leq m$, are independent $G$-valued random variables.
    Then
    \begin{align*}
      &\bbI[ \bigl(\sum_{i=1}^m X_{i,j}\bigr)_{j =1}^{m} : \bigl(\sum_{j=1}^m X_{i,j}\bigr)_{i = 1}^m \; \big| \; \sum_{i=1}^m \sum_{j = 1}^m  X_{i,j} ] \\
      &\quad \leq \sum_{j=1}^{m-1} \Bigl(D[(X_{i, j})_{i = 1}^m] - D[ (X_{i, j})_{i = 1}^m  \; \big| \; (X_{i,j} + \cdots + X_{i,m})_{i =1}^m ]\Bigr) \\ & \qquad\qquad\qquad\qquad +  D[(X_{i,m})_{i=1}^m] - D[ \bigl(\sum_{j=1}^m X_{i,j}\bigr)_{i=1}^m ],
    \end{align*}
  where all the multidistances here involve the indexing set $\{1,\dots, m\}$.
  \end{corollary}
\begin{proof}\uses{multidist-chain-rule-iter, add-entropy}
    In \Cref{multidist-chain-rule-iter} we take $G_d := G^d$ with the maps $\pi_d \colon G^m \to G^d$ for $d=1,\dots,m$ defined by
  \[
    \pi_d(x_1,\dots,x_m) := (x_1,\dots,x_{d-1}, x_d + \cdots + x_m)
  \]
  with $\pi_0=0$. Since $\pi_{d-1}(x)$ can be obtained from $\pi_{d}(x)$ by applying a homomorphism, we obtain a sequence of the form~\eqref{g-seq}.

  Now we apply \Cref{multidist-chain-rule-iter} with $I = \{1,\dots, m\}$ and $X_i :=  (X_{i,j})_{j = 1}^m$.  Using joint independence and \Cref{add-entropy}, we find that
  \[
    D[ X_{[m]} ] = \sum_{j=1}^m D[ (X_{i,j})_{1 \leq i \leq m} ].
  \]
  On the other hand, for $1 \leq j \leq m-1$, we see that once $\pi_{j}(X_i)$ is fixed, $\pi_{j+1}(X_i)$ is determined by $X_{i, j}$ and vice versa, so
  \[
    D[ \pi_{j+1}(X_{[m]}) \; | \; \pi_{j}(X_{[m]}) ] = D[ (X_{i, j})_{1 \leq i \leq m} \; | \; \pi_{j}(X_{[m]} )].
  \]
  Since the $X_{i,j}$ are jointly independent, we may further simplify:
  \[
    D[ (X_{i, j})_{1 \leq i \leq m} \; | \; \pi_{j}(X_{[m]})] = D[ (X_{i,j})_{1 \leq i \leq m} \; | \; ( X_{i, j} + \cdots + X_{i, m})_{1 \leq i \leq m} ].
  \]
  Putting all this into the conclusion of \Cref{multidist-chain-rule-iter}, we obtain
  \[
    \sum_{j=1}^{m} D[ (X_{i,j})_{1 \leq i \leq m} ]
    \geq
    \begin{aligned}[t]
    &\sum_{j=1}^{m-1} D[ (X_{i,j})_{1 \leq i \leq m} \; | \; (X_{i,j} + \cdots + X_{i,m})_{1 \leq i \leq m} ] \\
    &\!\!\!+
    D[ \bigl(\sum_{j=1}^m X_{i,j}\bigr)_{1 \leq i \leq m}] \\
    &\!\!\!+\bbI[  \bigl(\sum_{i=1}^m X_{i,j}\bigr)_{j =1}^{m} : \bigl(\sum_{j=1}^m X_{i,j}\bigr)_{i = 1}^m \; \big| \; \sum_{i=1}^m \sum_{j = 1}^m  X_{i,j} ]
    \end{aligned}
  \]
  and the claim follows by rearranging.
\end{proof}
lemma cor_multiDist_chainRule [Fintype G] {m:ℕ} (hm: m ≥ 1) {Ω : Type*} (hΩ : MeasureSpace Ω)
    (X : Fin (m + 1) × Fin (m + 1) → Ω → G) (h_indep : iIndepFun X) :
    I[fun ω ↦ (fun j ↦ ∑ i, X (i, j) ω) : fun ω ↦ (fun i ↦ ∑ j, X (i, j) ω) | ∑ p, X p]
      ≤ ∑ j, (D[fun i ↦ X (i, j); fun _ ↦ hΩ] - D[fun i ↦ X (i, j) |
        fun i ↦ ∑ k ∈ Finset.Ici j, X (i, k); fun _ ↦ hΩ]) + D[fun i ↦ X (i, m); fun _ ↦ hΩ]
         - D[fun i ↦ ∑ j, X (i, j); fun _ ↦ hΩ] := by sorry

end multiDistance_chainRule