\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 : ℕ}
    {G : Fin (m + 1) → Type*}
    [hG : ∀ i, MeasurableSpace (G i)] [hGs : ∀ i, MeasurableSingletonClass (G i)]
    [∀ i, AddCommGroup (G i)] [hGcounT : ∀ i, Fintype (G i)]
    {φ : ∀ i : Fin m, G (i.succ) →+ G i.castSucc} {π : ∀ d, G m →+ G d}
    (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) (n : Fin (m + 1)) :
    D[X | fun i ↦ (π 0) ∘ X i; fun _ ↦ hΩ] = D[X | fun i ↦ (π n) ∘ X i; fun _ ↦ hΩ]
      + ∑ d ∈ Finset.Iio n, (D[fun i ↦ (π (d+1)) ∘ X i | fun i ↦ (π d) ∘ X i; fun _ ↦ hΩ]
      + I[∑ i, X i : fun ω ↦ (fun i ↦ (π (d+1)) (X i ω)) |
            ⟨(π (d+1)) ∘ ∑ i, X i, fun ω ↦ (fun i ↦ (π d) (X i ω))⟩]) := by
  set S := ∑ i, X i
  set motive := fun n:Fin (m + 1) ↦ D[X | fun i ↦ (π 0) ∘ X i; fun _ ↦ hΩ]
    = D[X | fun i ↦ (π n) ∘ X i; fun _ ↦ hΩ]
      + ∑ d ∈ Finset.Iio n, (D[fun i ↦ (π (d+1)) ∘ X i | fun i ↦ (π d) ∘ X i; fun _ ↦ hΩ]
      + I[S : fun ω ↦ (fun i ↦ (π (d+1)) (X i ω)) |
            ⟨(π (d+1)) ∘ S, fun ω ↦ (fun i ↦ (π d) (X i ω))⟩])
  have zero : motive 0 := by
    have : (Finset.Iio 0 : Finset (Fin (m + 1))) = ∅ := rfl
    simp [motive, this]
  have succ : (n : Fin m) → motive n.castSucc → motive n.succ := by
    intro n hn
    dsimp [motive] at hn ⊢
    have h2 : n.castSucc ∈ Finset.Iio n.succ := by
      simp only [Nat.succ_eq_add_one, Finset.mem_Iio, Fin.castSucc_lt_succ_iff, le_refl]
    rw [hn, ← Finset.add_sum_erase _ _ h2, Iio_of_succ_eq_Iic_of_castSucc, Finset.Iic_erase, ← add_assoc, ← add_assoc, Fin.coeSucc_eq_succ]
    congr 1
    convert cond_multiDist_chainRule (X := X) (Y := fun i ↦ ⇑(π n.castSucc) ∘ X i) (π n.succ) hX ?_ ?_
    . set g : G n.succ → G n.succ × G n.castSucc := fun x ↦ ⟨x, ⇑(φ n) x⟩
      convert (condMultiDist_of_inj (f := g) (fun _ ↦ hΩ) X (fun i ↦ ⇑(π n.succ) ∘ X i) _).symm using 3 with i
      . ext ω
        . dsimp [g, prod]
        rw [hcomp n]
        simp [g, prod]
      intro x x' h
      simp [g] at h
      exact h.1
    . intro _
      exact Measurable.comp .of_discrete (hX _)
    set g : (G m) → (G m) × (G n.castSucc) := fun x ↦ ⟨x, ⇑(π n.castSucc) x⟩
    convert iIndepFun.comp h_indep (fun _ ↦ g) _
    intro _
    exact .of_discrete
  exact Fin.induction zero succ n