sub_condMultiDistance_le

lemma sub_condMultiDistance_le {G Ω₀ : Type u} [MeasurableFinGroup 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, Measure.real ℙ (Y i ⁻¹' {ω i})  have probmes (i : Fin p.m) : ∑ ωi : S, (Measure.real ℙ (Y i ⁻¹' {ωi})) = 1 := by    convert sum_measureReal_singleton (s := Finset.univ) (μ := .map (Y i) ℙ) with ω _ i _    · exact (map_measureReal_apply (hY i) ( .singleton ω)).symm    replace hΩ'prob := hΩ'prob i    rw [map_measureReal_apply (hY i) (Finset.measurableSet _), Finset.coe_univ, Set.preimage_univ,      probReal_univ]-- μ has total mass one  have total : ∑ ω, μ ω = 1 := calc    _ = ∏ i, ∑ ωi, Measure.real ℙ (Y i ⁻¹' {ωi}) := by      convert! Finset.sum_prod_piFinset Finset.univ _ with ω _ i _      rfl    _ = ∏ i, 1 := by congr with i; exact probmes i    _ = 1 := by      simp only [Finset.prod_const_one]  calc    _ = ∑ ω, μ ω * D[X; hΩ] -        ∑ ω, μ ω * D[X' ; fun i ↦ MeasureSpace.mk ℙ[|Y i ⁻¹' {ω i}]] := by      congr      rw [← Finset.sum_mul, total, one_mul]    _ = ∑ ω, μ ω * (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    _ ≤ ∑ ω, μ ω * (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 [measureReal_def, hω, ENNReal.toReal_zero]      exact sub_multiDistance_le hΩprob hmeasX h_min hΩ'prob_cond hmeasX'    _ = p.η * ∑ i, ∑ ω, μ ω * d[X i ; (hΩ i).volume # X' i; ℙ[|Y i ⁻¹' {ω i}] ] := by      rw [Finset.sum_comm, Finset.mul_sum]      congr with ω      rw [Finset.mul_sum, Finset.mul_sum, Finset.mul_sum]      congr with i      ring    _ = _ := by      congr with i      let f := fun j ↦ (fun ωj ↦ (Measure.real ℙ (Y j ⁻¹' {ωj})) *        (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]