src/HOL/Analysis/Binary_Product_Measure.thy

   have "\<And>x. x \<in> space M1 \<Longrightarrow> emeasure M (Pair x -` Q) = \<integral>\<^sup>+ y. indicator Q (x, y) \<partial>M"
     by (simp add: sets_Pair1[OF set])
   from this measurable_emeasure_Pair[OF set] show ?case
     by (rule measurable_cong[THEN iffD1])
 qed (simp_all add: nn_integral_add nn_integral_cmult measurable_compose_Pair1
-                   nn_integral_monotone_convergence_SUP incseq_def le_fun_def
+                   nn_integral_monotone_convergence_SUP incseq_def le_fun_def image_comp
               cong: measurable_cong)
 
 lemma (in sigma_finite_measure) nn_integral_fst:
   assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M)"
   shows "(\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. f (x, y) \<partial>M \<partial>M1) = integral\<^sup>N (M1 \<Otimes>\<^sub>M M) f" (is "?I f = _")

     by (intro nn_integral_cong) (auto simp: space_pair_measure)
   with cong show ?case
     by (simp cong: nn_integral_cong)
 qed (simp_all add: emeasure_pair_measure nn_integral_cmult nn_integral_add
                    nn_integral_monotone_convergence_SUP measurable_compose_Pair1
-                   borel_measurable_nn_integral_fst nn_integral_mono incseq_def le_fun_def
+                   borel_measurable_nn_integral_fst nn_integral_mono incseq_def le_fun_def image_comp
               cong: nn_integral_cong)
 
 lemma (in sigma_finite_measure) borel_measurable_nn_integral[measurable (raw)]:
   "case_prod f \<in> borel_measurable (N \<Otimes>\<^sub>M M) \<Longrightarrow> (\<lambda>x. \<integral>\<^sup>+ y. f x y \<partial>M) \<in> borel_measurable N"
   using borel_measurable_nn_integral_fst[of "case_prod f" N] by simp