diff -r b58a575d211e -r 62e47f06d22c src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy
--- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Sun Mar 03 20:27:42 2019 +0100
+++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Tue Mar 05 07:00:21 2019 +0000
@@ -386,7 +386,7 @@
         by (simp add: real)
     qed }
   ultimately show ?thesis
-    by (intro exI[of _ "\<lambda>i x. ennreal (f i x)"]) auto
+    by (intro exI [of _ "\<lambda>i x. ennreal (f i x)"]) (auto simp add: image_comp)
 qed
 
 lemma borel_measurable_implies_simple_function_sequence':
@@ -394,7 +394,8 @@
   assumes u: "u \<in> borel_measurable M"
   obtains f where
     "\<And>i. simple_function M (f i)" "incseq f" "\<And>i x. f i x < top" "\<And>x. (SUP i. f i x) = u x"
-  using borel_measurable_implies_simple_function_sequence[OF u] by (auto simp: fun_eq_iff) blast
+  using borel_measurable_implies_simple_function_sequence [OF u]
+  by (metis SUP_apply)
 
 lemma%important simple_function_induct
     [consumes 1, case_names cong set mult add, induct set: simple_function]:
@@ -481,7 +482,7 @@
 proof%unimportant (induct rule: borel_measurable_implies_simple_function_sequence')
   fix U assume U: "\<And>i. simple_function M (U i)" "incseq U" "\<And>i x. U i x < top" and sup: "\<And>x. (SUP i. U i x) = u x"
   have u_eq: "u = (SUP i. U i)"
-    using u sup by auto
+    using u by (auto simp add: image_comp sup)
 
   have not_inf: "\<And>x i. x \<in> space M \<Longrightarrow> U i x < top"
     using U by (auto simp: image_iff eq_commute)
@@ -1538,7 +1539,7 @@
     using N by auto
   from f show ?thesis
     apply induct
-    apply (simp_all add: nn_integral_add nn_integral_cmult nn_integral_monotone_convergence_SUP N)
+    apply (simp_all add: nn_integral_add nn_integral_cmult nn_integral_monotone_convergence_SUP N image_comp)
     apply (auto intro!: nn_integral_cong cong: nn_integral_cong simp: N(2)[symmetric])
     done
 qed
@@ -1667,7 +1668,7 @@
     by (subst nn_integral_cong[OF eq])
        (auto simp add: emeasure_distr intro!: nn_integral_indicator[symmetric] measurable_sets)
 qed (simp_all add: measurable_compose[OF T] T nn_integral_cmult nn_integral_add
-                   nn_integral_monotone_convergence_SUP le_fun_def incseq_def)
+                   nn_integral_monotone_convergence_SUP le_fun_def incseq_def image_comp)
 
 subsubsection%unimportant \<open>Counting space\<close>
 
@@ -2198,7 +2199,7 @@
   have eq: "AE x in M. f x * (SUP i. U i x) = (SUP i. f x * U i x)"
     by eventually_elim (simp add: SUP_mult_left_ennreal seq)
   from seq f show ?case
-    apply (simp add: nn_integral_monotone_convergence_SUP)
+    apply (simp add: nn_integral_monotone_convergence_SUP image_comp)
     apply (subst nn_integral_cong_AE[OF eq])
     apply (subst nn_integral_monotone_convergence_SUP_AE)
     apply (auto simp: incseq_def le_fun_def intro!: mult_left_mono)
@@ -2500,7 +2501,7 @@
 next
   case (seq U)
   thus ?case
-    by(simp add: nn_integral_monotone_convergence_SUP SUP_mult_left_ennreal)
+    by(simp add: nn_integral_monotone_convergence_SUP SUP_mult_left_ennreal image_comp)
 qed simp
 
 end