ProbabilityTheory.Kernel.entropy_triple_add_entropy_le'

lemma entropy_triple_add_entropy_le' {κ : Kernel T (S × U × V)} [IsZeroOrMarkovKernel κ]    {μ : Measure T} [IsZeroOrProbabilityMeasure μ] [FiniteSupport μ]    (hκ : AEFiniteKernelSupport κ μ) :    Hk[κ, μ] + Hk[fst κ, μ] ≤ Hk[deleteMiddle κ, μ] + Hk[deleteRight κ, μ] := by  rcases eq_zero_or_isMarkovKernel κ with rfl | hκ'  · simp  rcases eq_zero_or_isProbabilityMeasure μ with rfl | hμ  · simp  have : Nonempty (S × U × V) := nonempty_of_isProbabilityMeasure_of_isMarkovKernel μ κ  inhabit (S × U × V)  have : Nonempty U := ⟨(default : S × U × V).2.1⟩  have : Nonempty V := ⟨(default : S × U × V).2.2⟩  set κ' := map κ MeasurableEquiv.prodAssoc.symm with hκ'_def  set ξ := fst (fst κ') with ξ_def  let κ'' := condKernel (fst κ')  let η := condKernel κ'  have hξ_eq : ξ = fst κ := by    rw [ξ_def, hκ'_def, fst_eq, MeasurableEquiv.prodAssoc, MeasurableEquiv.coe_mk, Equiv.coe_fn_mk,     fst_eq, map_map _ (by fun_prop) (by fun_prop), map_map _ (by fun_prop) (by fun_prop), fst_eq]    rfl  have h_compProd_eq : ξ ⊗ₖ κ'' = fst κ' := (disintegration (fst κ')).symm  have h_compProd_triple_eq : (ξ ⊗ₖ κ'') ⊗ₖ η = κ' := by    rw [h_compProd_eq]    exact (disintegration κ').symm  have h_compProd_triple_eq' :      ξ ⊗ₖ (κ'' ⊗ₖ comap η MeasurableEquiv.prodAssoc MeasurableEquiv.prodAssoc.measurable)        = κ := by    rw [← compProd_assoc', h_compProd_triple_eq,hκ'_def, map_map _ (by fun_prop) (by fun_prop)]    simp  have h := entropy_compProd_triple_add_entropy_le (ξ := ξ) (κ := κ'') (η := η) (μ := μ) ?_ ?_ ?_  rotate_left  · exact aefiniteKernelSupport_of_cond _ hκ.map.fst  · rw [h_compProd_eq]    apply aefiniteKernelSupport_of_cond    exact hκ.map  · exact hκ.map.fst.fst  rw [← hξ_eq]  have h_right : deleteRight κ = fst κ' := by    rw [hκ'_def, deleteRight_eq, fst_eq, map_map _ (by fun_prop) (by fun_prop)]    congr  have h_middle : deleteMiddle κ      = ξ ⊗ₖ snd        (κ'' ⊗ₖ comap η MeasurableEquiv.prodAssoc MeasurableEquiv.prodAssoc.measurable) := by    rw [← deleteMiddle_compProd, h_compProd_triple_eq']  have hκ : Hk[κ, μ] = Hk[κ', μ] := by    rw [hκ'_def, entropy_map_of_injective _ _ _ (by fun_prop)]    exact MeasurableEquiv.prodAssoc.symm.injective  rw [h_right, h_middle, hκ, ← h_compProd_triple_eq, fst_compProd]  · exact h