KLDiv_of_comp_inj

lemma KLDiv_of_comp_inj {H : Type*} [MeasurableSpace H] [DiscreteMeasurableSpace G]    [MeasurableSingletonClass H] {f : G → H}    (hf : Function.Injective f) (hX : Measurable X) (hY : Measurable Y) :    KL[f ∘ X ; μ # f ∘ Y ; μ'] = KL[X ; μ # Y ; μ'] := by  simp only [KLDiv]  rw [← hf.tsum_eq]  · symm    congr with x    have A : (Measure.map X μ) {x} = (Measure.map (f ∘ X) μ) {f x} := by      rw [Measure.map_apply, Measure.map_apply]      · rw [Set.preimage_comp, ← Set.image_singleton, Set.preimage_image_eq _ hf]      · exact .comp .of_discrete hX      · exact measurableSet_singleton (f x)      · exact hX      · exact measurableSet_singleton x    have B : (Measure.map Y μ') {x} = (Measure.map (f ∘ Y) μ') {f x} := by      rw [Measure.map_apply, Measure.map_apply]      · congr        exact Set.Subset.antisymm (fun ⦃a⦄ ↦ congrArg f) fun ⦃a⦄ a_1 ↦ hf a_1      · exact .comp .of_discrete hY      · exact measurableSet_singleton (f x)      · exact hY      · exact measurableSet_singleton x    simp [A, B, measureReal_def]  · intro y hy    have : (μ.map (f ∘ X)).real {y} ≠ 0 := by      intro h      simp [h] at hy    rw [map_measureReal_apply (.comp .of_discrete hX) (.singleton y)] at this    have : f ∘ X ⁻¹' {y} ≠ ∅ := by      intro h      simp [h] at this    obtain ⟨z, hz⟩ := Set.nonempty_iff_ne_empty.2 this    simp only [Set.mem_preimage, Function.comp_apply, Set.mem_singleton_iff] at hz    exact Set.mem_range.2 ⟨X z, hz⟩