condRuzsaDist_eq_sum

lemma condRuzsaDist_eq_sum {X : Ω → G} {Z : Ω → S} {Y : Ω' → G} {W : Ω' → T}    (hX : Measurable X) (hZ : Measurable Z) (hY : Measurable Y) (hW : Measurable W)    (μ : Measure Ω) [IsFiniteMeasure μ] (μ' : Measure Ω') [IsFiniteMeasure μ']    [FiniteRange Z] [FiniteRange W] :    d[X | Z ; μ # Y | W ; μ']      = ∑ z ∈ FiniteRange.toFinset Z, ∑ w ∈ FiniteRange.toFinset W,        μ.real (Z ⁻¹' {z}) * μ'.real (W ⁻¹' {w})          * d[X ; (μ[|Z ← z]) # Y ; (μ'[|W ← w])] := by  have : ∀ᵐ x ∂Measure.prod (μ.map Z) (μ'.map W), x ∈    ((((FiniteRange.toFinset Z) ×ˢ (FiniteRange.toFinset W)) : Finset (S × T)): Set (S × T)) := by    apply Measure.prod_of_full_measure_finset    all_goals {      rw [Measure.map_apply ‹_›]      convert measure_empty (μ := μ)      simp [← FiniteRange.range]      measurability    }  rw [condRuzsaDist_def, Kernel.rdist, integral_eq_setIntegral this, setIntegral_finset _ .finset]  simp_rw [Measure.prod_real_singleton, smul_eq_mul, Finset.sum_product,    map_measureReal_apply hZ (.singleton _), map_measureReal_apply hW (.singleton _)]  congr with z  congr with w  by_cases hz : μ.real (Z ⁻¹' {z}) = 0  · simp only [mul_eq_mul_left_iff, mul_eq_zero]    refine Or.inr (Or.inl ?_)    simp [hz]  by_cases hw : μ'.real (W ⁻¹' {w}) = 0  · simp only [mul_eq_mul_left_iff, mul_eq_zero]    refine Or.inr (Or.inr ?_)    simp [hw]  congr 1  simp only [Measure.real, ENNReal.toReal_eq_zero_iff, measure_ne_top μ, or_false,    measure_ne_top] at hz hw  rw [rdist_eq_rdistm, condDistrib_apply hX hZ _ _ hz, condDistrib_apply hY hW _ _ hw]