cond_entropy_indep

lemma cond_entropy_indep {Ω : Type*} [hΩ : MeasureSpace Ω] {S T U : Type*}    {X : Ω → S} {Y : Ω → T} {Z : Ω → U}    [MeasurableSpace S] [MeasurableSingletonClass S] [Finite S]    [MeasurableSpace T] [MeasurableSingletonClass T] [Finite T]    [MeasurableSpace U] [MeasurableSingletonClass U] [Finite U]    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)    [IsZeroOrProbabilityMeasure hΩ.volume] (hindep : IndepFun (⟨X, Y⟩) Z) :    H[X | ⟨Y, Z⟩] = H[X | Y] := by  have h1 : H[X | ⟨Y, Z⟩] = H[⟨X, ⟨Y, Z⟩⟩] - H[⟨Y, Z⟩] :=    chain_rule'' _ (by fun_prop) (by fun_prop)  have h2 : H[X | Y] = H[⟨X, Y⟩] - H[Y] := chain_rule'' _ (by fun_prop) (by fun_prop)  have h3 : H[⟨X, ⟨Y, Z⟩⟩] = H[⟨⟨X, Y⟩, Z⟩] :=    entropy_of_comp_eq_of_comp _ (by fun_prop) (by fun_prop)    (fun x ↦ ⟨⟨x.1, x.2.1⟩, x.2.2⟩) (fun x ↦ ⟨x.1.1, ⟨x.1.2, x.2⟩⟩) (by rfl) (by rfl)  have h4 : H[⟨⟨X, Y⟩, Z⟩] = H[⟨X, Y⟩] + H[Z] :=    hindep.entropy_pair_eq_add (by fun_prop) (by fun_prop)  have h5 : H[⟨Y, Z⟩] = H[Y] + H[Z] := by    apply IndepFun.entropy_pair_eq_add <;> try fun_prop    exact IndepFun.comp (φ := fun x ↦ x.2) (ψ := id) hindep (by fun_prop) (by fun_prop)  linarith