src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy

     with u_range show "incseq (\<lambda>i. u x * (emeasure M) (?B' (u x) i))" "\<And>i. 0 \<le> u x * (emeasure M) (?B' (u x) i)"
       using B_mono B_u by (auto intro!: emeasure_mono ereal_mult_left_mono incseq_SucI simp: ereal_zero_le_0_iff)
   next
     show "integral\<^sup>S M u = (\<Sum>i\<in>u ` space M. SUP n. i * (emeasure M) (?B' i n))"
       using measure_conv u_range B_u unfolding simple_integral_def
-      by (auto intro!: setsum.cong SUP_ereal_cmult [symmetric])
+      by (auto intro!: setsum.cong SUP_ereal_mult_left [symmetric])
   qed
   moreover
   have "a * (SUP i. integral\<^sup>S M (?uB i)) \<le> ?S"
-    apply (subst SUP_ereal_cmult [symmetric])
+    apply (subst SUP_ereal_mult_left [symmetric])
   proof (safe intro!: SUP_mono bexI)
     fix i
     have "a * integral\<^sup>S M (?uB i) = (\<integral>\<^sup>Sx. a * ?uB i x \<partial>M)"
       using B `simple_function M u` u_range
       by (subst simple_integral_mult) (auto split: split_indicator)

     { fix x
       { fix i have "a * u i x \<noteq> -\<infinity>" "v i x \<noteq> -\<infinity>" "u i x \<noteq> -\<infinity>" using `0 \<le> a` u(6)[of i x] v(6)[of i x]
           by auto }
       then have "(SUP i. a * u i x + v i x) = a * (SUP i. u i x) + (SUP i. v i x)"
         using `0 \<le> a` u(3) v(3) u(6)[of _ x] v(6)[of _ x]
-        by (subst SUP_ereal_cmult [symmetric, OF u(6) `0 \<le> a`])
+        by (subst SUP_ereal_mult_left [symmetric, OF _ u(6) `0 \<le> a`])
            (auto intro!: SUP_ereal_add
                  simp: incseq_Suc_iff le_fun_def add_mono ereal_mult_left_mono) }
     then show "AE x in M. (SUP i. l i x) = (SUP i. ?L' i x)"
       unfolding l(5) using `0 \<le> a` u(5) v(5) l(5) f(2) g(2)
       by (intro AE_I2) (auto split: split_max)

   also have "\<dots> = (SUP i. a * integral\<^sup>S M (u i) + integral\<^sup>S M (v i))"
     using u(2, 6) v(2, 6) `0 \<le> a` by (auto intro!: arg_cong[where f="SUPREMUM UNIV"] ext)
   finally have "(\<integral>\<^sup>+ x. max 0 (a * f x + g x) \<partial>M) = a * (\<integral>\<^sup>+x. max 0 (f x) \<partial>M) + (\<integral>\<^sup>+x. max 0 (g x) \<partial>M)"
     unfolding l(5)[symmetric] u(5)[symmetric] v(5)[symmetric]
     unfolding l(1)[symmetric] u(1)[symmetric] v(1)[symmetric]
-    apply (subst SUP_ereal_cmult [symmetric, OF pos(1) `0 \<le> a`])
-    apply (subst SUP_ereal_add [symmetric, OF inc not_MInf]) .
+    apply (subst SUP_ereal_mult_left [symmetric, OF _ pos(1) `0 \<le> a`])
+    apply simp
+    apply (subst SUP_ereal_add [symmetric, OF inc not_MInf])
+    .
   then show ?thesis by (simp add: nn_integral_max_0)
 qed
 
 lemma nn_integral_cmult:
   assumes f: "f \<in> borel_measurable M" "0 \<le> c"

   with add f show ?case
     by (auto simp add: nn_integral_add ereal_zero_le_0_iff intro!: nn_integral_add[symmetric])
 next
   case (seq U)
   from f(2) 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_ereal_cmult seq)
+    by eventually_elim (simp add: SUP_ereal_mult_left seq)
   from seq f show ?case
     apply (simp add: nn_integral_monotone_convergence_SUP)
     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!: ereal_mult_left_mono)