src/HOL/Analysis/Lebesgue_Measure.thy

           by (intro Min_in) auto
         then obtain m where m: "m \<in> S" "l m < r m" "l m = Min (l ` {i\<in>S. l i < r i})"
           by fastforce
 
         have "(\<Sum>i\<in>S. F (r i) - F (l i)) = (F (r m) - F (l m)) + (\<Sum>i\<in>S - {m}. F (r i) - F (l i))"
-          using m psubset by (intro setsum.remove) auto
+          using m psubset by (intro sum.remove) auto
         also have "(\<Sum>i\<in>S - {m}. F (r i) - F (l i)) \<le> F b - F (r m)"
         proof (intro psubset.IH)
           show "S - {m} \<subset> S"
             using \<open>m\<in>S\<close> by auto
           show "r m \<le> b"

             done
           with \<open>j \<in> S\<close> have "F v - F u \<le> (\<Sum>i\<in>S - {j}. F (r i) - F (l i))"
             by (intro psubset) auto
           also have "\<dots> \<le> (\<Sum>i\<in>S. F (r i) - F (l i))"
             using psubset.prems
-            by (intro setsum_mono2 psubset) (auto intro: less_imp_le)
+            by (intro sum_mono2 psubset) (auto intro: less_imp_le)
           finally show ?thesis .
         next
           assume "\<not> ?R"
           then have j: "u \<le> r j" "l j \<le> v" "\<And>i. i \<in> S - {j} \<Longrightarrow> r i < r j \<or> l i > l j"
             by (auto simp: not_less)
           let ?S1 = "{i \<in> S. l i < l j}"
           let ?S2 = "{i \<in> S. r i > r j}"
 
           have "(\<Sum>i\<in>S. F (r i) - F (l i)) \<ge> (\<Sum>i\<in>?S1 \<union> ?S2 \<union> {j}. F (r i) - F (l i))"
             using \<open>j \<in> S\<close> \<open>finite S\<close> psubset.prems j
-            by (intro setsum_mono2) (auto intro: less_imp_le)
+            by (intro sum_mono2) (auto intro: less_imp_le)
           also have "(\<Sum>i\<in>?S1 \<union> ?S2 \<union> {j}. F (r i) - F (l i)) =
             (\<Sum>i\<in>?S1. F (r i) - F (l i)) + (\<Sum>i\<in>?S2 . F (r i) - F (l i)) + (F (r j) - F (l j))"
             using psubset(1) psubset.prems(1) j
-            apply (subst setsum.union_disjoint)
+            apply (subst sum.union_disjoint)
             apply simp_all
-            apply (subst setsum.union_disjoint)
+            apply (subst sum.union_disjoint)
             apply auto
             apply (metis less_le_not_le)
             done
           also (xtrans) have "(\<Sum>i\<in>?S1. F (r i) - F (l i)) \<ge> F (l j) - F u"
             using \<open>j \<in> S\<close> \<open>finite S\<close> psubset.prems j

       apply (frule Sprop2)
       apply (subgoal_tac "delta i > 0")
       apply arith
       by (rule deltai_gt0)
     also have "... \<le> (\<Sum>i \<in> S. F(r i) - F(l i) + epsilon / 2^(i+2))"
-      apply (rule setsum_mono)
+      apply (rule sum_mono)
       apply simp
       apply (rule order_trans)
       apply (rule less_imp_le)
       apply (rule deltai_prop)
       by auto
     also have "... = (\<Sum>i \<in> S. F(r i) - F(l i)) +
         (epsilon / 4) * (\<Sum>i \<in> S. (1 / 2)^i)" (is "_ = ?t + _")
-      by (subst setsum.distrib) (simp add: field_simps setsum_distrib_left)
+      by (subst sum.distrib) (simp add: field_simps sum_distrib_left)
     also have "... \<le> ?t + (epsilon / 4) * (\<Sum> i < Suc n. (1 / 2)^i)"
       apply (rule add_left_mono)
       apply (rule mult_left_mono)
