src/HOL/Library/Extended_Nonnegative_Real.thy

 
 lemma sup_continuous_SUP[order_continuous_intros]:
   fixes M :: "_ \<Rightarrow> _ \<Rightarrow> 'a::complete_lattice"
   assumes M: "\<And>i. i \<in> I \<Longrightarrow> sup_continuous (M i)"
   shows  "sup_continuous (SUP i\<in>I. M i)"
-  unfolding sup_continuous_def by (auto simp add: sup_continuousD[OF M] intro: SUP_commute)
+  unfolding sup_continuous_def by (auto simp add: sup_continuousD [OF M] image_comp intro: SUP_commute)
 
 lemma sup_continuous_apply_SUP[order_continuous_intros]:
   fixes M :: "_ \<Rightarrow> _ \<Rightarrow> 'a::complete_lattice"
   shows "(\<And>i. i \<in> I \<Longrightarrow> sup_continuous (M i)) \<Longrightarrow> sup_continuous (\<lambda>x. SUP i\<in>I. M i x)"
   unfolding SUP_apply[symmetric] by (rule sup_continuous_SUP)

 lemma INF_ennreal_add_const:
   fixes f g :: "nat \<Rightarrow> ennreal"
   shows "(INF i. f i + c) = (INF i. f i) + c"
   using continuous_at_Inf_mono[of "\<lambda>x. x + c" "f`UNIV"]
   using continuous_add[of "at_right (Inf (range f))", of "\<lambda>x. x" "\<lambda>x. c"]
-  by (auto simp: mono_def)
+  by (auto simp: mono_def image_comp)
 
 lemma INF_ennreal_const_add:
   fixes f g :: "nat \<Rightarrow> ennreal"
   shows "(INF i. c + f i) = c + (INF i. f i)"
   using INF_ennreal_add_const[of f c] by (simp add: ac_simps)

     by (rule mono_SUP[OF sup_continuous_mono[OF f]])
   from ennreal_Sup_countable_SUP[of "g`I"] \<open>I \<noteq> {}\<close>
   obtain M :: "nat \<Rightarrow> ennreal" where "incseq M" and M: "range M \<subseteq> g ` I" and eq: "(SUP i \<in> I. g i) = (SUP i. M i)"
     by auto
   have "f (SUP i \<in> I. g i) = (SUP i \<in> range M. f i)"
-    unfolding eq sup_continuousD[OF f \<open>mono M\<close>] by simp
+    unfolding eq sup_continuousD[OF f \<open>mono M\<close>] by (simp add: image_comp)
   also have "\<dots> \<le> (SUP i \<in> I. f (g i))"
-    by (insert M, drule SUP_subset_mono) auto
+    by (insert M, drule SUP_subset_mono) (auto simp add: image_comp)
   finally show "f (SUP i \<in> I. g i) \<le> (SUP i \<in> I. f (g i))" .
 qed
 
 lemma ennreal_suminf_SUP_eq:
   fixes f :: "nat \<Rightarrow> nat \<Rightarrow> ennreal"