condRuzsaDist_of_inj_map

lemma condRuzsaDist_of_inj_map {G' : Type*} [Countable G'] [AddCommGroup G']  [MeasurableSpace G'] [MeasurableSingletonClass G'] [IsProbabilityMeasure μ]  (Y : Fin 4 → Ω → G) (h_indep : IndepFun (⟨Y 0, Y 2⟩) (⟨Y 1, Y 3⟩) μ)  (h_meas : ∀ i, Measurable (Y i)) (π : G × G →+ G')  (hπ : ∀ (h : G), Injective (fun g ↦ π (g, h)))  [FiniteRange (Y 2)] [FiniteRange (Y 3)] :    d[π ∘ ⟨Y 0, Y 2⟩ | Y 2 ; μ # π ∘ ⟨Y 1, Y 3⟩ | Y 3 ; μ] = d[Y 0 | Y 2 ; μ # Y 1 | Y 3 ; μ] := by  let f (h : G) (g : G) : G' := π (g, h)  let f' : G × G → G → G' := fun (h1, h2) ↦ fun g ↦ π (g, h1 - h2)  have hf' (t : G × G) : Injective (f' t) := fun _ _ h ↦ hπ _ h  let f'' : G × G → G' × G := fun (g, h) ↦ (π (g, h), h)  have hf'' : Measurable f'' := .of_discrete  have hm1 : Measurable (Y 0 - Y 1) := (h_meas 0).sub (h_meas 1)  have hm2 : Measurable (⟨Y 2, Y 3⟩) := (h_meas 2).prodMk (h_meas 3)  rw [condRuzsaDist_of_indep (h_meas 0) (h_meas 2) (h_meas 1) (h_meas 3) μ h_indep,    condRuzsaDist_of_indep (by fun_prop) (by fun_prop) (by fun_prop) (by fun_prop) μ    (by exact h_indep.comp hf'' hf''),    ← condEntropy_of_injective μ hm1 hm2 f' hf', ← map_comp_sub π,    ← condEntropy_of_injective μ (h_meas 0) (h_meas 2) f hπ,    ← condEntropy_of_injective μ (h_meas 1) (h_meas 3) f hπ]  rfl