rdist_of_inj

lemma rdist_of_inj {H : Type*} [hH : MeasurableSpace H] [MeasurableSingletonClass H]  [AddCommGroup H] [Countable H] (hX : Measurable X) (hY : Measurable Y)  (φ : G →+ H) (hφ : Injective φ) [IsProbabilityMeasure μ] [IsProbabilityMeasure μ'] :    d[φ ∘ X ; μ # φ ∘ Y ; μ'] = d[X ; μ # Y ; μ'] := by    rw [rdist_def, rdist_def]    congr 2    · rw [← entropy_comp_of_injective _ (by fun_prop) _ hφ]      apply IdentDistrib.entropy_congr      constructor      · exact Measurable.aemeasurable .of_discrete      · exact Measurable.aemeasurable .of_discrete      set g := fun x : H × H ↦ x.1 - x.2      set f := fun x : G × G ↦ (φ x.1, φ x.2)      have : φ ∘ (fun x ↦ x.1 - x.2) = g ∘ f := by ext; simp [f, g]      rw [this, ← Measure.map_map (g := g) (f := f) .of_discrete        .of_discrete, ← Measure.map_map .of_discrete hX,        ← Measure.map_map .of_discrete hY]      congr      exact Measure.map_prod_map _ _ .of_discrete .of_discrete    · congr 1      exact entropy_comp_of_injective _ hX _ hφ    exact entropy_comp_of_injective _ hY _ hφ