ProbabilityTheory.Kernel.entropy_snd_compProd_deterministic_of_injective

lemma entropy_snd_compProd_deterministic_of_injective [MeasurableSingletonClass U]    (κ : Kernel T S) [IsMarkovKernel κ]    (μ : Measure T) {f : T × S → U}    (hf : ∀ t, Function.Injective (fun x ↦ f (t, x))) (hmes : Measurable f) :    Hk[snd (κ ⊗ₖ deterministic f hmes), μ] = Hk[κ, μ] := by  have : ∀ t, snd (κ ⊗ₖ deterministic f hmes) t      = map κ (fun x ↦ f (t, x)) t := by    intro t    ext s hs    rw [snd_apply' _ _ hs, compProd_deterministic_apply, map_apply' _ (by fun_prop) _ hs]    · rfl    · exact measurable_snd hs  simp_rw [entropy]  congr with y  convert measureEntropy_map_of_injective (κ y) _ (hmes.comp measurable_prodMk_left) (hf y)  rw [this y, map_apply _ (by fun_prop)]  rfl