src/HOL/Analysis/Measure_Space.thy

   have "A ` {a \<in> I. k (B a) = (SUP x\<in>I. k (B x))} =  {a \<in> A ` I. k a = (SUP x\<in>I. k (B x))}"
     using assms(1) by auto
   moreover have "B ` {a \<in> I. k (B a) = (SUP x\<in>I. k (B x))} =  {a \<in> B ` I. k a = (SUP x\<in>I. k (B x))}"
     by auto
   ultimately show ?thesis
-    using assms by (auto simp: Sup_lexord_def Let_def)
+    using assms by (auto simp: Sup_lexord_def Let_def image_comp)
 qed
 
 lemma sets_SUP_cong:
   assumes eq: "\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sets (N i)" shows "sets (SUP i\<in>I. M i) = sets (SUP i\<in>I. N i)"
   unfolding Sup_measure_def

     by (subst sigma_le_iff) (auto simp add: M *)
 qed
 
 lemma SUP_sigma_sigma:
   "M \<noteq> {} \<Longrightarrow> (\<And>m. m \<in> M \<Longrightarrow> f m \<subseteq> Pow \<Omega>) \<Longrightarrow> (SUP m\<in>M. sigma \<Omega> (f m)) = sigma \<Omega> (\<Union>m\<in>M. f m)"
-  using Sup_sigma[of "f`M" \<Omega>] by auto
+  using Sup_sigma[of "f`M" \<Omega>] by (auto simp: image_comp)
 
 lemma sets_vimage_Sup_eq:
   assumes *: "M \<noteq> {}" "f \<in> X \<rightarrow> Y" "\<And>m. m \<in> M \<Longrightarrow> space m = Y"
   shows "sets (vimage_algebra X f (Sup M)) = sets (SUP m \<in> M. vimage_algebra X f m)"
   (is "?IS = ?SI")