condRuzsaDist'_of_inj_map'

lemma condRuzsaDist'_of_inj_map' [Module (ZMod 2) G] [IsProbabilityMeasure μ]    [IsProbabilityMeasure μ''] {A : Ω'' → G} {B C : Ω → G} (hA : Measurable A) (hB : Measurable B)    (hC : Measurable C) [FiniteRange A] [FiniteRange B] [FiniteRange C] :    d[A ; μ'' # B | B + C ; μ] = d[A ; μ'' # C | B + C ; μ] := by  -- we want to apply `condRuzsaDist'_of_inj_map'`, but for that all variables need to  -- be in the same probability space  let Ω' := Ω'' × Ω  set X₂' : Ω' → G := A ∘ Prod.fst with hX₂'_def  have hX₂' : Measurable X₂' := hA.comp measurable_fst  let B' : Ω' → G := B ∘ Prod.snd  have hB' : Measurable B' := hB.comp measurable_snd  let C' : Ω' → G := C ∘ Prod.snd  have hC' : Measurable C' := hC.comp measurable_snd  let μ' : Measure Ω' := Measure.prod μ'' μ  have : IsProbabilityMeasure μ' := by infer_instance  -- h1 and h2 should be applications of a new lemma?  have h1 : d[A ; μ'' # B | B + C ; μ] = d[X₂' ; μ' # B' | B' + C' ; μ'] := by    refine condRuzsaDist'_of_copy A hB (by fun_prop) X₂' hB' (by fun_prop) ?_ ?_    · constructor      · exact hA.aemeasurable      · exact hX₂'.aemeasurable      · rw [← Measure.map_map hA measurable_fst]        simp [μ']    · constructor      · exact (hB.prodMk (hB.add hC)).aemeasurable      · exact (hB'.prodMk (hB'.add hC')).aemeasurable      · have : ⟨B', B' + C'⟩ = (⟨B, B + C⟩) ∘ Prod.snd := by ext1 _; simp [C', B']        rw [this, ← Measure.map_map _ measurable_snd]        · simp only [Measure.map_snd_prod, measure_univ, one_smul, μ']        · exact hB.prodMk (hB.add hC)  have h2 : d[A ; μ'' # C | B + C ; μ] = d[X₂' ; μ' # C' | B' + C' ; μ'] := by    apply condRuzsaDist'_of_copy _ hC (by fun_prop) X₂' hC' (by fun_prop) ?_ ?_    · constructor      · exact hA.aemeasurable      · exact hX₂'.aemeasurable      · rw [← Measure.map_map hA measurable_fst]        simp [μ']    · constructor      · exact (hC.prodMk (hB.add hC)).aemeasurable      · exact (hC'.prodMk (hB'.add hC')).aemeasurable      · have : ⟨C', B' + C'⟩ = (⟨C, B + C⟩) ∘ Prod.snd := by ext1 _; simp [B', C']        rw [this, ← Measure.map_map _ measurable_snd]        · simp only [Measure.map_snd_prod, measure_univ, one_smul, μ']        · exact hC.prodMk (hB.add hC)  rw [h1, h2, condRuzsaDist'_of_inj_map hX₂' hB' hC']  rw [indepFun_iff_map_prod_eq_prod_map_map hX₂'.aemeasurable (hB'.prodMk hC').aemeasurable]  have h_prod : (fun ω ↦ (X₂' ω, prod B' C' ω)) = Prod.map A (⟨B, C⟩) := by    ext1    simp only [comp_apply, X₂', B', C']    rfl  have h_comp_snd : (fun a ↦ (B' a, C' a)) = (⟨B, C⟩) ∘ Prod.snd := by ext1; simp [B', C']  rw [h_prod, h_comp_snd, hX₂'_def, ← Measure.map_map _ measurable_snd,    ← Measure.map_map _ measurable_fst, Measure.map_prod_map]  rotate_left  · exact hA  · exact hB.prodMk hC  · exact hA  · exact hB.prodMk hC  simp [μ']