src/HOL/Probability/Bochner_Integration.thy

   "integrable M f \<Longrightarrow> g \<in> measurable N M \<Longrightarrow> (\<lambda>x. f (g x)) \<in> borel_measurable N"
   using borel_measurable_integrable[measurable] by measurable
 
 lemma integrable_cong:
   "M = N \<Longrightarrow> (\<And>x. x \<in> space N \<Longrightarrow> f x = g x) \<Longrightarrow> integrable M f \<longleftrightarrow> integrable N g"
-  using assms by (simp cong: has_bochner_integral_cong add: integrable.simps)
+  by (simp cong: has_bochner_integral_cong add: integrable.simps)
 
 lemma integrable_cong_AE:
   "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> AE x in M. f x = g x \<Longrightarrow>
     integrable M f \<longleftrightarrow> integrable M g"
   unfolding integrable.simps
   by (intro has_bochner_integral_cong_AE arg_cong[where f=Ex] ext)
 
 lemma integral_cong:
   "M = N \<Longrightarrow> (\<And>x. x \<in> space N \<Longrightarrow> f x = g x) \<Longrightarrow> integral\<^sup>L M f = integral\<^sup>L N g"
-  using assms by (simp cong: has_bochner_integral_cong cong del: if_cong add: lebesgue_integral_def)
+  by (simp cong: has_bochner_integral_cong cong del: if_cong add: lebesgue_integral_def)
 
 lemma integral_cong_AE:
   "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> AE x in M. f x = g x \<Longrightarrow>
     integral\<^sup>L M f = integral\<^sup>L M g"
   unfolding lebesgue_integral_def