ProbabilityTheory.Kernel.entropy_map_le

lemma entropy_map_le    {κ : Kernel T S} [IsZeroOrMarkovKernel κ] {μ : Measure T} [IsZeroOrProbabilityMeasure μ]    (f : S → U) [FiniteSupport μ] (hκ : AEFiniteKernelSupport κ μ) :    Hk[map κ f, μ] ≤ Hk[κ, μ] := by  rcases eq_zero_or_isMarkovKernel κ with rfl | hκ'  · simp  rcases eq_zero_or_isProbabilityMeasure μ with rfl | hμ  · simp  have : Nonempty S := nonempty_of_isProbabilityMeasure_of_isMarkovKernel μ κ  have : Hk[κ, μ] = Hk[map κ (fun x ↦ (x, f x)), μ] := by    refine (entropy_map_of_injective κ μ (f := fun x ↦ (x, f x)) ?_ (by fun_prop)).symm    intro x y hxy    simp only [Prod.mk.injEq] at hxy    exact hxy.1  rw [this, chain_rule' hκ.map]  simp_rw [snd_map_prod κ measurable_id', le_add_iff_nonneg_right]  exact entropy_nonneg _ _