comparison_of_ruzsa_distances

lemma comparison_of_ruzsa_distances [IsProbabilityMeasure μ] [IsProbabilityMeasure μ']    {X : Ω → G} {Y : Ω' → G} {Z : Ω' → G}    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (h : IndepFun Y Z μ')    [FiniteRange X] [FiniteRange Z] [FiniteRange Y] :    d[X ; μ # Y+ Z ; μ'] - d[X ; μ # Y ; μ'] ≤ (H[Y + Z; μ'] - H[Y; μ']) / 2 ∧    (Module (ZMod 2) G →      H[Y + Z; μ'] - H[Y; μ'] = d[Y; μ' # Z; μ'] + H[Z; μ'] / 2 - H[Y; μ'] / 2) := by  obtain ⟨Ω'', mΩ'', μ'', X', Y', Z', hμ, hi, hX', hY', hZ', h2X', h2Y', h2Z', _, _, _⟩ :=    independent_copies3_nondep_finiteRange hX hY hZ μ μ' μ'  have hY'Z' : IndepFun Y' Z' μ'' := hi.indepFun (show (1 : Fin 3) ≠ 2 by decide)  have h2 : IdentDistrib (Y' + Z') (Y + Z) μ'' μ' := h2Y'.add h2Z' hY'Z' h  have hm : ∀ (i : Fin 3), Measurable (![X', Y', Z'] i) :=    fun i ↦ by fin_cases i <;> (dsimp; assumption)  have hXY' : IndepFun X' Y' μ'' := hi.indepFun (show (0 : Fin 3) ≠ 1 by decide)  have hYZ' : IndepFun Y' Z' μ'' := hi.indepFun (show (1 : Fin 3) ≠ 2 by decide)  have hXYZ' : IndepFun X' (Y' + Z') μ'' := by    symm    exact hi.indepFun_add_left hm 1 2 0 (by decide) (by decide)  rw [← h2X'.rdist_congr h2Y', ← h2X'.rdist_congr h2, ← h2Y'.rdist_congr h2Z',    ← h2.entropy_congr, ← h2Y'.entropy_congr, ← h2Z'.entropy_congr]  rw [hXY'.rdist_eq hX' hY', hYZ'.rdist_eq hY' hZ', hXYZ'.rdist_eq hX' (hY'.add hZ')]  constructor  · linarith [kaimanovich_vershik' hi hX' hY' hZ']  · intro hG    rw [ZModModule.sub_eq_add Y' Z']    ring