isUniform_sub_const_of_rdist_eq_zero

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₀