iter_multiDist_chainRule'

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 ⊤ →+ G d} (hπ0 : π 0 = 0) (hcomp : ∀ i : Fin m, π i.castSucc = φ i ∘ π i.succ)    {Ω : Type*} [hΩ : MeasureSpace Ω] {X : Fin m → Ω → G ⊤}    (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]    exact (condMultiDist_of_const (fun _ ↦ (0: G 0)) X).symm  _ = D[X | fun i ↦ π ⊤ ∘ X i ; fun _ ↦ hΩ] +    ∑ d ∈ .Iio (.last m),      (D[fun i ↦ π (d + 1) ∘ X i | fun i ↦ π d ∘ X i ; fun _ ↦ hΩ] +        I[∑ i, X i : fun ω i ↦ π (d + 1) (X i ω)|          ⟨π (d + 1) ∘ ∑ i, X i, fun ω i ↦ (π d) (X i ω)⟩]) :=    iter_multiDist_chainRule hcomp hX h_indep (.last m : Fin (m + 1))  _ ≥ ∑ d ∈ .Iio (.last m),      (D[fun i ↦ π (d + 1) ∘ X i | fun i ↦ π d ∘ X i ; fun _ ↦ hΩ] +        I[∑ i, X i : fun ω i ↦ π (d + 1) (X i ω)|          ⟨π (d + 1) ∘ ∑ i, 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.castSucc (X i ω)⟩]) := by      rw [← Fin.sum_univ_castSucc']      congr!      any_goals rw [Fin.coeSucc_eq_succ]      simp_all  _ ≥ _ := 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.castSucc (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)      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          have hF : Injective F := fun x y ↦ congr_arg Prod.fst          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 only [Fin.castSucc_zero, hπ0, F, f]      rw [← Fin.succ_zero_eq_one']      congr 1