ProbabilityTheory.measureEntropy_comap

lemma measureEntropy_comap (μ : Measure T) (f : S → T) (hf : MeasurableEmbedding f)    (hf_range : Set.range f =ᵐ[μ] Set.univ) :    Hm[μ.comap f] = Hm[μ] := by  simp_rw [measureEntropy, Measure.ennreal_smul_real_apply,    Measure.comap_real_apply hf.injective hf.measurableSet_image' _ (.singleton _),    Measure.comap_apply f hf.injective hf.measurableSet_image' _ MeasurableSet.univ]  simp only [Set.image_univ, Set.image_singleton, smul_eq_mul]  classical  rw [← tsum_range (f := fun x ↦ negMulLog ((μ (Set.range f))⁻¹.toReal * μ.real {x})) (g := f)    hf.injective, measure_congr hf_range ]  let F (x : T) : ℝ := negMulLog ((μ .univ)⁻¹.toReal * μ.real {x})  change ∑' x : (Set.range f), F x = ∑' x : T, F x  apply tsum_subtype_eq_of_support_subset  intro x hx  contrapose hx  suffices μ {x} = 0 by simp [F, Measure.real, this]  simp only [ae_eq_univ] at hf_range  exact measure_mono_null (by simp [*]) hf_range