condRho_prod_eq_sum

lemma condRho_prod_eq_sum [IsProbabilityMeasure μ] {S : Type*} [MeasurableSpace S]    [Fintype S] [MeasurableSingletonClass S]    {Z T : Ω → S} (hZ : Measurable Z) (hT : Measurable T) :    ρ[X | ⟨Z, T⟩ ; μ # A] = ∑ g, μ.real (T ⁻¹' {g}) * ρ[X | Z ; μ[|T ← g] # A] := by  rw [condRho, tsum_fintype, ← Finset.univ_product_univ, Finset.sum_product_right]  congr 1 with w  simp only [condRho, tsum_fintype, Finset.mul_sum]  congr 1 with w'  rw [← mul_assoc]  have A : (fun a ↦ (Z a, T a)) ⁻¹' {(w', w)} = Z ⁻¹' {w'} ∩ T ⁻¹' {w} := by ext; simp  congr 1  · simp only [A, ProbabilityTheory.cond]    rcases le_or_gt (μ.real (T ⁻¹' {w})) 0 with hw|hw    · have : μ.real (Z ⁻¹' {w'} ∩ T ⁻¹' {w}) = 0 :=        le_antisymm (le_trans (measureReal_mono Set.inter_subset_right) hw) measureReal_nonneg      have hw' : μ.real (T ⁻¹' {w}) = 0 := le_antisymm hw measureReal_nonneg      simp [hw', this]    · simp only [measureReal_ennreal_smul_apply, ENNReal.toReal_inv]      rw [← mul_assoc, ← measureReal_def, mul_inv_cancel₀ hw.ne', one_mul]      rw [measureReal_def, measureReal_def, Measure.restrict_apply]      exact hZ (measurableSet_singleton w')  · congr 1    rw [A, cond_cond_eq_cond_inter' (hT (.singleton _)) (hZ (.singleton _)), Set.inter_comm]    finiteness