I₃_eq

lemma I₃_eq [IsProbabilityMeasure (ℙ : Measure Ω)] : I[V : W | S] = I₂ := by  have h_indep2 : iIndepFun ![X₁', X₂, X₁, X₂'] := by    exact h_indep.reindex_four_cbad  have hident : IdentDistrib (fun a (i : Fin 4) => ![X₁, X₂, X₁', X₂'] i a)    (fun a (j : Fin 4) => ![X₁', X₂, X₁, X₂'] j a) := by    exact { aemeasurable_fst := by              apply Measurable.aemeasurable              rw [measurable_pi_iff]              intro x              fin_cases x;              all_goals aesop            aemeasurable_snd := by              apply Measurable.aemeasurable              rw [measurable_pi_iff]              intro x              fin_cases x;              all_goals aesop            map_eq := by              rw [(ProbabilityTheory.iIndepFun_iff_map_fun_eq_pi_map                (Fin.cases hX₁.aemeasurable <| Fin.cases hX₂.aemeasurable <|                Fin.cases hX₁'.aemeasurable <| Fin.cases hX₂'.aemeasurable Fin.rec0)).mp h_indep,                (ProbabilityTheory.iIndepFun_iff_map_fun_eq_pi_map                (Fin.cases hX₁'.aemeasurable <| Fin.cases hX₂.aemeasurable <|                Fin.cases hX₁.aemeasurable <| Fin.cases hX₂'.aemeasurable Fin.rec0)).mp h_indep2]              congr              ext i              fin_cases i              all_goals simp [h₁.map_eq] }  have hmeas1 : Measurable (fun p : Fin 4 → G => (p 0 + p 1, p 0 + p 1 + p 2 + p 3)) := by    fun_prop  have hUVS : IdentDistrib (prod U S) (prod V S) := by    convert! hident.comp hmeas1; simp; abel  have hUVWS : IdentDistrib (prod (prod U W) S) (prod (prod V W) S) := by    convert (hident.comp hmeas2) <;> simp <;> abel  have hU : Measurable U := Measurable.add hX₁ hX₂  have hV : Measurable V := Measurable.add hX₁' hX₂  have hW : Measurable W := Measurable.add hX₁' hX₁  have hS : Measurable S := by fun_prop  rw [condMutualInfo_eq hV hW hS, condMutualInfo_eq hU hW hS, chain_rule'' ℙ hU hS,    chain_rule'' ℙ hV hS, chain_rule'' ℙ hW hS, chain_rule'' ℙ _ hS, chain_rule'' ℙ _ hS,    hUVS.entropy_congr, hUVWS.entropy_congr]  · exact Measurable.prod hU hW  · exact Measurable.prod hV hW