rdist_of_indep_eq_sum_fibre

lemma rdist_of_indep_eq_sum_fibre {Z_1 Z_2 : Ω → H} (h : IndepFun Z_1 Z_2 μ)    (h1 : Measurable Z_1) (h2 : Measurable Z_2) [FiniteRange Z_1] [FiniteRange Z_2] :    d[Z_1; μ # Z_2; μ] = d[π ∘ Z_1; μ # π ∘ Z_2; μ] + d[Z_1|π∘Z_1; μ # Z_2|π∘Z_2; μ]      + I[Z_1-Z_2 : ⟨π∘Z_1, π∘Z_2⟩ | π∘(Z_1 - Z_2); μ] := by  have hπ : Measurable π := .of_discrete  have step1 : d[Z_1; μ # Z_2; μ] = d[π ∘ Z_1; μ # π ∘ Z_2; μ] +      H[(Z_1 - Z_2)| π ∘ (Z_1 - Z_2); μ] - H[Z_1 | π ∘ Z_1; μ] / 2 - H[Z_2 | π ∘ Z_2; μ] / 2 := by    have hsub : H[(Z_1 - Z_2)| π ∘ (Z_1 - Z_2); μ] = H[(Z_1 - Z_2); μ] - H[π ∘ (Z_1 - Z_2); μ] :=      condEntropy_comp_self (by fun_prop) hπ    rw [h.rdist_eq h1 h2, (h.comp hπ hπ).rdist_eq (hπ.comp h1) (hπ.comp h2),      condEntropy_comp_self h1 hπ, condEntropy_comp_self h2 hπ, hsub, map_comp_sub π]    ring_nf  have m0 : Measurable (fun x ↦ (x, π x)) := .of_discrete  have h' : IndepFun (⟨Z_1, π ∘ Z_1⟩) (⟨Z_2, π ∘ Z_2⟩) μ := h.comp m0 m0  have m1 : Measurable (Z_1 - Z_2) := h1.sub h2  have m2 : Measurable (⟨↑π ∘ Z_1, ↑π ∘ Z_2⟩) := (hπ.comp h1).prodMk (hπ.comp h2)  have m3 : Measurable (↑π ∘ (Z_1 - Z_2)) := hπ.comp m1  have entroplem : H[Z_1 - Z_2|⟨⟨↑π ∘ Z_1, ↑π ∘ Z_2⟩, ↑π ∘ (Z_1 - Z_2)⟩; μ]      = H[Z_1 - Z_2|⟨↑π ∘ Z_1, ↑π ∘ Z_2⟩; μ] := by    rw [map_comp_sub π]    let f : H' × H' → (H' × H') × H' := fun (x,y) ↦ ((x,y), x - y)    have hf : Injective f := fun _ _ h ↦ (Prod.ext_iff.1 h).1    have mf : Measurable f := measurable_id.prodMk measurable_sub    refine condEntropy_of_injective' μ m1 m2 f hf (mf.comp m2)  rw [step1, condMutualInfo_eq' m1 m2 m3, entroplem,    condRuzsaDist_of_indep h1 (hπ.comp h1) h2 (hπ.comp h2) μ h']  ring_nf