condRuzsaDist'_prod_eq_sum

lemma condRuzsaDist'_prod_eq_sum {X : Ω → G} {Y : Ω' → G} {W W' : Ω' → T}    (μ : Measure Ω) (μ' : Measure Ω') (hY : Measurable Y) (hW' : Measurable W') (hW : Measurable W)    [IsFiniteMeasure μ'] [FiniteRange W] [FiniteRange W'] :    d[X ; μ # Y | ⟨W', W⟩; μ']      = ∑ w ∈ FiniteRange.toFinset W, μ'.real (W ⁻¹' {w}) * d[X ; μ # Y | W' ; (μ'[|W ← w])] := by  have : d[X ; μ # Y | ⟨W', W⟩; μ'] = ∑ w ∈ ((FiniteRange.toFinset W') ×ˢ FiniteRange.toFinset W),    μ'.real ((fun a => (W' a, W a)) ⁻¹' {w}) * d[X; μ # Y; μ'[|(fun a ↦ (W' a, W a)) ⁻¹' {w}]] := by    rw [condRuzsaDist'_eq_sum hY (hW'.prodMk hW)]    apply Finset.sum_subset    · intro (t, t')      simp only [FiniteRange.mem_iff, Prod.mk.injEq, Finset.mem_product, forall_exists_index,        and_imp]      exact fun ω h1 h2 ↦ ⟨⟨ω, h1⟩, ⟨ω, h2⟩⟩    intro (t, t') _ ht    simp only [FiniteRange.mem_iff, Prod.mk.injEq, not_exists, not_and] at ht    have : (fun a => (W' a, W a)) ⁻¹' {(t, t')} = ∅ := by      ext ω      simpa using ht ω    simp [this]  rw [this, Finset.sum_product_right]  congr 1 with w  rw [condRuzsaDist'_eq_sum hY hW', Finset.mul_sum]  congr 1 with w'  rw [← mul_assoc]  have A : (fun a ↦ (W' a, W a)) ⁻¹' {(w', w)} = W' ⁻¹' {w'} ∩ W⁻¹' {w} := by ext; simp  congr 1  · simp only [A, ProbabilityTheory.cond_real_apply (hW (.singleton w))]    obtain hw | hw := eq_or_ne (μ'.real (W ⁻¹' {w})) 0    · have : μ'.real (W' ⁻¹' {w'} ∩ W ⁻¹' {w}) = 0 :=        measureReal_mono_null Set.inter_subset_right hw      simp [hw, this]    · rw [mul_inv_cancel_left₀ hw, Set.inter_comm]  · congr 1    rw [A, cond_cond_eq_cond_inter' (hW (.singleton _)) (hW' (.singleton _)), Set.inter_comm]    finiteness