ProbabilityTheory.Kernel.entropy_snd_sub_mutualInfo_le_entropy_map_of_injective

lemma entropy_snd_sub_mutualInfo_le_entropy_map_of_injective {V : Type*} [Countable V]    [MeasurableSpace V] [MeasurableSingletonClass V]    (κ : Kernel T (S × U)) [IsZeroOrMarkovKernel κ] (μ : Measure T) [IsZeroOrProbabilityMeasure μ]    (f : S × U → V) (hfi : ∀ x, Injective (fun y ↦ f (x, y))) [FiniteSupport μ]    (hκ : AEFiniteKernelSupport κ μ) :    Hk[snd κ, μ] - Ik[κ, μ] ≤ Hk[map κ f, μ] := by  rcases eq_zero_or_isMarkovKernel κ with rfl | hκ'  · simp  rcases eq_zero_or_isProbabilityMeasure μ with rfl | hμ'  · simp  have : Nonempty (S × U) := nonempty_of_isProbabilityMeasure_of_isMarkovKernel μ κ  inhabit (S × U)  have : Nonempty U := ⟨(default : S × U).2⟩  have : Nonempty V := ⟨f default⟩  rw [mutualInfo_eq_snd_sub hκ]  have hf : Measurable f := by fun_prop  ring_nf  calc    Hk[condKernel κ, μ ⊗ₘ fst κ] = Hk[snd ((condKernel κ) ⊗ₖ        (deterministic (fun x : (T × S) × U ↦ f (x.1.2, x.2))        .of_discrete)), μ ⊗ₘ fst κ] := by      symm      apply entropy_snd_compProd_deterministic_of_injective _ _ (fun t ↦ hfi t.2)    _ = Hk[condKernel (map κ (fun p ↦ (p.1, f p))),      μ ⊗ₘ fst κ] := entropy_congr (condKernel_map_prodMk_left κ μ f).symm    _ = Hk[condKernel (map κ (fun p ↦ (p.1, f p))),      μ ⊗ₘ fst (map κ (fun p ↦ (p.1, f p)))] := by        congr 2 with x        rw [fst_map_prod _ hf, fst_apply, map_apply _ measurable_fst]    _ ≤ Hk[snd (map κ (fun p ↦ (p.1, f p))), μ] :=      entropy_condKernel_le_entropy_snd hκ.map    _ = Hk[map κ f, μ] := by rw [snd_map_prod _ measurable_fst]