sum_of_rdist_eq_step_condRuzsaDist

lemma sum_of_rdist_eq_step_condRuzsaDist {Y : Fin 4 → Ω → G} (h_indep : iIndepFun Y μ)    (h_meas : ∀ i, Measurable (Y i)) :    d[⟨Y 0, Y 2⟩ | Y 0 - Y 2 ; μ # ⟨Y 1, Y 3⟩ | Y 1 - Y 3 ; μ]      = d[Y 0 | Y 0 - Y 2 ; μ # Y 1 | Y 1 - Y 3 ; μ] := by  let Y' : Fin 4 → Ω → G    | 0 => Y 0    | 1 => Y 1    | 2 => Y 0 - Y 2    | 3 => Y 1 - Y 3  let f : (G × G) → (G × G) := fun (g, h) ↦ (g, g - h)  have hf : Measurable f := .of_discrete  have h_indep' : IndepFun (⟨Y' 0, Y' 2⟩) (⟨Y' 1, Y' 3⟩) μ :=    (h_indep.indepFun_prodMk_prodMk h_meas 0 2 1 3      (by decide) (by decide) (by decide) (by decide)).comp hf hf  have h_meas' : ∀ i, Measurable (Y' i)    | 0 => h_meas 0    | 1 => h_meas 1    | 2 => (h_meas 0).sub (h_meas 2)    | 3 => (h_meas 1).sub (h_meas 3)  have h' (i j : Fin 4) : ⟨Y i, Y j⟩ = ⟨Y i, Y i - (Y i - Y j)⟩ := by simp only [sub_sub_cancel]  rw [h' 0 2, h' 1 3]  exact condRuzsaDist_of_inj_map Y' h_indep' h_meas'    ((AddMonoidHom.fst G G).prod ((AddMonoidHom.fst G G) - (AddMonoidHom.snd G G)))    (fun _ _ _ h ↦ (Prod.ext_iff.1 h).1)