\begin{lemma}[Translate is uniform on symmetry group]\label{sym-zero}
\lean{isUniform_sub_const_of_rdist_eq_zero}\leanok
  If $X$ is a $G$-valued random variable with $d[X ;X]=0$, and $x_0$ is a point with $P[X=x_0] > 0$, then $X-x_0$ is uniformly distributed on $\mathrm{Sym}[X]$.
\end{lemma}
\begin{proof}\uses{zero-large,sym-group-def,uniform-def}\leanok  The law of $X-x_0$ is invariant under $\mathrm{Sym}[X]$, non-zero at the origin, and supported on  $\mathrm{Sym}[X]$, giving the claim.
\end{proof}
lemma isUniform_sub_const_of_rdist_eq_zero (hX : Measurable X) (hdist : d[X # X] = 0) {x₀ : G}
    (hx₀ : ℙ (X⁻¹' {x₀}) ≠ 0) : IsUniform (symmGroup X hX) (fun ω ↦ X ω - x₀) where
  eq_of_mem := by
    have B c z : (fun ω ↦ X ω - c) ⁻¹' {z} = X ⁻¹' {c + z} := by
      ext w; simp [sub_eq_iff_eq_add']
    have A : ∀ (z : G), z ∈ symmGroup X hX →
        ℙ ((fun ω ↦ X ω - x₀) ⁻¹' {z}) = ℙ ((fun ω ↦ X ω - x₀) ⁻¹' {0}) := by
      intro z hz
      have : X ⁻¹' {x₀ + z} = (fun ω ↦ X ω - z) ⁻¹' {x₀} := by simp [B, add_comm]
      simp_rw [B, add_zero, this]
      have Z := (mem_symmGroup hX).1 (AddSubgroup.neg_mem (symmGroup X hX) hz)
      simp [← sub_eq_add_neg] at Z
      exact Z.symm.measure_mem_eq .of_discrete
    intro x hx y hy
    rw [A x hx, A y hy]
  measure_preimage_compl := by
    apply (measure_preimage_eq_zero_iff_of_countable (Set.to_countable _)).2
    intro x hx
    contrapose! hx
    have B : (fun ω ↦ X ω - x₀) ⁻¹' {x} = X ⁻¹' {x₀ + x} := by
      ext w; simp [sub_eq_iff_eq_add']
    rw [B] at hx
    simpa using sub_mem_symmGroup hX hdist hx hx₀