condRuzsaDist'_eq_sum

lemma condRuzsaDist'_eq_sum {X : Ω → G} {Y : Ω' → G} {W : Ω' → T} (hY : Measurable Y)    (hW : Measurable W) (μ : Measure Ω) (μ' : Measure Ω') [IsFiniteMeasure μ'] [FiniteRange W] :    d[X ; μ # Y | W ; μ']      = ∑ w ∈ FiniteRange.toFinset W, μ'.real (W ⁻¹' {w}) * d[X ; μ # Y ; (μ'[|W ← w])] := by  have : ∀ᵐ x ∂Measure.prod (dirac ()) (μ'.map W), x ∈    ((Finset.univ (α := Unit) ×ˢ FiniteRange.toFinset W : Finset (Unit × T)) : Set (Unit × T)) := by    apply Measure.prod_of_full_measure_finset    · simp    rw [Measure.map_apply ‹_› (by measurability)]    convert measure_empty (μ := μ)    simp [← FiniteRange.range]  rw [condRuzsaDist'_def, Kernel.rdist, integral_eq_setIntegral this, setIntegral_finset _ .finset]  simp_rw [Measure.prod_real_singleton, smul_eq_mul, Finset.sum_product]  simp only [Finset.univ_unique, PUnit.default_eq_unit, Finset.sum_singleton]  simp_rw [map_measureReal_apply hW (.singleton _)]  congr with w  by_cases hw : μ'.real (W ⁻¹' {w}) = 0  · simp [hw]  rw [rdist_eq_rdistm, condDistrib_apply hY hW _ _]  · congr    simp  · intro h    simp [h, measureReal_def] at hw