ProbabilityTheory.condMutualInfo_of_inj_map

lemma condMutualInfo_of_inj_map [Countable U] [IsZeroOrProbabilityMeasure μ]    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)    {V : Type*} [MeasurableSpace V] [MeasurableSingletonClass V] [Countable V]    (f : U → S → V) (hf : ∀ t, Function.Injective (f t)) [FiniteRange Z] :    I[fun ω ↦ f (Z ω) (X ω) : Y | Z ; μ] =    I[X : Y | Z ; μ] := by  have hM : Measurable (Function.uncurry f ∘ ⟨Z, X⟩) := by fun_prop  have hM : Measurable fun ω ↦ f (Z ω) (X ω) := hM  rw [condMutualInfo_eq hM hY hZ, condMutualInfo_eq hX hY hZ]  let g : U → (S × T) → (V × T) := fun z (x, y) ↦ (f z x, y)  have hg : ∀ t, Function.Injective (g t) :=    fun _ _ _ h ↦ Prod.ext_iff.2 ⟨hf _ (Prod.ext_iff.1 h).1, (Prod.ext_iff.1 h).2⟩  rw [← condEntropy_of_injective μ (hX.prodMk hY) hZ g hg, ← condEntropy_of_injective μ hX hZ _ hf]