\begin{lemma}[Symmetric 100\% inverse theorem]\label{lem:100pc-self}
  \lean{exists_isUniform_of_rdist_self_eq_zero}\leanok
  Suppose that $X$ is a $G$-valued random variable such that
  $d[X ;X]=0$. Then there exists a subgroup $H \leq G$ such that $d[X ;U_H] = 0$.
\end{lemma}
\begin{proof}\uses{sym-group, sym-zero}\leanok
Take $H$ to be the symmetry group of $X$, which is a group by \Cref{sym-group}. From \Cref{sym-zero}, $X-x_0$ is uniform on $H$, and $d[X ;X-x_0] = d[X ;X] \leq 0$, and the claim follows.
\end{proof}
/-- If $d[X ;X]=0$, then there exists a subgroup $H \leq G$ such that $d[X ;U_H] = 0$. -/
theorem exists_isUniform_of_rdist_self_eq_zero (hX : Measurable X) (hdist : d[X # X] = 0) :
    ∃ H : AddSubgroup G, ∃ U : Ω → G, Measurable U ∧ IsUniform H U ∧ d[X # U] = 0 := by
  -- use for `U` a translate of `X` to make sure that `0` is in its support.
  obtain ⟨x₀, h₀⟩ : ∃ x₀, ℙ (X⁻¹' {x₀}) ≠ 0 := by
    by_contra! h
    have A a : (ℙ : Measure Ω).map X {a} = 0 := by
      rw [Measure.map_apply hX .of_discrete]
      exact h _
    have B : (ℙ : Measure Ω).map X = 0 := by
      rw [← Measure.sum_smul_dirac (μ := (ℙ : Measure Ω).map X)]
      simp [A]
    have : IsProbabilityMeasure ((ℙ : Measure Ω).map X) :=
      isProbabilityMeasure_map hX.aemeasurable
    exact IsProbabilityMeasure.ne_zero _ B
  refine ⟨symmGroup X hX, fun ω ↦ X ω - x₀, hX.sub_const _,
    isUniform_sub_const_of_rdist_eq_zero hX hdist h₀, ?_⟩
  simp_rw [sub_eq_add_neg]
  suffices d[X # X + fun _ ↦ -x₀] = 0 by convert this
  rw [rdist_add_const hX hX]
  exact hdist

/-- If $d[X_1;X_2]=0$, then there exists a subgroup $H \leq G$ such that
$d[X_1;U_H] = d[X_2;U_H] = 0$. Follows from the preceding claim by the triangle inequality. -/