condRho_prod_eq_of_indepFun

lemma condRho_prod_eq_of_indepFun [IsProbabilityMeasure μ]    {X : Ω → G} {S : Type*} [Finite S] [MeasurableSpace S] [MeasurableSingletonClass S]    {W W' : Ω → S} (hX : Measurable X) (hW : Measurable W)    (hW' : Measurable W') (h : IndepFun (⟨X, W⟩) W' μ) :    ρ[X | ⟨W, W'⟩ ; μ # A] = ρ[X | W ; μ # A] := by  cases nonempty_fintype S  rw [condRho_prod_eq_sum hW hW']  have : ρ[X | W ; μ # A] = ∑ z, μ.real (W' ⁻¹' {z}) * ρ[X | W ; μ # A] := by    rw [← Finset.sum_mul, sum_measureReal_preimage_singleton]    · simp    · exact fun y hy ↦ hW' (measurableSet_singleton y)  rw [this]  congr with w  rcases eq_or_ne (μ.real (W' ⁻¹' {w})) 0 with hw|hw  · simp [hw]  congr 1  apply condRho_eq_of_identDistrib hX hW hX hW  simp only [ne_eq, measure_ne_top, not_false_eq_true, measureReal_eq_zero_iff] at hw  exact (h.identDistrib_cond (MeasurableSet.singleton w) (by fun_prop) hW' hw).symm