ProbabilityTheory.measureEntropy_map_of_injective

lemma measureEntropy_map_of_injective    (μ : Measure T) (f : T → S) (hf_m : Measurable f) (hf : Function.Injective f) :    Hm[μ.map f] = Hm[μ] := by  have : μ.map f Set.univ = μ Set.univ := by      rw [Measure.map_apply hf_m MeasurableSet.univ]      simp  simp_rw [measureEntropy, Measure.ennreal_smul_real_apply,    map_measureReal_apply hf_m (.singleton _)]  rw [this]  classical  let F (x : S) : ℝ := negMulLog ((μ Set.univ)⁻¹.toReal • μ.real (f ⁻¹' {x}))  have : ∑' x : S, F x      = ∑' x : (f '' Set.univ), F x := by    apply (tsum_subtype_eq_of_support_subset _).symm    intro x hx    contrapose hx    suffices f ⁻¹' {x} = ∅ by simp [F, this]    contrapose! hx    rw [Set.image_univ]    exact hx  rw [this, tsum_image _ hf.injOn, tsum_univ fun x ↦ F (f x)]  congr! with s  ext s'  simpa using hf.eq_iff