sub_mem_symmGroup

lemma sub_mem_symmGroup (hX : Measurable X) (hdist : d[X # X] = 0)    {x y : G} (hx : ℙ (X ⁻¹' {x}) ≠ 0) (hy : ℙ (X ⁻¹' {y}) ≠ 0) : x - y ∈ symmGroup X hX := by  /- Consider two independent copies `X'` and `Y'` of `X`. The assumption on the Rusza distance  ensures that `H[X' - Y' | Y'] = H[X' - Y']`, i.e., `X' - Y'` and `Y'` are independent. Therefore,  the distribution of `X' - c` is independent of `c` for `c` in the support of `Y'`.  In particular, `X' - x` and `X' - y` have the same distribution, which is equivalent to the  claim of the lemma. -/  rcases ProbabilityTheory.independent_copies_two hX hX with    ⟨Ω', mΩ', X', Y', hP, hX', hY', h_indep, hidX, hidY⟩  rw [hidX.symm.symmGroup_eq hX hX']  have A : H[X' - Y' | Y'] = H[X' - Y'] := calc    H[X' - Y' | Y'] = H[X' | Y'] := condEntropy_sub_right hX' hY'    _ = H[X'] := h_indep.condEntropy_eq_entropy hX' hY'    _ = H[X' - Y'] := by      have : d[X' # Y'] = 0 := by rwa [hidX.rdist_congr hidY]      rw [h_indep.rdist_eq hX' hY', ← (hidX.trans hidY.symm).entropy_congr] at this      linarith  have I : IndepFun (X' - Y') Y' := by    refine (mutualInfo_eq_zero (by fun_prop) hY').1 ?_    rw [mutualInfo_eq_entropy_sub_condEntropy (by fun_prop) hY', A, sub_self]  have M : ∀ c, ℙ (Y' ⁻¹' {c}) ≠ 0 → IdentDistrib (fun ω ↦ X' ω - c) (X' - Y') := by    intro c hc    let F := fun ω ↦ X' ω - c    refine ⟨by fun_prop, by fun_prop, ?_⟩    ext s hs    rw [Measure.map_apply (by fun_prop) hs, Measure.map_apply (by fun_prop) hs]    have : ℙ (F ⁻¹' s) * ℙ (Y' ⁻¹' {c}) = ℙ ((X' - Y') ⁻¹' s) * ℙ (Y' ⁻¹' {c}) := by calc      ℙ (F ⁻¹' s) * ℙ (Y' ⁻¹' {c}) = ℙ (F ⁻¹' s ∩ Y' ⁻¹' {c}) := by        have hFY' : IndepFun F Y' := by          have : Measurable (fun z ↦ z - c) := measurable_sub_const' c          apply h_indep.comp this measurable_id        rw [indepFun_iff_measure_inter_preimage_eq_mul.1 hFY' _ _ hs .of_discrete]      _ = ℙ ((X' - Y') ⁻¹' s ∩ Y' ⁻¹' {c}) := by        congr 1; ext z; simp +contextual [F]      _ = ℙ ((X' - Y') ⁻¹' s) * ℙ (Y' ⁻¹' {c}) := by        rw [indepFun_iff_measure_inter_preimage_eq_mul.1 I _ _ hs .of_discrete]    rwa [ENNReal.mul_left_inj hc (measure_ne_top ℙ _)] at this  have J : IdentDistrib (fun ω ↦ X' ω - x) (fun ω ↦ X' ω - y) := by    have Px : ℙ (Y' ⁻¹' {x}) ≠ 0 := by      convert hx; exact hidY.measure_mem_eq .of_discrete    have Py : ℙ (Y' ⁻¹' {y}) ≠ 0 := by      convert hy; exact hidY.measure_mem_eq .of_discrete    exact (M x Px).trans (M y Py).symm  have : IdentDistrib X' (fun ω ↦ X' ω + (x - y)) := by    have : Measurable (fun c ↦ c + x) := measurable_add_const x    convert J.comp this using 1    · ext ω; simp    · ext ω; simp; abel  exact this