[STATEMENT]
lemma measurable_Pair_compose_split[measurable_dest]:
  assumes f: "case_prod f \<in> measurable (M1 \<Otimes>\<^sub>M M2) N"
  assumes g: "g \<in> measurable M M1" and h: "h \<in> measurable M M2"
  shows "(\<lambda>x. f (g x) (h x)) \<in> measurable M N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. f (g x) (h x)) \<in> M \<rightarrow>\<^sub>M N
[PROOF STEP]
using measurable_compose[OF measurable_Pair f, OF g h]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. case (g x, h x) of (x, xa) \<Rightarrow> f x xa) \<in> M \<rightarrow>\<^sub>M N

goal (1 subgoal):
 1. (\<lambda>x. f (g x) (h x)) \<in> M \<rightarrow>\<^sub>M N
[PROOF STEP]
by simp