work on second half

PFR/ForMathlib/Entropy/Basic.lean

@@ -448,6 +448,15 @@ lemma chain_rule'' (μ : Measure Ω) [IsProbabilityMeasure μ] (hX : Measurable
     H[X | Y ; μ] = H[⟨X, Y⟩ ; μ] - H[Y ; μ] := by
   rw [chain_rule μ hX hY, add_sub_cancel']
 
+/-- Two pairs of variables that have the same joint distribution, have the same
+conditional entropy. -/
+lemma IdentDistrib.condEntropy_eq {Ω' : Type*} [MeasurableSpace Ω'] {X Y : Ω → S}
+    {μ' : Measure Ω'} {X' Y' : Ω' → S} [IsProbabilityMeasure μ] [IsProbabilityMeasure μ']
+    (hX : Measurable X) (hY : Measurable Y) (hX' : Measurable X') (hY' : Measurable Y')
+    (h : IdentDistrib (⟨X, Y⟩) (⟨X', Y'⟩) μ μ') : H[X | Y ; μ] = H[X' | Y' ; μ'] := by
+  have : IdentDistrib Y Y' μ μ' := h.comp measurable_snd
+  rw [chain_rule'' _ hX hY, chain_rule'' _ hX' hY', h.entropy_eq, this.entropy_eq]
+
 /-- If $X : \Omega \to S$ and $Y : \Omega \to T$ are random variables, and $f : T \to U$ is an injection then $H[X|f(Y)] = H[X|Y]$.
  -/
 lemma condEntropy_of_injective' [MeasurableSingletonClass S] (μ : Measure Ω) [IsProbabilityMeasure μ]