\begin{lemma}[Distance lower bound]\label{distance-lower}
  \uses{tau-min-def}\leanok
  \lean{distance_ge_of_min}
  For any $G$-valued random variables $X'_1,X'_2$, one has
$$ d[X'_1;X'_2] \geq k - \eta (d[X^0_1;X'_1] - d[X^0_1;X_1] ) - \eta (d[X^0_2;X'_2] - d[X^0_2;X_2] ).$$
\end{lemma}
\begin{proof}
  \uses{tau-def, tau-min}\leanok
  Immediate from \Cref{tau-def} and \Cref{tau-min}.
\end{proof}
lemma distance_ge_of_min (h : tau_minimizes p X₁ X₂) (h1 : Measurable X₁') (h2 : Measurable X₂') :
    d[X₁ # X₂] - p.η * (d[p.X₀₁ # X₁'] - d[p.X₀₁ # X₁]) - p.η * (d[p.X₀₂ # X₂'] - d[p.X₀₂ # X₂])
      ≤ d[X₁' # X₂'] := by
  have Z := is_tau_min p h h1 h2
  simp [tau] at Z
  linarith

omit [IsProbabilityMeasure (ℙ : Measure Ω₀₁)] [IsProbabilityMeasure (ℙ : Measure Ω₀₂)] [Fintype G]
[IsProbabilityMeasure (ℙ : Measure Ω)] in