condRuzsaDist'_of_inj_map

lemma condRuzsaDist'_of_inj_map [IsProbabilityMeasure μ] [Module (ZMod 2) G]  {X B C : Ω → G}    (hX : Measurable X) (hB : Measurable B) (hC : Measurable C)    (h_indep : IndepFun X (⟨B, C⟩) μ) [FiniteRange X] [FiniteRange B] [FiniteRange C] :    d[X ; μ # B | B + C ; μ] = d[X ; μ # C | B + C ; μ] := by  let π : G × G →+ G :=  { toFun := fun x ↦ x.2 - x.1    map_zero' := by simp    map_add' := fun a b ↦ by simp only [Prod.snd_add, Prod.fst_add, ZModModule.sub_eq_add]; abel }  let Y : Fin 4 → Ω → G := ![-X, C, fun _ ↦ 0, B + C]  have _ : FiniteRange (Y 0) := by simp [Y]; infer_instance  have _ : FiniteRange (Y 1) := by simp [Y]; infer_instance  have _ : FiniteRange (Y 2) := by simp [Y]; infer_instance  have _ : FiniteRange (Y 3) := by simp [Y]; infer_instance  have hY_meas i : Measurable (Y i) := by    fin_cases i; exacts [hX.neg, hC, measurable_const, hB.add hC]  calc d[X ; μ # B | B + C ; μ]    = d[X | fun _ : Ω ↦ (0 : G) ; μ # B | B + C ; μ] := by rw [condRuzsaDist_of_const hX]  _ = d[π ∘ ⟨-X, fun _ : Ω ↦ (0 : G)⟩ | fun _ : Ω ↦ (0 : G) ; μ # π ∘ ⟨C, B + C⟩ | B + C ; μ] := by    congr    · ext1 ω; simp [π]    · ext1 ω      simp only [AddMonoidHom.coe_mk, ZeroHom.coe_mk, comp_apply, Pi.add_apply, π]      abel  _ = d[π ∘ ⟨Y 0, Y 2⟩ | Y 2 ; μ # π ∘ ⟨Y 1, Y 3⟩ | Y 3 ; μ] := by congr  _ = d[-X | fun _ : Ω ↦ (0 : G) ; μ # C | B + C ; μ] := by    rw [condRuzsaDist_of_inj_map _ _ hY_meas π (fun _ ↦ sub_right_injective)]    · congr    · have h1 : (⟨Y 0, Y 2⟩) = (fun x ↦ (-x, 0)) ∘ X := by ext1 ω; simp [Y]      have h2 : (⟨Y 1, Y 3⟩) = (fun p ↦ (p.2, p.1 + p.2)) ∘ (⟨B, C⟩) := by        ext ω : 1; simp [ZModModule.neg_eq_self, Y]      rw [h1, h2]      refine h_indep.comp ?_ ?_      · exact measurable_neg.prodMk measurable_const      · exact measurable_snd.prodMk (measurable_fst.add measurable_snd)  _ = d[-X ; μ # C | B + C ; μ] := by rw [condRuzsaDist_of_const]; exact hX.neg  _ = d[X ; μ # C | B + C ; μ] := by simp_rw [ZModModule.neg_eq_self]