src/HOL/Analysis/Bochner_Integration.thy

   proof (rule seq)
     show U': "U' i \<in> borel_measurable M" "\<And>x. 0 \<le> U' i x" for i
       using U by (auto
           intro: borel_measurable_simple_function
           intro!: borel_measurable_enn2real borel_measurable_times
-          simp: U'_def zero_le_mult_iff enn2real_nonneg)
+          simp: U'_def zero_le_mult_iff)
     show "incseq U'"
       using U(2,3)
       by (auto simp: incseq_def le_fun_def image_iff eq_commute U'_def indicator_def enn2real_mono)
 
     fix x assume x: "x \<in> space M"

     moreover have "\<And>z. {y. U' i z = y \<and> y \<in> U' i ` space M \<and> z \<in> space M} = (if z \<in> space M then {U' i z} else {})"
       by auto
     ultimately have U': "(\<lambda>z. \<Sum>y\<in>U' i`space M. y * indicator {x\<in>space M. U' i x = y} z) = U' i"
       by (simp add: U'_def fun_eq_iff)
     have "\<And>x. x \<in> U' i ` space M \<Longrightarrow> 0 \<le> x"
-      by (auto simp: U'_def enn2real_nonneg)
+      by (auto simp: U'_def)
     with fin have "P (\<lambda>z. \<Sum>y\<in>U' i`space M. y * indicator {x\<in>space M. U' i x = y} z)"
     proof induct
       case empty from set[of "{}"] show ?case
         by (simp add: indicator_def[abs_def])
     next

   assumes \<Omega>: "\<Omega> \<inter> space M \<in> sets M"
   shows "simple_bochner_integrable (restrict_space M \<Omega>) f \<longleftrightarrow>
     simple_bochner_integrable M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x)"
   by (simp add: simple_bochner_integrable.simps space_restrict_space
     simple_function_restrict_space[OF \<Omega>] emeasure_restrict_space[OF \<Omega>] Collect_restrict
-    indicator_eq_0_iff conj_ac)
+    indicator_eq_0_iff conj_left_commute)
 
 lemma simple_bochner_integral_restrict_space:
   fixes f :: "_ \<Rightarrow> 'b::real_normed_vector"
   assumes \<Omega>: "\<Omega> \<inter> space M \<in> sets M"
   assumes f: "simple_bochner_integrable (restrict_space M \<Omega>) f"

       have "integrable M (U i)" for i
         using seq.prems by (rule integrable_bound) (insert U_le seq, auto)
       with seq show "\<exists>N. \<forall>n\<ge>N. 0 \<le> integral\<^sup>L M (U n)"
         by auto
     qed
-  qed (auto simp: measure_nonneg integrable_mult_left_iff)
+  qed (auto simp: integrable_mult_left_iff)
   also have "\<dots> = integral\<^sup>L M f"
     using nonneg by (auto intro!: integral_cong_AE)
   finally show ?thesis .
 qed (simp add: not_integrable_integral_eq)
 

   assumes [measurable]: "f \<in> borel_measurable M"
   assumes ae: "AE x in M. f x \<le> ennreal B" "0 \<le> B"
   shows "ennreal (\<integral>x. enn2real (f x) \<partial>M) = (\<integral>\<^sup>+x. f x \<partial>M)"
 proof (subst nn_integral_eq_integral[symmetric])
   show "integrable M (\<lambda>x. enn2real (f x))"
-    using ae by (intro integrable_const_bound[where B=B]) (auto simp: enn2real_leI enn2real_nonneg)
+    using ae by (intro integrable_const_bound[where B=B]) (auto simp: enn2real_leI)
   show "(\<integral>\<^sup>+ x. ennreal (enn2real (f x)) \<partial>M) = integral\<^sup>N M f"
     using ae by (intro nn_integral_cong_AE) (auto simp: le_less_trans[OF _ ennreal_less_top])
-qed (auto simp: enn2real_nonneg)
+qed auto
 
 lemma (in finite_measure) integral_less_AE:
   fixes X Y :: "'a \<Rightarrow> real"
   assumes int: "integrable M X" "integrable M Y"
   assumes A: "(emeasure M) A \<noteq> 0" "A \<in> sets M" "AE x in M. x \<in> A \<longrightarrow> X x \<noteq> Y x"