\begin{corollary}[General 100\% inverse theorem]\label{lem:100pc}
  \lean{exists_isUniform_of_rdist_eq_zero}\leanok
  Suppose that $X_1,X_2$ are $G$-valued random variables such that
  $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$.
\end{corollary}
\begin{proof}\uses{lem:100pc-self,ruzsa-triangle, ruzsa-nonneg}\leanok
Using \Cref{ruzsa-triangle} and \Cref{ruzsa-nonneg} we have $d[X_1;X_1]=0$, hence by \Cref{lem:100pc-self} $d[X_1;U_H]=0$ for some subgroup $H$.  By \Cref{ruzsa-triangle} and \Cref{ruzsa-nonneg} again we also have $d[X_2;U_H]$ as required.
\end{proof}
theorem exists_isUniform_of_rdist_eq_zero
    {Ω' : Type*} [MeasureSpace Ω'] [IsProbabilityMeasure (ℙ : Measure Ω')] {X' : Ω' → G}
    (hX : Measurable X) (hX' : Measurable X') (hdist : d[X # X'] = 0) :
    ∃ H : AddSubgroup G, ∃ U : Ω → G,
      Measurable U ∧ IsUniform H U ∧ d[X # U] = 0 ∧ d[X' # U] = 0 := by
  have h' : d[X # X] = 0 := by
    apply le_antisymm _ (rdist_nonneg hX hX)
    calc
      d[X # X] ≤ d[X # X'] + d[X' # X] := rdist_triangle hX hX' hX
      _ = 0 := by rw [hdist, rdist_symm, hdist, zero_add]
  rcases exists_isUniform_of_rdist_self_eq_zero hX h' with ⟨H, U, hmeas, hunif, hd⟩
  refine ⟨H, U, hmeas, hunif, hd, ?_⟩
  apply le_antisymm _ (rdist_nonneg hX' hmeas)
  calc
    d[X' # U] ≤ d[X' # X] + d[X # U] := rdist_triangle hX' hX hmeas
    _ = 0 := by rw [hd, rdist_symm, hdist, zero_add]