rdist_le_sum_fibre

lemma rdist_le_sum_fibre {Z_1 : Ω → H} {Z_2 : Ω' → H}  (h1 : Measurable Z_1) (h2 : Measurable Z_2) [FiniteRange Z_1] [FiniteRange Z_2] :  d[π ∘ Z_1; μ # π ∘ Z_2; μ'] + d[Z_1|π∘Z_1; μ # Z_2|π∘Z_2; μ'] ≤ d[Z_1; μ # Z_2; μ'] := by  obtain ⟨ν, W_1, W_2, hν, m1, m2, hi, hi1, hi2, _, _⟩ := independent_copies_finiteRange h1 h2 μ μ'  have hπ : Measurable π := .of_discrete  have hφ : Measurable (fun x ↦ (x, π x)) := .of_discrete  have hπ1 : IdentDistrib (⟨Z_1, π ∘ Z_1⟩) (⟨W_1, π ∘ W_1⟩) μ ν := hi1.symm.comp hφ  have hπ2 : IdentDistrib (⟨Z_2, π ∘ Z_2⟩) (⟨W_2, π ∘ W_2⟩) μ' ν := hi2.symm.comp hφ  rw [← hi1.rdist_congr hi2, ← (hi1.comp hπ).rdist_congr (hi2.comp hπ),    rdist_of_indep_eq_sum_fibre π hi m1 m2,    condRuzsaDist_of_copy h1 (hπ.comp h1) h2 (hπ.comp h2) m1 (hπ.comp m1) m2 (hπ.comp m2) hπ1 hπ2]  exact le_add_of_nonneg_right (condMutualInfo_nonneg (by fun_prop) (by fun_prop))