\begin{lemma}\label{multidist-chain-rule-iter}\lean{iter_multiDist_chainRule,iter_multiDist_chainRule'}\leanok  Let $m$ be a positive integer.
    Suppose one has a sequence
    \begin{equation}\label{g-seq}
      G_m \to G_{m-1} \to \dots \to G_1 \to G_0 = \{0\}
    \end{equation}
    of homomorphisms between abelian groups $G_0,\dots,G_m$, and for each $d=0,\dots,m$, let $\pi_d : G_m \to G_d$ be the homomorphism from $G_m$ to $G_d$ arising from this sequence by composition (so for instance $\pi_m$ is the identity homomorphism and $\pi_0$ is the zero homomorphism).
    Let $X_{[m]} = (X_i)_{1 \leq i \leq m}$ be a jointly independent tuple of $G_m$-valued random variables.
    Then
    \begin{equation}
      \begin{split}
        D[ X_{[m]} ] &=  \sum_{d=1}^m D[ \pi_d(X_{[m]}) \,|\, \pi_{d-1}(X_{[m]})] \\
         &\quad + \sum_{d=1}^{m-1} \bbI[ \sum_i X_i : \pi_d(X_{[m]}) \; \big| \; \pi_d\big(\sum_i X_i\big), \pi_{d-1}(X_{[m]}) ].
      \end{split}\label{chain-eq-cond'}
    \end{equation}
    In particular, by \Cref{conditional-nonneg},
    \begin{align}\nonumber
        D[ X_{[m]} ] \geq  & \sum_{d=1}^m D[ \pi_d(X_{[m]})|\pi_{d-1}(X_{[m]}) ] \\
         & + \bbI[ \sum_i X_i : \pi_1(X_{[m]}) \; \big| \; \pi_1\bigl(\sum_i X_i\bigr) ].\label{chain-eq-cond''}
    \end{align}
  \end{lemma}
\begin{proof}\uses{multidist-chain-rule-cond, conditional-nonneg}\leanok
  From \Cref{multidist-chain-rule-cond} (taking $Y_{[m]} = \pi_{d-1}(X_{[m]})$ and $\pi = \pi_d$ there, and noting that $\pi_d(X_{[m]})$ determines $Y_{[m]}$) we have
  \begin{align*}
    D[ X_{[m]} \,|\, \pi_{d-1}(X_{[m]}) ] &=  D[ X_{[m]} \,|\, \pi_d(X_{[m]}) ] + D[  \pi_d(X_{[m]})\,|\,\pi_{d-1}(X_{[m]}) ] \\
                                             &\quad + \bbI[ \sum_{i=1}^m X_i : \pi_d(X_{[m]}) \; \big| \; \pi_d\bigl(\sum_{i=1}^m X_i\bigr), \pi_{d-1}(X_{[m]}) ]
  \end{align*}
  for $d=1,\dots,m$. The claim follows by telescoping series, noting that $D[X_{[m]} | \pi_0(X_{[m]})] = D[X_{[m]}]$ and that $\pi_m(X_{[m]})=X_{[m]}$ (and also $\pi_m( \sum_i X_i ) = \sum_i X_i$).
  \end{proof}
lemma iter_multiDist_chainRule' {m : ℕ} (hm : m > 0)
    {G : Fin (m + 1) → Type*} [hG : ∀ i, MeasurableSpace (G i)]
    [hGs : ∀ i, MeasurableSingletonClass (G i)] [hGa : ∀ i, AddCommGroup (G i)]
    [hGcount : ∀ i, Fintype (G i)] {φ : ∀ i : Fin m, G (i.succ) →+ G i.castSucc}
    {π : ∀ d, G m →+ G d} (hπ0 : π 0 = 0) (hcomp : ∀ i : Fin m, π i.castSucc = (φ i) ∘ (π i.succ))
    {Ω : Type*} [hΩ : MeasureSpace Ω] {X : Fin m → Ω → (G m)}
    (hX : ∀ i, Measurable (X i)) (h_indep : iIndepFun X) :
    D[X; fun _ ↦ hΩ] ≥
      ∑ d : Fin m, D[fun i ↦ (π (d.succ)) ∘ X i | fun i ↦ (π d.castSucc) ∘ X i; fun _ ↦ hΩ]
      + I[∑ i : Fin m, X i : fun ω i ↦ (π 1) (X i ω)| ⇑(π 1) ∘ ∑ i : Fin m, X i] := by
  have : IsProbabilityMeasure (ℙ : Measure Ω) := h_indep.isProbabilityMeasure
  calc
  _ = D[X | fun i ↦ ⇑(π 0) ∘ X i ; fun _x ↦ hΩ] := by
    rw [hπ0]
    convert (condMultiDist_of_const (fun _ ↦ (0: G 0)) X).symm
  _ = D[X | fun i ↦ ⇑(π m) ∘ X i ; fun _ ↦ hΩ] +
    ∑ d ∈ Finset.Iio (m : Fin (m + 1)),
      (D[fun i ↦ ⇑(π (d + 1)) ∘ X i | fun i ↦ π d ∘ X i ; fun _ ↦ hΩ] +
        I[∑ i : Fin m, X i : fun ω i ↦ (π (d + 1)) (X i ω)|⟨⇑(π (d + 1)) ∘ ∑ i : Fin m, X i, fun ω i ↦ (π d) (X i ω)⟩]) :=
    iter_multiDist_chainRule hcomp hX h_indep (m : Fin (m + 1))
  _ ≥ ∑ d ∈ Finset.Iio (m : Fin (m + 1)),
      (D[fun i ↦ ⇑(π (d + 1)) ∘ X i | fun i ↦ π d ∘ X i ; fun _ ↦ hΩ] +
        I[∑ i : Fin m, X i : fun ω i ↦ (π (d + 1)) (X i ω)|⟨⇑(π (d + 1)) ∘ ∑ i : Fin m, X i, fun ω i ↦ (π d) (X i ω)⟩]) := by
      apply le_add_of_nonneg_left (condMultiDist_nonneg _ (fun _ => this) X _ hX)
  _ = ∑ d : Fin m,
      (D[fun i ↦ ⇑(π (d.succ)) ∘ X i | fun i ↦ ⇑(π d.castSucc) ∘ X i ; fun _ ↦ hΩ] +
        I[∑ i : Fin m, X i : fun ω i ↦ π d.succ (X i ω)|⟨π d.succ ∘ ∑ i : Fin m, X i, fun ω i ↦ π d (X i ω)⟩]) := by
      rw [sum_of_iio_last]
      congr with d
      rw [Fin.coeSucc_eq_succ, Fin.coe_eq_castSucc]
  _ ≥ _ := by
      rw [Finset.sum_add_distrib]
      gcongr
      have : NeZero m := ⟨hm.ne'⟩
      let f (i : Fin m) :=
        I[∑ i', X i' : fun ω i' ↦ π i.succ (X i' ω)|
          ⟨π i.succ ∘ ∑ i', X i', fun ω i' ↦ π i (X i' ω)⟩]
      have hf i : 0 ≤ f i := condMutualInfo_nonneg (by fun_prop) (by fun_prop)
      let F (x : G 1) : G 1 × (Fin m → G 0) := (x, fun _ ↦ 0)
      have hF : Injective F := fun x y ↦ congr_arg Prod.fst
      calc
        I[∑ i, X i : fun ω i ↦ π 1 (X i ω) | π 1 ∘ ∑ i, X i]
          = I[∑ i, X i : fun ω i ↦ π 1 (X i ω) | F ∘ π 1 ∘ ∑ i, X i] := by
          exact (condMutualInfo_of_inj (by fun_prop) (by fun_prop) (by fun_prop) _ hF).symm
        _ = f 0 := ?_
        _ ≤ ∑ j, f j := Finset.single_le_sum (f := f) (fun _ _ ↦ hf _) (Finset.mem_univ _)
      . simp [f]
        simp [hπ0, AddMonoidHom.zero_apply, comp_apply, Finset.sum_apply, _root_.map_sum, F,
          Fin.succ_zero_eq_one']
        congr
        any_goals congr!
        any_goals simp [Fin.succ_zero_eq_one']
        simp [Function.comp_def]
        sorry

/-- Let `G` be an abelian group and let `m ≥ 2`. Suppose that `X_{i,j}`, `1 ≤ i, j ≤ m`, are
independent `G`-valued random variables. Then
`I[(∑ i, X_{i,j})_{j=1}^m : (∑ j, X_{i,j})_{i=1}^m | ∑ i j, X_{i,j}]`
is less than
`∑_{j=1}^{m-1} (D[(X_{i, j})_{i=1}^m] - D[(X_{i, j})_{i = 1}^m | (X_{i,j} + ... + X_{i,m})_{i=1}^m])`
`+ D[(X_{i,m})_{i=1}^m] - D[(∑ j, X_{i,j})_{i=1}^m],`
where all the multidistances here involve the indexing set `{1, ..., m}`. -/