sum_of_rdist_eq

lemma sum_of_rdist_eq (Y : Fin 4 → Ω → G) (h_indep : iIndepFun Y μ)  (h_meas : ∀ i, Measurable (Y i)) :    d[Y 0; μ # Y 1; μ] + d[Y 2; μ # Y 3; μ]      = d[(Y 0) - (Y 2); μ # (Y 1) - (Y 3); μ]        + d[Y 0 | (Y 0) - (Y 2); μ # Y 1 | (Y 1) - (Y 3); μ]        + I[(Y 0) - (Y 1) : (Y 1) - (Y 3) | (Y 0) - (Y 1) - (Y 2) + (Y 3); μ] := by  let π : G × G →+ G := (AddMonoidHom.fst G G) - (AddMonoidHom.snd G G)  have hπ {W_1 W_2 : Ω → G} : π ∘ ⟨W_1, W_2⟩ = W_1 - W_2 := rfl  let Z_1 : Ω → G × G := ⟨Y 0, Y 2⟩  let Z_2 : Ω → G × G := ⟨Y 1, Y 3⟩  have hZ : Z_1 - Z_2 = ⟨Y 0 - Y 1, Y 2 - Y 3⟩ := rfl  have m1 : Measurable Z_1 := (h_meas 0).prodMk (h_meas 2)  have m2 : Measurable Z_2 := (h_meas 1).prodMk (h_meas 3)  have h_indep_0 : IndepFun (Y 0) (Y 1) μ := h_indep.indepFun (by decide)  have h_indep_2 : IndepFun (Y 2) (Y 3) μ := h_indep.indepFun (by decide)  have h_indep_Z : IndepFun Z_1 Z_2 μ := h_indep.indepFun_prodMk_prodMk h_meas    0 2 1 3 (by decide) (by decide) (by decide) (by decide)  have h_indep_sub : IndepFun (Y 0 - Y 1) (Y 2 - Y 3) μ :=    h_indep.indepFun_sub_sub h_meas 0 1 2 3 (by decide) (by decide) (by decide) (by decide)  have msub (i j : Fin 4) : Measurable (Y i - Y j) := (h_meas i).sub (h_meas j)  have h_add : d[Z_1; μ # Z_2; μ] = d[Y 0; μ # Y 1; μ] + d[Y 2; μ # Y 3; μ] := by    rw [h_indep_0.rdist_eq (h_meas 0) (h_meas 1), h_indep_2.rdist_eq (h_meas 2) (h_meas 3),      h_indep_Z.rdist_eq m1 m2, hZ,      (entropy_pair_eq_add (h_meas 0) (h_meas 2)).2 (h_indep.indepFun (by decide)),      (entropy_pair_eq_add (h_meas 1) (h_meas 3)).2 (h_indep.indepFun (by decide)),      (entropy_pair_eq_add (msub 0 1) (msub 2 3)).2 h_indep_sub]    ring_nf  rw [← h_add, rdist_of_indep_eq_sum_fibre π h_indep_Z m1 m2]  simp only [hπ, hZ]  rw [sum_of_rdist_eq_step_condRuzsaDist h_indep h_meas,    sum_of_rdist_eq_step_condMutualInfo h_meas]