ProbabilityTheory.Kernel.entropy_compProd

lemma entropy_compProd [Countable S] [MeasurableSingletonClass S]    [Countable T] [MeasurableSingletonClass T] [MeasurableSingletonClass U] {μ}    [IsFiniteMeasure μ] {κ : Kernel T S} [IsZeroOrMarkovKernel κ]    {η : Kernel (T × S) U} [IsMarkovKernel η] [FiniteSupport μ]    (hκ : AEFiniteKernelSupport κ μ) (hη : AEFiniteKernelSupport η (μ ⊗ₘ κ)) :    Hk[κ ⊗ₖ η, μ] = Hk[κ, μ] + Hk[η, μ ⊗ₘ κ] := by  have h_meas_eq : μ ⊗ₘ hκ.mk = μ ⊗ₘ κ := Measure.compProd_congr hκ.ae_eq_mk.symm  have h_ent1 : Hk[hκ.mk ⊗ₖ hη.mk, μ] = Hk[κ ⊗ₖ η, μ] := by    refine entropy_congr <| compProd_congr_ae hκ.ae_eq_mk.symm ?_    convert hη.ae_eq_mk.symm  have h_ent2 : Hk[hκ.mk, μ] = Hk[κ, μ] := entropy_congr hκ.ae_eq_mk.symm  have h_ent3 : Hk[hη.mk, μ ⊗ₘ hκ.mk] = Hk[η, μ ⊗ₘ κ] := by    rw [h_meas_eq, entropy_congr hη.ae_eq_mk]  rw [← h_ent1, ← h_ent2, ← h_ent3,    entropy_compProd' hκ.finiteKernelSupport_mk hη.finiteKernelSupport_mk]