ProbabilityTheory.Kernel.entropy_fst_sub_mutualInfo_le_entropy_map_div

@[to_additive]lemma entropy_fst_sub_mutualInfo_le_entropy_map_div    (κ : 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_div (swapRight κ) μ hκ.swapRight    simp only [snd_swapRight, mutualInfo_swapRight, map_swapRight] at h    refine h.trans_eq ?_    have : (fun p : G × G ↦ p.1 / p.2) ∘ Prod.swap = (fun p ↦ p.2 / p.1) := rfl    simp_rw [this]    rw [← entropy_div_comm]