condRho_le_condRuzsaDist_of_phiMinimizes

lemma condRho_le_condRuzsaDist_of_phiMinimizes {S T : Type*}    [Finite S] [MeasurableSpace S] [MeasurableSingletonClass S]    [Finite T] [MeasurableSpace T] [MeasurableSingletonClass T]    (h : phiMinimizes X₁ X₂ η A ℙ) (h1 : Measurable X₁') (h2 : Measurable X₂')    {Z : Ω → S} {W : Ω → T} (hZ : Measurable Z) (hW : Measurable W) :    k - η * (ρ[X₁' | Z # A] - ρ[X₁ # A]) - η * (ρ[X₂' | W # A] - ρ[X₂ # A])      ≤ d[X₁' | Z # X₂' | W] := by  cases nonempty_fintype S  cases nonempty_fintype T  have : IsProbabilityMeasure (Measure.map Z ℙ) := isProbabilityMeasure_map hZ.aemeasurable  have : IsProbabilityMeasure (Measure.map W ℙ) := isProbabilityMeasure_map hW.aemeasurable  have hz (a : ℝ) : a = ∑ z, (Measure.real ℙ (Z ⁻¹' {z})) * a := by    simp_rw [← Finset.sum_mul, ← map_measureReal_apply hZ (MeasurableSet.singleton _),      sum_measureReal_singleton]    simp  have hw (a : ℝ) : a = ∑ w, (Measure.real ℙ (W ⁻¹' {w})) * a := by    simp_rw [← Finset.sum_mul, ← map_measureReal_apply hW (MeasurableSet.singleton _),      sum_measureReal_singleton]    simp  rw [condRuzsaDist_eq_sum' h1 hZ h2 hW, hz d[X₁ # X₂],    hz (ρ[X₁ # A]), hz (η * (ρ[X₂' | W # A] - ρ[X₂ # A])), condRho, tsum_fintype,    ← Finset.sum_sub_distrib, Finset.mul_sum, ← Finset.sum_sub_distrib, ← Finset.sum_sub_distrib]  apply Finset.sum_le_sum  intro z _  rw [condRho, tsum_fintype, hw ρ[X₂ # A],    hw ( (Measure.real ℙ (Z ⁻¹' {z})) * k -    η * ((Measure.real ℙ (Z ⁻¹' {z})) * ρ[X₁' ; ℙ[|Z ⁻¹' {z}] # A]      - (Measure.real ℙ (Z ⁻¹' {z})) * ρ[X₁ # A])),    ← Finset.sum_sub_distrib, Finset.mul_sum, Finset.mul_sum, ← Finset.sum_sub_distrib]  apply Finset.sum_le_sum  intro w _  rcases eq_or_ne (Measure.real ℙ (Z ⁻¹' {z})) 0 with hpz | hpz  · simp [hpz]  rcases eq_or_ne (Measure.real ℙ (W ⁻¹' {w})) 0 with hpw | hpw  · simp [hpw]  set μ := ℙ[|Z ← z]  have hμ : IsProbabilityMeasure μ := cond_isProbabilityMeasure_of_real hpz  set μ' := ℙ[|W ← w]  have hμ' : IsProbabilityMeasure μ' := cond_isProbabilityMeasure_of_real hpw  suffices d[X₁ # X₂] - η * (ρ[X₁' ; μ # A] - ρ[X₁ # A]) -      η * (ρ[X₂' ; μ' # A] - ρ[X₂ # A]) ≤ d[X₁' ; μ # X₂'; μ'] by    replace this := mul_le_mul_of_nonneg_left this      (show 0 ≤ (Measure.real ℙ (Z ⁻¹' {z})) * (Measure.real ℙ (W ⁻¹' {w})) by positivity)    convert this using 1    ring  exact le_rdist_of_phiMinimizes h h1 h2