condRuzsaDist'_of_indep

lemma condRuzsaDist'_of_indep {X : Ω → G} {Y : Ω → G} {W : Ω → T}    (hX : Measurable X) (hY : Measurable Y) (hW : Measurable W)    (μ : Measure Ω) [IsProbabilityMeasure μ]    (h : IndepFun X (⟨Y, W⟩) μ) [FiniteRange W] :    d[X ; μ # Y | W ; μ] = H[X - Y | W ; μ] - H[X ; μ]/2 - H[Y | W ; μ]/2 := by  have : IsProbabilityMeasure (μ.map W) := isProbabilityMeasure_map hW.aemeasurable  rw [condRuzsaDist'_def, Kernel.rdist_eq', condEntropy_eq_kernel_entropy _ hW,    condEntropy_eq_kernel_entropy hY hW, entropy_eq_kernel_entropy]  rotate_left  · exact hX.sub hY  congr 2  let Z : Ω → Unit := fun _ ↦ ()  rw [← condDistrib_unit_right hX μ]  have h' : IndepFun (⟨X,Z⟩) (⟨Y, W⟩) μ := by    rw [indepFun_iff_measure_inter_preimage_eq_mul]    intro s t hs ht    have : ⟨X, Z⟩ ⁻¹' s = X ⁻¹' ((fun c ↦ (c, ())) ⁻¹' s) := by ext1 y; simp    rw [this]    rw [indepFun_iff_measure_inter_preimage_eq_mul] at h    exact h _ _ (measurable_prodMk_right hs) ht  have h_indep := condDistrib_eq_prod_of_indepFun hX measurable_const hY hW _ h'  have h_meas_eq : μ.map (⟨Z, W⟩) = (Measure.dirac ()).prod (μ.map W) := by    ext s hs    rw [Measure.map_apply (measurable_const.prodMk hW) hs, Measure.prod_apply hs, lintegral_dirac,      Measure.map_apply hW (measurable_prodMk_left hs)]    congr  rw [← h_meas_eq]  have : Kernel.map (Kernel.prodMkRight T (condDistrib X Z μ)        ×ₖ Kernel.prodMkLeft Unit (condDistrib Y W μ)) (fun x ↦ x.1 - x.2)      =ᵐ[μ.map (⟨Z, W⟩)] Kernel.map (condDistrib (⟨X, Y⟩) (⟨Z, W⟩) μ) (fun x ↦ x.1 - x.2) := by    filter_upwards [h_indep] with y hy    conv_rhs => rw [Kernel.map_apply _ (by fun_prop), hy]    rw [← Kernel.mapOfMeasurable_eq_map _ (by fun_prop)]    rfl  rw [Kernel.entropy_congr this]  have : Kernel.map (condDistrib (⟨X, Y⟩) (⟨Z, W⟩) μ) (fun x ↦ x.1 - x.2)      =ᵐ[μ.map (⟨Z, W⟩)] condDistrib (X - Y) (⟨Z, W⟩) μ :=    (condDistrib_comp _ (by fun_prop) (by fun_prop)).symm  rw [Kernel.entropy_congr this]  have h_meas : μ.map (⟨Z, W⟩) = (μ.map W).map (Prod.mk ()) := by    ext s hs    rw [Measure.map_apply measurable_prodMk_left hs, h_meas_eq, Measure.prod_apply hs,      lintegral_dirac]  have h_ker : condDistrib (X - Y) (⟨Z, W⟩) μ      =ᵐ[μ.map (⟨Z, W⟩)] Kernel.prodMkLeft Unit (condDistrib (X - Y) W μ) := by    rw [Filter.EventuallyEq, ae_iff_of_countable]    intro x hx    rw [Measure.map_apply (measurable_const.prodMk hW) (.singleton _)] at hx    ext s hs    have h_preimage_eq : (fun a ↦ (PUnit.unit, W a)) ⁻¹' {x} = W ⁻¹' {x.2} := by      conv_lhs => rw [← Prod.eta x, ← Set.singleton_prod_singleton, Set.mk_preimage_prod]      ext1 y      simp    rw [Kernel.prodMkLeft_apply, condDistrib_apply' _ (measurable_const.prodMk hW) _ _ hx hs,      condDistrib_apply' _ hW _ _ _ hs]    rotate_left    · exact hX.sub hY    · convert hx      exact h_preimage_eq.symm    · exact hX.sub hY    congr  rw [Kernel.entropy_congr h_ker, h_meas, Kernel.entropy_prodMkLeft_unit]