ProbabilityTheory.Kernel.entropy_comap

lemma entropy_comap [MeasurableSingletonClass T]    {T' : Type*} [MeasurableSpace T'] [MeasurableSingletonClass T']    (κ : Kernel T S) (μ : Measure T) (f : T' → T) (hf : MeasurableEmbedding f)    (hf_range : Set.range f =ᵐ[μ] Set.univ)    [IsFiniteMeasure μ] [IsFiniteMeasure (μ.comap f)] (hfμ : FiniteSupport (μ.comap f)) :    Hk[comap κ f hf.measurable, μ.comap f] = Hk[κ, μ] := by  classical  rcases hfμ with ⟨A, (hA : ∀ᵐ x ∂μ.comap f, x ∈ A)⟩  have : ∀ᵐ x ∂μ, x ∈ Finset.image f A := by    change μ (Finset.image f A : Set T)ᶜ = 0    simp only [Finset.coe_image, hf.injective.compl_image_eq, measure_union_null_iff]    constructor    · rwa [← Measure.comap_apply f hf.injective hf.measurableSet_image']      exact MeasurableSet.compl (Finset.measurableSet A)    exact ae_eq_univ.mp hf_range  simp_rw [entropy]  simp_rw [integral_eq_setIntegral hA, integral_eq_setIntegral this,    setIntegral_finset _ .finset,    Measure.comap_real_apply hf.injective hf.measurableSet_image' _ (.singleton _)]  simp only [Set.image_singleton, smul_eq_mul]  simp_rw [comap_apply]  rw [← Finset.sum_image (f := fun x ↦ μ.real {x} * measureEntropy (κ x)) (g := f)]  intro x _ y _ hxy  exact hf.injective hxy