\begin{corollary}[Lower bound on conditional multidistance, II]\label{cond-multidist-lower-II}\lean{sub_condMultiDistance_le'}\leanok With the notation of the previous lemma, we have
  \begin{equation}\label{5.3-conv}
    k - D[ X'_{[m]} | Y_{[m]} ] \leq \eta \sum_{i=1}^m d[X_{\sigma(i)};X'_i|Y_i]
  \end{equation}
for any permutation $\sigma : \{1,\dots,m\} \rightarrow \{1,\dots,m\}$.
\end{corollary}
\begin{proof}\uses{cond-multidist-lower, multidist-perm}\leanok  This follows from \Cref{cond-multidist-lower} and \Cref{multidist-perm}.
\end{proof}
lemma sub_condMultiDistance_le' {G Ω₀ : Type u} [MeasureableFinGroup G] [MeasureSpace Ω₀] (p : multiRefPackage G Ω₀) (Ω : Fin p.m → Type u) (hΩ : ∀ i, MeasureSpace (Ω i)) (hΩprob: ∀ i, IsProbabilityMeasure (hΩ i).volume) (X : ∀ i, Ω i → G) (hmeasX: ∀ i, Measurable (X i)) (h_min : multiTauMinimizes p Ω hΩ X) (Ω' : Fin p.m → Type u) (hΩ' : ∀ i, MeasureSpace (Ω' i)) (hΩ'prob: ∀ i, IsProbabilityMeasure (hΩ' i).volume) (X' : ∀ i, Ω' i → G) (hmeasX': ∀ i, Measurable (X' i)) {S : Type u} [Fintype S] [MeasurableSpace S] [MeasurableSingletonClass S] (Y : ∀ i, Ω' i → S) (hY : ∀ i, Measurable (Y i)) (φ : Equiv.Perm (Fin p.m)) : D[X; hΩ] - D[X'|Y; hΩ'] ≤ p.η * ∑ i, d[X (φ i) ; (hΩ (φ i)).volume # X' i | Y i; (hΩ' i).volume ] := by
  let Xφ := fun i => X (φ i)
  let Ωφ := fun i => Ω (φ i)
  let hΩφ := fun i => hΩ (φ i)
  let hΩφprob := fun i => hΩprob (φ i)
  let hmeasXφ := fun i => hmeasX (φ i)
  calc
    _ = D[Xφ; hΩφ] - D[X'|Y; hΩ'] := by
      congr 1
      rw [multiDist_of_perm hΩ hΩprob X φ]
    _ ≤ _ := by
      apply sub_condMultiDistance_le p Ωφ hΩφ hΩφprob Xφ hmeasXφ _ Ω' hΩ' hΩ'prob X' hmeasX' Y hY
      intro Ω'' hΩ'' X''
      calc
      _ = multiTau p Ω hΩ X := by
        dsimp [multiTau]
        congr 1
        · exact multiDist_of_perm hΩ hΩprob X φ
        congr 1
        exact Fintype.sum_equiv φ _ _ fun _ ↦ rfl
      _ ≤ multiTau p Ω'' hΩ'' X'' := h_min Ω'' hΩ'' X''