ProbabilityTheory.condEntropy_prod_eq_sum

lemma condEntropy_prod_eq_sum {X : Ω → S} {Y : Ω → T} {Z : Ω → T'} [MeasurableSpace T']    [MeasurableSingletonClass T']    (μ : Measure Ω) (hY : Measurable Y) (hZ : Measurable Z)    [IsFiniteMeasure μ] [Finite T] [Fintype T'] :    H[X | ⟨Y, Z⟩ ; μ] = ∑ z, μ.real (Z ⁻¹' {z}) * H[X | Y ; μ[|Z ⁻¹' {z}]] := by  cases nonempty_fintype T  simp_rw [condEntropy_eq_sum_fintype _ _ _ (hY.prodMk hZ), condEntropy_eq_sum_fintype _ _ _ hY,    Fintype.sum_prod_type_right, Finset.mul_sum, ← mul_assoc]  congr with y  congr with x  have A : (fun a ↦ (Y a, Z a)) ⁻¹' {(x, y)} = Z ⁻¹' {y} ∩ Y ⁻¹' {x} := by    ext p; simp [and_comm]  congr 2  · rw [cond_real_apply (hZ (.singleton y)), A]    obtain hy | hy := eq_or_ne (μ.real (Z ⁻¹' {y})) 0    · have : μ.real (Z ⁻¹' {y} ∩ Y ⁻¹' {x}) = 0 :=        measureReal_mono_null Set.inter_subset_left hy (by finiteness)      simp [this, hy]    · rw [mul_inv_cancel_left₀ hy]  · rw [A, cond_cond_eq_cond_inter (hZ (.singleton y)) (hY (.singleton x))]