ProbabilityTheory.chain_rule'

lemma chain_rule' (μ : Measure Ω) [IsZeroOrProbabilityMeasure μ]    (hX : Measurable X) (hY : Measurable Y) [FiniteRange X] [FiniteRange Y] :    H[⟨X, Y⟩ ; μ] = H[X ; μ] + H[Y | X ; μ] := by  rcases eq_zero_or_isProbabilityMeasure μ with rfl | hμ  · simp  have : Nonempty T := Nonempty.map Y (μ.nonempty_of_neZero)  rw [entropy_eq_kernel_entropy, Kernel.chain_rule]  · simp_rw [← Kernel.map_const _ (hX.prodMk hY), Kernel.fst_map_prod _ hY, Kernel.map_const _ hX,      Kernel.map_const _ (hX.prodMk hY)]    congr 1    · rw [Kernel.entropy, integral_dirac]      rfl    · simp_rw [condEntropy_eq_kernel_entropy hY hX]      have : Measure.dirac () ⊗ₘ Kernel.const Unit (μ.map X) = μ.map (fun ω ↦ ((), X ω)) := by        ext s _        rw [Measure.dirac_unit_compProd_const, Measure.map_map measurable_prodMk_left hX]        congr      rw [this, Kernel.entropy_congr (condDistrib_const_unit hX hY μ)]      have : μ.map (fun ω ↦ ((), X ω)) = (μ.map X).map (Prod.mk ()) := by        ext s _        rw [Measure.map_map measurable_prodMk_left hX]        rfl      rw [this, Kernel.entropy_prodMkLeft_unit]  · apply Kernel.FiniteKernelSupport.aefiniteKernelSupport    exact Kernel.finiteKernelSupport_of_const _