ProbabilityTheory.measureEntropy_prod

@[simp]lemma measureEntropy_prod {μ : Measure S} {ν : Measure T} [FiniteSupport μ] [FiniteSupport ν]    [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] [MeasurableSingletonClass T] :    Hm[μ.prod ν] = Hm[μ] + Hm[ν] := by  let A := μ.support  have hA := measure_compl_support μ  let B := ν.support  have hB := measure_compl_support ν  have hC : (μ.prod ν) (A ×ˢ B : Finset (S × T))ᶜ = 0 := by    have : ((A ×ˢ B : Finset (S × T)) : Set (S × T))ᶜ      = ((A : Set S)ᶜ ×ˢ Set.univ) ∪ (Set.univ ×ˢ (B : Set T)ᶜ) := by ext ⟨a, b⟩; simp; tauto    rw [this]    simp [hA, hB, A, B]  have h1 : Hm[μ] = ∑ p ∈ (A ×ˢ B), (negMulLog (μ.real {p.1})) * (ν.real {p.2}) := by    rw [measureEntropy_of_isProbabilityMeasure_finite' hA, Finset.sum_product]    congr with s    dsimp    simp only [← Finset.mul_sum, sum_measureReal_singleton]    suffices ν.real B = ν.real Set.univ by simp at this; simp [this]    apply measureReal_congr    simp [hB, B]  have h2 : Hm[ν] = ∑ p ∈ (A ×ˢ B), (negMulLog (ν.real {p.2})) * (μ.real {p.1}) := by    rw [measureEntropy_of_isProbabilityMeasure_finite' hB, Finset.sum_product_right]    congr with t    dsimp    simp only [← Finset.mul_sum, sum_measureReal_singleton]    suffices μ.real A = μ.real Set.univ by simp at this; simp [this]    apply measureReal_congr    simp [hA, A]  rw [measureEntropy_of_isProbabilityMeasure_finite' hC, h1, h2, ← Finset.sum_add_distrib]  congr with ⟨s, t⟩  simp_rw [← Set.singleton_prod_singleton, measureReal_prod_prod, negMulLog_mul]  ring