\begin{lemma}[Lower bound on conditional multidistance]\label{cond-multidist-lower}\lean{sub_condMultiDistance_le}\leanok  If  $(X_i)_{1 \leq i \leq m}$ is a $\tau$-minimizer, and $k := D[(X_i)_{1 \leq i \leq m}]$, then for any other tuples $(X'_i)_{1 \leq i \leq m}$ and $(Y_i)_{1 \leq i \leq m}$ with the $X'_i$ $G$-valued, one has
  $$ k - D[(X'_i)_{1 \leq i \leq m} | (Y_i)_{1 \leq i \leq m}] \leq \eta \sum_{i=1}^m d[X_i; X'_i|Y_i].$$
\end{lemma}
\begin{proof}\uses{multidist-lower, cond-multidist-def, cond-multidist-alt}\leanok
  Immediate from \Cref{multidist-lower}, \Cref{cond-multidist-alt}, and \Cref{cond-dist-def}.
\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)): D[X; hΩ] - D[X'|Y; hΩ'] ≤ p.η * ∑ i, d[X i ; (hΩ i).volume # X' i | Y i; (hΩ' i).volume ] := by
  set μ := fun ω: Fin p.m → S ↦ ∏ i : Fin p.m, (ℙ (Y i ⁻¹' {ω i})).toReal

  have probmes (i : Fin p.m) : ∑ ωi : S, (ℙ (Y i ⁻¹' {ωi})).toReal = 1 := by
    convert Finset.sum_toReal_measure_singleton (s := Finset.univ) (Measure.map (Y i) ℙ) with ω _ i _
    · exact (MeasureTheory.Measure.map_apply (hY i) ( .singleton ω)).symm
    replace hΩ'prob := hΩ'prob i
    rw [MeasureTheory.Measure.map_apply (hY i) (Finset.measurableSet _), Finset.coe_univ, Set.preimage_univ, measure_univ, ENNReal.one_toReal]
-- μ has total mass one
  have total : ∑ (ω : Fin p.m → S), μ ω = 1 := calc
    _ = ∏ i, ∑ ωi, (ℙ (Y i ⁻¹' {ωi})).toReal := by
      convert Finset.sum_prod_piFinset Finset.univ _ with ω _ i _
      rfl
    _ = ∏ i, 1 := by
      apply Finset.prod_congr rfl
      intro i _
      exact probmes i
    _ = 1 := by
      simp only [Finset.prod_const_one]

  calc
    _ = ∑ (ω: Fin p.m → S), μ ω * D[X; hΩ] - ∑ (ω: Fin p.m → S), μ ω * D[X' ; fun i ↦ MeasureSpace.mk ℙ[|Y i ⁻¹' {ω i}]] := by
      congr
      rw [← Finset.sum_mul, total, one_mul]
    _ = ∑ (ω: Fin p.m → S), μ ω * (D[X; hΩ] - D[X' ; fun i ↦ MeasureSpace.mk ℙ[|Y i ⁻¹' {ω i}]]) := by
      rw [← Finset.sum_sub_distrib]
      apply Finset.sum_congr rfl
      intro _ _
      exact (mul_sub_left_distrib _ _ _).symm
    _ ≤ ∑ (ω: Fin p.m → S), μ ω * (p.η * ∑ i, d[X i ; (hΩ i).volume # X' i; ℙ[|Y i ⁻¹' {ω i}] ]) := by
      apply Finset.sum_le_sum
      intro ω _
      rcases eq_or_ne (μ ω) 0 with hω | hω
      · simp [hω]
      gcongr
      let hΩ'_cond i := MeasureSpace.mk ℙ[|Y i ⁻¹' {ω i}]
      have hΩ'prob_cond i : IsProbabilityMeasure (hΩ'_cond i).volume := by
        refine cond_isProbabilityMeasure ?_
        contrapose! hω
        apply Finset.prod_eq_zero (Finset.mem_univ i)
        simp only [hω, ENNReal.zero_toReal]
      exact sub_multiDistance_le p Ω hΩ hΩprob X hmeasX h_min Ω' hΩ'_cond hΩ'prob_cond X' hmeasX'
    _ = p.η * ∑ i, ∑ (ω: Fin p.m → S), μ ω * d[X i ; (hΩ i).volume # X' i; ℙ[|Y i ⁻¹' {ω i}] ] := by
      rw [Finset.sum_comm, Finset.mul_sum]
      apply Finset.sum_congr rfl
      intro ω _
      rw [Finset.mul_sum, Finset.mul_sum, Finset.mul_sum]
      apply Finset.sum_congr rfl
      intro i _
      ring
    _ = _ := by
      congr with i
      let f := fun j ↦ (fun ωj ↦ (ℙ (Y j ⁻¹' {ωj})).toReal * (if i=j then d[X i ; ℙ # X' i ; ℙ[|Y i ⁻¹' {ωj}]] else 1))
      calc
        _ = ∑ ω : Fin p.m → S, ∏ j, f j (ω j) := by
          apply Finset.sum_congr rfl
          intro ω _
          rw [Finset.prod_mul_distrib]
          congr
          simp only [Finset.prod_ite_eq, Finset.mem_univ, ↓reduceIte]
        _ = ∏ j, ∑ ωj, f j ωj := Finset.sum_prod_piFinset Finset.univ f
        _ = ∏ j, if i = j then d[X i # X' i | Y i] else 1 := by
          apply Finset.prod_congr rfl
          intro j _
          by_cases hij : i = j
          · simp only [hij, mul_ite, mul_one, ↓reduceIte, f]
            rw [condRuzsaDist'_eq_sum' (hmeasX' i) (hY i), ← hij]
          simp only [mul_ite, mul_one, hij, ↓reduceIte, f]
          exact probmes j
        _ = _ := by
          simp only [Finset.prod_ite_eq, Finset.mem_univ, ↓reduceIte]

/-- 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\}$. -/