condRuszaDist_prod_eq_of_indepFun

lemma condRuszaDist_prod_eq_of_indepFun {μ : Measure Ω} {μ' : Measure Ω'} {X : Ω → G} {Y : Ω' → G}    {W W' : Ω' → T} (hX : Measurable X) (hY : Measurable Y) (hW : Measurable W)    (hW' : Measurable W') (h : IndepFun (⟨Y, W⟩) W' μ')    [IsProbabilityMeasure μ'] [Finite T] :    d[X ; μ # Y | ⟨W, W'⟩ ; μ'] = d[X ; μ # Y | W ; μ'] := by  cases nonempty_fintype T  rw [condRuzsaDist'_prod_eq_sum' _ _ hY hW hW']  have : d[X ; μ # Y | W ; μ'] = ∑ z, μ'.real (W' ⁻¹' {z}) * d[X ; μ # Y | W ; μ'] := by    rw [← Finset.sum_mul, sum_measureReal_preimage_singleton _ fun _ _ ↦ hW' <| .singleton _]    simp  rw [this]  congr with w  obtain hw | hw := eq_or_ne (μ'.real (W' ⁻¹' {w})) 0  · simp [hw]  congr 1  apply condRuzsaDist'_of_copy _ hY hW _ hY hW (IdentDistrib.refl hX.aemeasurable)    (h.identDistrib_cond (MeasurableSet.singleton w) (hY.prodMk hW) hW' ?_).symm  intro h  simp [measureReal_def, h] at hw