ProbabilityTheory.condEntropy_prod_eq_of_indepFun

lemma condEntropy_prod_eq_of_indepFun [Finite T] [Finite U] [IsZeroOrProbabilityMeasure μ]    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) [FiniteRange X]    (h : IndepFun (⟨X, Y⟩) Z μ) :    H[X | ⟨Y, Z⟩ ; μ] = H[X | Y ; μ] := by  cases nonempty_fintype U  rcases eq_zero_or_isProbabilityMeasure μ with rfl | hμ  · simp  rw [condEntropy_prod_eq_sum _ hY hZ]  have : H[X | Y ; μ] = ∑ z, (μ.real (Z ⁻¹' {z})) * H[X | Y ; μ] := by    rw [← Finset.sum_mul, sum_measureReal_preimage_singleton _ fun z _ ↦ hZ <| .singleton z]; simp  rw [this]  congr with w  rcases eq_or_ne (μ (Z ⁻¹' {w})) 0 with hw|hw  · simp [hw, Measure.real]  congr 1  have : IsProbabilityMeasure (μ[|Z ⁻¹' {w}]) := cond_isProbabilityMeasure hw  apply IdentDistrib.condEntropy_eq hX hY hX hY  exact (h.identDistrib_cond (MeasurableSet.singleton w) (hX.prodMk hY) hZ hw).symm