Cond multi Dist chain Rule

lemma cond_multiDist_chainRule {G H : Type*} [hG : MeasurableSpace G] [MeasurableSingletonClass G]    [AddCommGroup G] [Finite G]    [hH : MeasurableSpace H] [MeasurableSingletonClass H] [AddCommGroup H]    [Fintype H] (π : G →+ H)    {S : Type*} [Fintype S] [hS : MeasurableSpace S] [MeasurableSingletonClass S]    {m : ℕ} {Ω : Type*} [hΩ : MeasureSpace Ω]    {X : Fin m → Ω → G} (hX : ∀ i, Measurable (X i))    {Y : Fin m → Ω → S} (hY : ∀ i, Measurable (Y i))    (h_indep : iIndepFun (fun i ↦ ⟨X i, Y i⟩)) :    D[X | Y; fun _ ↦ hΩ] = D[X | fun i ↦ ⟨π ∘ X i, Y i⟩; fun _ ↦ hΩ]      + D[fun i ↦ π ∘ X i | Y; fun _ ↦ hΩ]      + I[∑ i, X i : fun ω ↦ (fun i ↦ π (X i ω)) |            ⟨π ∘ (∑ i, X i), fun ω ↦ (fun i ↦ Y i ω)⟩] := by  have : IsProbabilityMeasure (ℙ : Measure Ω) := h_indep.isProbabilityMeasure  set E' := fun (y : Fin m → S) ↦ ⋂ i, Y i ⁻¹' {y i}  set f := fun (y : Fin m → S) ↦ (ℙ (E' y)).toReal  set hΩc : (Fin m → S) → MeasureSpace Ω := fun y ↦ ⟨cond ℙ (E' y)⟩  calc    _ = ∑ y, (f y) * D[X; fun _ ↦ hΩc y] := condMultiDist_eq' hX hY h_indep    _ = ∑ y, (f y) * D[X | fun i ↦ π ∘ X i; fun _ ↦ hΩc y]        + ∑ y, (f y) * D[fun i ↦ π ∘ X i; fun _ ↦ hΩc y]        + ∑ y, (f y) * I[∑ i, X i : fun ω ↦ (fun i ↦ π (X i ω)) |          π ∘ (∑ i, X i); (hΩc y).volume] := by      simp_rw [← Finset.sum_add_distrib, ← left_distrib]      congr with y      by_cases hf : f y = 0      · simp only [hf, zero_mul]      congr 1      convert multiDist_chainRule π (hΩc y) hX _      refine h_indep.cond hY ?_ fun _ ↦ .singleton _      apply prob_nonzero_of_prod_prob_nonzero      convert hf      rw [← ENNReal.toReal_prod]      congr      exact (iIndepFun.meas_iInter h_indep fun _ ↦ mes_of_comap <| .singleton _).symm    _ = _ := by      have hmes : Measurable (π ∘ ∑ i : Fin m, X i) := by        apply Measurable.comp .of_discrete        convert Finset.measurable_sum (f := X) Finset.univ _ with ω        · exact Fintype.sum_apply ω X        exact (fun i _ ↦ hX i)      have hpi_indep : iIndepFun (fun i ↦ ⟨π ∘ X i, Y i⟩) ℙ := by        set g : G × S → H × S := fun p ↦ ⟨π p.1, p.2⟩        exact iIndepFun.comp h_indep (fun _ ↦ g) (by fun_prop)      have hpi_indep' : iIndepFun (fun i ↦ ⟨X i, ⟨π ∘ X i, Y i⟩⟩) ℙ := by        set g : G × S → G × (H × S) := fun p ↦ ⟨p.1, ⟨π p.1, p.2⟩⟩        exact iIndepFun.comp h_indep (fun _ ↦ g) (by fun_prop)      have hey_mes y : MeasurableSet (E' y) := by        apply MeasurableSet.iInter        intro i        exact MeasurableSet.preimage (.singleton (y i)) (hY i)      congr 2      · rw [condMultiDist_eq' hX _ hpi_indep']        · rw [← Equiv.sum_comp (Equiv.arrowProdEquivProdArrow _ _ _).symm, Fintype.sum_prod_type,            Finset.sum_comm]          congr with y          by_cases pey : ℙ (E' y) = 0          · simp only [pey, ENNReal.toReal_zero, zero_mul, f]            apply (Finset.sum_eq_zero _).symm            intro s _            convert zero_mul _            convert ENNReal.toReal_zero            apply measure_mono_null _ pey            intro ω hω            simp only [Equiv.arrowProdEquivProdArrow, Equiv.coe_fn_symm_mk, Set.mem_iInter,              Set.mem_preimage, _root_.prod_eq, comp_apply, Set.mem_singleton_iff, Prod.mk.injEq,              E'] at hω ⊢            intro i            exact (hω i).2          rw [condMultiDist_eq' (hΩ := hΩc y) hX, Finset.mul_sum]          · congr with s            dsimp [f, E', Equiv.arrowProdEquivProdArrow]            rw [← mul_assoc, ← ENNReal.toReal_mul]            congr 2            · rw [mul_comm]              convert! cond_mul_eq_inter (hey_mes y) ?_ _              · rw [← Set.iInter_inter_distrib]                apply Set.iInter_congr                intro i                ext ω                simp [and_comm]              infer_instance            funext _            congr 1            unfold hΩc            dsimp [E']            rw [cond_cond_eq_cond_inter (hey_mes y), ← Set.iInter_inter_distrib]            · congr 1              apply Set.iInter_congr              intro i              ext ω              simp [and_comm]            apply MeasurableSet.iInter            intro i            apply MeasurableSet.preimage (.singleton _)            exact Measurable.comp .of_discrete (hX i)          · intro i            exact Measurable.comp .of_discrete (hX i)          set g : G → G × H := fun x ↦ ⟨x, π x⟩          refine iIndepFun.comp ?_ (fun _ ↦ g) fun _ ↦ .of_discrete          · refine h_indep.cond hY ?_ fun _ ↦ .singleton _            rw [iIndepFun.meas_iInter h_indep fun _ ↦ mes_of_comap <| .singleton _] at pey            contrapose! pey            obtain ⟨i, hi⟩ := pey            exact Finset.prod_eq_zero (Finset.mem_univ i) hi        intro i        exact Measurable.prodMk (.comp .of_discrete (hX i)) (hY i)      · rw [condMultiDist_eq' _ hY hpi_indep]        intro i        apply Measurable.comp .of_discrete (hX i)      rw [condMutualInfo_eq_sum', Fintype.sum_prod_type, Finset.sum_comm]      · congr with y        by_cases pey : ℙ (E' y) = 0        · simp only [pey, ENNReal.toReal_zero, zero_mul, f]          apply (Finset.sum_eq_zero _).symm          intro s _          convert zero_mul _          simp only [ne_eq, measure_ne_top, not_false_eq_true, measureReal_eq_zero_iff]          apply measure_mono_null _ pey          intro ω hω          simp only [Set.mem_preimage, _root_.prod_eq, comp_apply, Finset.sum_apply, _root_.map_sum,            Set.mem_singleton_iff, Prod.mk.injEq, Set.mem_iInter, E'] at hω ⊢          rw [← hω.2]          simp only [implies_true]        have : IsProbabilityMeasure (hΩc y).volume := cond_isProbabilityMeasure pey        rw [condMutualInfo_eq_sum' hmes, Finset.mul_sum]        congr with x        dsimp [f, E']        rw [← mul_assoc, measureReal_def, ← ENNReal.toReal_mul]        congr 2        · rw [mul_comm]          convert! cond_mul_eq_inter (hey_mes y) ?_ _          · ext ω            simp only [Set.mem_preimage, Set.mem_singleton_iff, Prod.mk.injEq, comp_apply,              Finset.sum_apply, _root_.map_sum, Set.mem_inter_iff, Set.mem_iInter, E']            rw [and_comm]            apply and_congr_left            intro _            exact funext_iff          infer_instance        unfold hΩc        dsimp [E']        rw [cond_cond_eq_cond_inter (hey_mes y)]        · congr          ext ω          simp only [Set.mem_inter_iff, Set.mem_iInter, Set.mem_preimage, Set.mem_singleton_iff,            comp_apply, Finset.sum_apply, _root_.map_sum, Prod.mk.injEq, E']          rw [and_comm]          apply and_congr_right          intro _          exact Iff.symm funext_iff        exact MeasurableSet.preimage (.singleton x) hmes      exact Measurable.prodMk hmes (measurable_pi_lambda (fun ω i ↦ Y i ω) hY)