\begin{lemma}[Kullback--Leibler and conditioning]\label{kl-cond}\lean{condKLDiv_eq}\leanok If $X, Y$ are independent $G$-valued random variables, and $Z$ is another random variable defined on the same sample space as $X$, then
  $$D_{KL}((X|Z)\Vert Y) = D_{KL}(X\Vert Y) + \bbH[X] - \bbH[X|Z].$$
\end{lemma}
\begin{proof}\leanok
  \uses{ckl-div} Compare the terms correspond to each $x\in G$ on both sides.
\end{proof}
lemma condKLDiv_eq {S : Type*} [MeasurableSpace S] [Fintype S] [MeasurableSingletonClass S]
    [Fintype G] [IsZeroOrProbabilityMeasure μ] [IsFiniteMeasure μ']
    {X : Ω → G} {Y : Ω' → G} {Z : Ω → S}
    (hX : Measurable X) (hZ : Measurable Z)
    (habs : ∀ x, μ'.map Y {x} = 0 → μ.map X {x} = 0) :
    KL[ X | Z ; μ # Y ; μ'] = KL[X ; μ # Y ; μ'] + H[X ; μ] - H[ X | Z ; μ] := by
  rcases eq_zero_or_isProbabilityMeasure μ with rfl | hμ
  · simp [condKLDiv, tsum_fintype, KLDiv_eq_sum, Finset.mul_sum, entropy_eq_sum]
  simp only [condKLDiv, tsum_fintype, KLDiv_eq_sum, Finset.mul_sum, entropy_eq_sum]
  rw [Finset.sum_comm, condEntropy_eq_sum_sum_fintype hZ, Finset.sum_comm (α := G),
    ← Finset.sum_add_distrib, ← Finset.sum_sub_distrib]
  congr with g
  simp only [negMulLog, neg_mul, Finset.sum_neg_distrib, mul_neg, sub_neg_eq_add, ← sub_eq_add_neg,
    ← mul_sub]
  simp_rw [← Measure.map_apply hZ (measurableSet_singleton _)]
  have : Measure.map X μ {g} = ∑ x, (Measure.map Z μ {x}) * (Measure.map X μ[|Z ⁻¹' {x}] {g}) := by
    simp_rw [Measure.map_apply hZ (measurableSet_singleton _)]
    have : Measure.map X μ {g} = Measure.map X (∑ x, μ (Z ⁻¹' {x}) • μ[|Z ⁻¹' {x}]) {g} := by
      rw [sum_meas_smul_cond_fiber hZ μ]
    rw [← MeasureTheory.Measure.sum_fintype, Measure.map_sum hX.aemeasurable] at this
    simpa using this
  nth_rewrite 1 [this]
  rw [ENNReal.toReal_sum (by simp [ENNReal.mul_eq_top]), Finset.sum_mul, ← Finset.sum_add_distrib]
  congr with s
  rw [ENNReal.toReal_mul, mul_assoc, ← mul_add, ← mul_add]
  rcases eq_or_ne (Measure.map Z μ {s}) 0 with hs | hs
  · simp [hs]
  rcases eq_or_ne (Measure.map X μ[|Z ⁻¹' {s}] {g}) 0 with hg | hg
  · simp [hg]
  have h'g : (Measure.map X μ[|Z ⁻¹' {s}] {g}).toReal ≠ 0 := by
    simp [ENNReal.toReal_eq_zero_iff, hg]
  congr
  have hXg : μ.map X {g} ≠ 0 := by
    intro h
    rw [this, Finset.sum_eq_zero_iff] at h
    specialize h s (Finset.mem_univ _)
    rw [mul_eq_zero] at h
    tauto
  have hXg' : (μ.map X {g}).toReal ≠ 0 := by simp [ENNReal.toReal_eq_zero_iff, hXg]
  have hYg : μ'.map Y {g} ≠ 0 := fun h ↦ hXg (habs _ h)
  have hYg' : (μ'.map Y {g}).toReal ≠ 0 := by simp [ENNReal.toReal_eq_zero_iff, hYg]
  rw [Real.log_div h'g hYg', Real.log_div hXg' hYg']
  abel