\begin{lemma}[Zero Ruzsa distance implies large symmetry group]\label{zero-large}
  \lean{sub_mem_symmGroup}\leanok  If $X$ is a $G$-valued random variable such that
  $d[X ;X]=0$, and $x,y \in G$ are such that $P[X=x], P[X=y]>0$, then $x-y \in \mathrm{Sym}[X]$.
\end{lemma}
\begin{proof}
  \uses{ruz-indep, ruz-copy, relabeled-entropy-cond,vanish-entropy, alternative-mutual, independent-exist,sym-group-def}\leanok
   Let $X_1,X_2$ be independent copies of $X$ (from \Cref{independent-exist}). Let $A$ denote the range of $X$.  From \Cref{ruz-indep} and \Cref{ruz-copy} we have
  $$ \bbH[X_1-X_2] = \bbH[X_1].$$
Observe from \Cref{relabeled-entropy-cond} that
$$ \bbH[X_1-X_2|X_2] = \bbH[X_1|X_2] = \bbH[X_1]$$
and hence by \Cref{alternative-mutual}
$$ \bbI[X_1-X_2 : X_1] = 0.$$
By \Cref{vanish-entropy}, $X_1-X_2$ and $X_1$ are therefore independent, thus the law of $(X_1-X_2|X_1=x)$ does not depend on $x \in A$. The claim follows.
\end{proof}
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_eq hidY]
      rw [h_indep.rdist_eq hX' hY', ← (hidX.trans hidY.symm).entropy_eq] 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 (config := {contextual := true}) [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

/-- If `d[X # X] = 0`, then `X - x₀` is the uniform distribution on the subgroup of `G`
stabilizing the distribution of `X`, for any `x₀` of positive probability. -/