\begin{lemma}[Kullback--Leibler and injections]\label{kl-div-inj}\lean{KLDiv_of_comp_inj}\leanok  If $f:G \to H$ is an injection, then $D_{KL}(f(X)\Vert f(Y)) = D_{KL}(X\Vert Y)$.
\end{lemma}
\begin{proof}\leanok\uses{kl-div} Clear from definition.
\end{proof}
/-- If $f:G \to H$ is an injection, then $D_{KL}(f(X)\Vert f(Y)) = D_{KL}(X\Vert Y)$. -/
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 : (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 :  (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
    congr
  · intro y hy
    have : Measure.map (f ∘ X) μ {y} ≠ 0 := by
      intro h
      simp [h] at hy
    rw [Measure.map_apply (.comp .of_discrete hX) (measurableSet_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⟩