ProbabilityTheory.Kernel.entropy_fst_sub_mutualInfo_le_entropy_map_mul

@[to_additive]lemma entropy_fst_sub_mutualInfo_le_entropy_map_mul    (κ : Kernel T (G × G)) [IsZeroOrMarkovKernel κ] (μ : Measure T) [IsZeroOrProbabilityMeasure μ]    [FiniteSupport μ] (hκ : AEFiniteKernelSupport κ μ) :    Hk[fst κ, μ] - Ik[κ, μ] ≤ Hk[map κ (fun p ↦ p.1 * p.2), μ] := by    have h := entropy_snd_sub_mutualInfo_le_entropy_map_mul' (swapRight κ) μ hκ.swapRight    simp only [snd_swapRight, mutualInfo_swapRight, map_swapRight] at h    refine h.trans_eq ?_    have : (fun p : G × G ↦ p.2 * p.1) ∘ Prod.swap = (fun p ↦ p.1 * p.2) := rfl    simp_rw [this]