ProbabilityTheory.Kernel.rdist_triangle_aux1

lemma rdist_triangle_aux1 (κ : Kernel T G) (η : Kernel T' G)    [IsMarkovKernel κ] [IsMarkovKernel η]    (μ : Measure T) (μ' : Measure T') (μ'' : Measure T'')    [IsProbabilityMeasure μ] [IsProbabilityMeasure μ'] [IsProbabilityMeasure μ'']    [FiniteSupport μ] [FiniteSupport μ'] [FiniteSupport μ''] :    Hk[map (prodMkRight T' (prodMkRight T'' κ) ×ₖ prodMkLeft (T × T'') η)          (fun p ↦ p.1 - p.2), (μ.prod μ'').prod μ']      = Hk[map (prodMkRight T' κ ×ₖ prodMkLeft T η) (fun x ↦ x.1 - x.2),        μ.prod μ'] := by  have hAB : ∀ᵐ x ∂(μ.prod μ'), x ∈ ((μ.support ×ˢ μ'.support : Finset (T × T')) : Set (T × T')) :=    Measure.prod_of_full_measure_finset (measure_compl_support μ) (measure_compl_support μ')  have hAC : (μ.prod μ'') ((μ.support ×ˢ μ''.support : Finset (T × T'')) : Set (T × T''))ᶜ = 0 :=    Measure.prod_of_full_measure_finset (measure_compl_support μ) (measure_compl_support μ'')  have hACB : ∀ᵐ x ∂(μ.prod μ'').prod μ', x ∈      (((μ.support ×ˢ μ''.support) ×ˢ μ'.support : Finset ((T × T'') × T')) : Set ((T × T'') × T'))        := Measure.prod_of_full_measure_finset hAC (measure_compl_support μ')  simp_rw [entropy, integral_eq_setIntegral hAB, integral_eq_setIntegral hACB,    setIntegral_finset _ .finset, smul_eq_mul, Measure.prod_real_singleton, Finset.sum_product,    mul_assoc, ← Finset.mul_sum]  congr with x  have : ∀ z y, map (prodMkRight T' (prodMkRight T'' κ) ×ₖ prodMkLeft (T × T'') η)        (fun p ↦ p.1 - p.2) ((x, z), y)      = map (prodMkRight T' κ ×ₖ prodMkLeft T η) (fun p ↦ p.1 - p.2) (x, y) := by    intro z y    ext s hs    rw [map_apply' _ (by fun_prop) _ hs, map_apply' _ (by fun_prop) _ hs, prod_apply, prod_apply]    simp  simp_rw [this, ← Finset.sum_mul, sum_measureReal_singleton, Measure.real,    measure_of_measure_compl_eq_zero (measure_compl_support μ'')]  simp