-      apply (rule setsum_mono2)
+      apply (rule sum_mono2)
       using egt0 apply auto
       by (frule Sbound, auto)
     also have "... \<le> ?t + (epsilon / 2)"
       apply (rule add_left_mono)
       apply (subst geometric_sum)

       apply (rule aux2)
       done
     also have "... = (\<Sum>i\<in>S. F (r i) - F (l i)) + epsilon"
       by auto
     also have "... \<le> (\<Sum>i\<le>n. F (r i) - F (l i)) + epsilon"
-      using finS Sbound Sprop by (auto intro!: add_right_mono setsum_mono3)
+      using finS Sbound Sprop by (auto intro!: add_right_mono sum_mono3)
     finally have "ennreal (F b - F a) \<le> (\<Sum>i\<le>n. ennreal (F (r i) - F (l i))) + epsilon"
-      using egt0 by (simp add: ennreal_plus[symmetric] setsum_nonneg del: ennreal_plus)
+      using egt0 by (simp add: ennreal_plus[symmetric] sum_nonneg del: ennreal_plus)
     then show "ennreal (F b - F a) \<le> (\<Sum>i. ennreal (F (r i) - F (l i))) + (epsilon :: real)"
-      by (rule order_trans) (auto intro!: add_mono setsum_le_suminf simp del: setsum_ennreal)
+      by (rule order_trans) (auto intro!: add_mono sum_le_suminf simp del: sum_ennreal)
   qed
   moreover have "(\<Sum>i. ennreal (F (r i) - F (l i))) \<le> ennreal (F b - F a)"
     using \<open>a \<le> b\<close> by (auto intro!: suminf_le_const ennreal_le_iff[THEN iffD2] claim1)
   ultimately show "(\<Sum>n. ennreal (F (r n) - F (l n))) = ennreal (F b - F a)"
     by (rule antisym[rotated])

 
 lemma lborel_affine:
   fixes t :: "'a::euclidean_space"
   shows "c \<noteq> 0 \<Longrightarrow> lborel = density (distr lborel borel (\<lambda>x. t + c *\<^sub>R x)) (\<lambda>_. \<bar>c\<bar>^DIM('a))"
   using lborel_affine_euclidean[where c="\<lambda>_::'a. c" and t=t]
-  unfolding scaleR_scaleR[symmetric] scaleR_setsum_right[symmetric] euclidean_representation setprod_constant by simp
+  unfolding scaleR_scaleR[symmetric] scaleR_sum_right[symmetric] euclidean_representation setprod_constant by simp
 
 lemma lborel_real_affine:
   "c \<noteq> 0 \<Longrightarrow> lborel = density (distr lborel borel (\<lambda>x. t + c * x)) (\<lambda>_. ennreal (abs c))"
   using lborel_affine[of c t] by simp
 

     by (auto simp: fun_eq_iff)
   then show ?thesis by auto
 next
   assume "x \<noteq> 0" then show ?thesis
     using lebesgue_affine_measurable[of "\<lambda>_. x" 0]
-    unfolding scaleR_scaleR[symmetric] scaleR_setsum_right[symmetric] euclidean_representation
+    unfolding scaleR_scaleR[symmetric] scaleR_sum_right[symmetric] euclidean_representation
     by (auto simp add: ac_simps)
 qed
 
 lemma
   fixes m :: real and \<delta> :: "'a::euclidean_space"

       by (auto intro: inv_unique_comp o_bij)
     then have eq: "T m \<delta> ` S = T (1 / m) ((-1/m) *\<^sub>R \<delta>) -` S \<inter> space lebesgue"
       using bij_vimage_eq_inv_image[OF \<open>bij ?T'\<close>, of S] by auto
 
     have trans_eq_T: "(\<lambda>x. \<delta> + (\<Sum>j\<in>Basis. (m * (x \<bullet> j)) *\<^sub>R j)) = T m \<delta>" for m \<delta>
-      unfolding T_def[abs_def] scaleR_scaleR[symmetric] scaleR_setsum_right[symmetric]
+      unfolding T_def[abs_def] scaleR_scaleR[symmetric] scaleR_sum_right[symmetric]
       by (auto simp add: euclidean_representation ac_simps)
 
     have T[measurable]: "T r d \<in> lebesgue \<rightarrow>\<^sub>M lebesgue" for r d
       using lebesgue_affine_measurable[of "\<lambda>_. r" d]
       by (cases "r = 0") (auto simp: trans_eq_T T_def[abs_def])