# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1672352052 0
# Node ID 25c0d4c0e1105cfeb42bc47b7c819ecde5fc4fc3
# Parent  337c2265d8a238325f7691fa5bb0aeffbf5a6957
More tidying

diff -r 337c2265d8a2 -r 25c0d4c0e110 src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy	Thu Dec 29 16:32:56 2022 +0000
+++ b/src/HOL/Analysis/Measure_Space.thy	Thu Dec 29 22:14:12 2022 +0000
@@ -26,9 +26,9 @@
   proof (rule SUP_eqI)
     fix y :: ennreal assume "\<And>n. n \<in> UNIV \<Longrightarrow> (if i < n then f i else 0) \<le> y"
     from this[of "Suc i"] show "f i \<le> y" by auto
-  qed (insert assms, simp)
+  qed (use assms in simp)
   ultimately show ?thesis using assms
-    by (subst suminf_eq_SUP) (auto simp: indicator_def)
+    by (simp add: suminf_eq_SUP)
 qed
 
 lemma suminf_indicator:
@@ -71,11 +71,8 @@
         by (induct n)  (auto simp add: binaryset_def f)
     qed
   moreover
-  have "... \<longlonglongrightarrow> f A + f B" by (rule tendsto_const)
-  ultimately
-  have "(\<lambda>n. \<Sum>i< Suc (Suc n). f (binaryset A B i)) \<longlonglongrightarrow> f A + f B"
-    by metis
-  hence "(\<lambda>n. \<Sum>i< n+2. f (binaryset A B i)) \<longlonglongrightarrow> f A + f B"
+  have "\<dots> \<longlonglongrightarrow> f A + f B" by (rule tendsto_const)
+  ultimately have "(\<lambda>n. \<Sum>i< n+2. f (binaryset A B i)) \<longlonglongrightarrow> f A + f B"
     by simp
   thus ?thesis by (rule LIMSEQ_offset [where k=2])
 qed
@@ -83,7 +80,7 @@
 lemma binaryset_sums:
   assumes f: "f {} = 0"
   shows  "(\<lambda>n. f (binaryset A B n)) sums (f A + f B)"
-    by (simp add: sums_def LIMSEQ_binaryset [where f=f, OF f] atLeast0LessThan)
+  using LIMSEQ_binaryset f sums_def by blast
 
 lemma suminf_binaryset_eq:
   fixes f :: "'a set \<Rightarrow> 'b::{comm_monoid_add, t2_space}"
@@ -148,7 +145,7 @@
   by (auto simp add: increasing_def)
 
 lemma countably_additiveI[case_names countably]:
-  "(\<And>A. range A \<subseteq> M \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i. A i) \<in> M \<Longrightarrow> (\<Sum>i. f (A i)) = f (\<Union>i. A i))
+  "(\<And>A. \<lbrakk>range A \<subseteq> M; disjoint_family A; (\<Union>i. A i) \<in> M\<rbrakk> \<Longrightarrow> (\<Sum>i. f(A i)) = f(\<Union>i. A i))
   \<Longrightarrow> countably_additive M f"
   by (simp add: countably_additive_def)
 
@@ -198,9 +195,9 @@
   assume xy: "x \<in> M" "y \<in> M" "x \<subseteq> y"
   then have "y - x \<in> M" by auto
   then have "f x + 0 \<le> f x + f (y-x)" by (intro add_left_mono zero_le)
-  also have "... = f (x \<union> (y-x))" using addf
-    by (auto simp add: additive_def) (metis Diff_disjoint Un_Diff_cancel Diff xy(1,2))
-  also have "... = f y"
+  also have "\<dots> = f (x \<union> (y-x))"
+    by (metis addf Diff_disjoint \<open>y - x \<in> M\<close> additiveD xy(1))
+  also have "\<dots> = f y"
     by (metis Un_Diff_cancel Un_absorb1 xy(3))
   finally show "f x \<le> f y" by simp
 qed
@@ -222,9 +219,12 @@
   also have "\<dots> = f (A x) + f ((\<Union>i\<in>F. A i) - A x)"
     using f(2) by (rule additiveD) (insert in_M, auto)
   also have "\<dots> \<le> f (A x) + f (\<Union>i\<in>F. A i)"
-    using additive_increasing[OF f] in_M subs by (auto simp: increasing_def intro: add_left_mono)
-  also have "\<dots> \<le> f (A x) + (\<Sum>i\<in>F. f (A i))" using insert by (auto intro: add_left_mono)
-  finally show "f (\<Union>i\<in>(insert x F). A i) \<le> (\<Sum>i\<in>(insert x F). f (A i))" using insert by simp
+    using additive_increasing[OF f] in_M subs 
+    by (simp add: increasingD)
+  also have "\<dots> \<le> f (A x) + (\<Sum>i\<in>F. f (A i))" 
+    using insert by (auto intro: add_left_mono)
+  finally show "f (\<Union>i\<in>(insert x F). A i) \<le> (\<Sum>i\<in>(insert x F). f (A i))"
+    by (simp add: insert)
 qed
 
 lemma (in ring_of_sets) countably_additive_additive:
@@ -239,10 +239,8 @@
   hence "range (binaryset x y) \<subseteq> M \<longrightarrow>
          (\<Union>i. binaryset x y i) \<in> M \<longrightarrow>
          f (\<Union>i. binaryset x y i) = (\<Sum> n. f (binaryset x y n))"
-    using ca
-    by (simp add: countably_additive_def)
-  hence "{x,y,{}} \<subseteq> M \<longrightarrow> x \<union> y \<in> M \<longrightarrow>
-         f (x \<union> y) = (\<Sum>n. f (binaryset x y n))"
+    using ca by (simp add: countably_additive_def)
+  hence "{x,y,{}} \<subseteq> M \<longrightarrow> x \<union> y \<in> M \<longrightarrow> f (x \<union> y) = (\<Sum>n. f (binaryset x y n))"
     by (simp add: range_binaryset_eq UN_binaryset_eq)
   thus "f (x \<union> y) = f x + f y" using posf x y
     by (auto simp add: Un suminf_binaryset_eq positive_def)
@@ -259,8 +257,8 @@
   fix N
   note disj_N = disjoint_family_on_mono[OF _ disj, of "{..<N}"]
   have "(\<Sum>i<N. f (A i)) = f (\<Union>i\<in>{..<N}. A i)"
-    using A by (intro additive_sum [OF f ad _ _]) (auto simp: disj_N)
-  also have "... \<le> f \<Omega>" using space_closed A
+    using A by (intro additive_sum [OF f ad]) (auto simp: disj_N)
+  also have "\<dots> \<le> f \<Omega>" using space_closed A
     by (intro increasingD[OF inc] finite_UN) auto
   finally show "(\<Sum>i<N. f (A i)) \<le> f \<Omega>" by simp
 qed (insert f A, auto simp: positive_def)
@@ -272,16 +270,10 @@
 proof (rule countably_additiveI)
   fix F :: "nat \<Rightarrow> 'a set" assume F: "range F \<subseteq> M" "(\<Union>i. F i) \<in> M" and disj: "disjoint_family F"
 
-  have "\<forall>i\<in>{i. F i \<noteq> {}}. \<exists>x. x \<in> F i" by auto
-  from bchoice[OF this] obtain f where f: "\<And>i. F i \<noteq> {} \<Longrightarrow> f i \<in> F i" by auto
-
-  have inj_f: "inj_on f {i. F i \<noteq> {}}"
-  proof (rule inj_onI, simp)
-    fix i j a b assume *: "f i = f j" "F i \<noteq> {}" "F j \<noteq> {}"
-    then have "f i \<in> F i" "f j \<in> F j" using f by force+
-    with disj * show "i = j" by (auto simp: disjoint_family_on_def)
-  qed
-  have "finite (\<Union>i. F i)"
+  have "\<forall>i. F i \<noteq> {} \<longrightarrow> (\<exists>x. x \<in> F i)" by auto
+  then obtain f where f: "\<And>i. F i \<noteq> {} \<Longrightarrow> f i \<in> F i" by metis
+
+  have finU: "finite (\<Union>i. F i)"
     by (metis F(2) assms(1) infinite_super sets_into_space)
 
   have F_subset: "{i. \<mu> (F i) \<noteq> 0} \<subseteq> {i. F i \<noteq> {}}"
@@ -290,8 +282,11 @@
   proof (rule finite_imageD)
     from f have "f`{i. F i \<noteq> {}} \<subseteq> (\<Union>i. F i)" by auto
     then show "finite (f`{i. F i \<noteq> {}})"
-      by (rule finite_subset) fact
-  qed fact
+      by (simp add: finU finite_subset)
+    show inj_f: "inj_on f {i. F i \<noteq> {}}" 
+      using f disj
+      by (simp add: inj_on_def disjoint_family_on_def disjoint_iff) metis
+  qed 
   ultimately have fin_not_0: "finite {i. \<mu> (F i) \<noteq> 0}"
     by (rule finite_subset)
 
@@ -323,8 +318,7 @@
   have f_UN: "(\<Sum>i. f (disjointed A i)) = f (\<Union>i. A i)"
     by (auto simp: UN_disjointed_eq disjoint_family_disjointed)
   moreover have "(\<lambda>n. (\<Sum>i<n. f (disjointed A i))) \<longlonglongrightarrow> (\<Sum>i. f (disjointed A i))"
-    using f(1)[unfolded positive_def] dA
-    by (auto intro!: summable_LIMSEQ)
+    by (simp add: summable_LIMSEQ)
   from LIMSEQ_Suc[OF this]
   have "(\<lambda>n. (\<Sum>i\<le>n. f (disjointed A i))) \<longlonglongrightarrow> (\<Sum>i. f (disjointed A i))"
     unfolding lessThan_Suc_atMost .
@@ -332,23 +326,21 @@
     using disjointed_additive[OF f A(1,2)] .
   ultimately show "(\<lambda>i. f (A i)) \<longlonglongrightarrow> f (\<Union>i. A i)" by simp
 next
-  assume cont: "\<forall>A. range A \<subseteq> M \<longrightarrow> incseq A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> f (\<Union>i. A i)"
+  assume cont[rule_format]: "\<forall>A. range A \<subseteq> M \<longrightarrow> incseq A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> f (\<Union>i. A i)"
   fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" "disjoint_family A" "(\<Union>i. A i) \<in> M"
   have *: "(\<Union>n. (\<Union>i<n. A i)) = (\<Union>i. A i)" by auto
-  have "(\<lambda>n. f (\<Union>i<n. A i)) \<longlonglongrightarrow> f (\<Union>i. A i)"
-  proof (unfold *[symmetric], intro cont[rule_format])
-    show "range (\<lambda>i. \<Union>i<i. A i) \<subseteq> M" "(\<Union>i. \<Union>i<i. A i) \<in> M"
-      using A * by auto
-  qed (force intro!: incseq_SucI)
+  have "range (\<lambda>i. \<Union>i<i. A i) \<subseteq> M" "(\<Union>i. \<Union>i<i. A i) \<in> M"
+    using A * by auto
+  then have "(\<lambda>n. f (\<Union>i<n. A i)) \<longlonglongrightarrow> f (\<Union>i. A i)"
+    unfolding *[symmetric] by (force intro!: cont incseq_SucI)+
   moreover have "\<And>n. f (\<Union>i<n. A i) = (\<Sum>i<n. f (A i))"
     using A
-    by (intro additive_sum[OF f, of _ A, symmetric])
-       (auto intro: disjoint_family_on_mono[where B=UNIV])
+    by (intro additive_sum[OF f, symmetric]) (auto intro: disjoint_family_on_mono)
   ultimately
   have "(\<lambda>i. f (A i)) sums f (\<Union>i. A i)"
     unfolding sums_def by simp
-  from sums_unique[OF this]
-  show "(\<Sum>i. f (A i)) = f (\<Union>i. A i)" by simp
+  then show "(\<Sum>i. f (A i)) = f (\<Union>i. A i)"
+    by (metis sums_unique)
 qed
 
 lemma (in ring_of_sets) continuous_from_above_iff_empty_continuous:
@@ -357,13 +349,15 @@
   shows "(\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) \<in> M \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> f (\<Inter>i. A i))
      \<longleftrightarrow> (\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) = {} \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> 0)"
 proof safe
-  assume cont: "(\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) \<in> M \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> f (\<Inter>i. A i))"
-  fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" "decseq A" "(\<Inter>i. A i) = {}" "\<forall>i. f (A i) \<noteq> \<infinity>"
-  with cont[THEN spec, of A] show "(\<lambda>i. f (A i)) \<longlonglongrightarrow> 0"
+  assume cont[rule_format]: "(\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) \<in> M \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> f (\<Inter>i. A i))"
+  fix A :: "nat \<Rightarrow> 'a set" 
+  assume A: "range A \<subseteq> M" "decseq A" "(\<Inter>i. A i) = {}" "\<forall>i. f (A i) \<noteq> \<infinity>"
+  with cont[of A] show "(\<lambda>i. f (A i)) \<longlonglongrightarrow> 0"
     using \<open>positive M f\<close>[unfolded positive_def] by auto
 next
-  assume cont: "\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) = {} \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> 0"
-  fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" "decseq A" "(\<Inter>i. A i) \<in> M" "\<forall>i. f (A i) \<noteq> \<infinity>"
+  assume cont[rule_format]: "\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) = {} \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> 0"
+  fix A :: "nat \<Rightarrow> 'a set" 
+  assume A: "range A \<subseteq> M" "decseq A" "(\<Inter>i. A i) \<in> M" "\<forall>i. f (A i) \<noteq> \<infinity>"
 
   have f_mono: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<subseteq> b \<Longrightarrow> f a \<le> f b"
     using additive_increasing[OF f] unfolding increasing_def by simp
@@ -378,23 +372,19 @@
     using A by (auto intro!: f_mono)
   then have f_Int_fin: "f (\<Inter>x. A x) \<noteq> \<infinity>"
     using A by (auto simp: top_unique)
-  { fix i
-    have "f (A i - (\<Inter>i. A i)) \<le> f (A i)" using A by (auto intro!: f_mono)
-    then have "f (A i - (\<Inter>i. A i)) \<noteq> \<infinity>"
-      using A by (auto simp: top_unique) }
-  note f_fin = this
+  have f_fin: "f (A i - (\<Inter>i. A i)) \<noteq> \<infinity>" for i
+    using A by (metis Diff Diff_subset f_mono infinity_ennreal_def range_subsetD top_unique)
   have "(\<lambda>i. f (A i - (\<Inter>i. A i))) \<longlonglongrightarrow> 0"
-  proof (intro cont[rule_format, OF _ decseq _ f_fin])
+  proof (intro cont[ OF _ decseq _ f_fin])
     show "range (\<lambda>i. A i - (\<Inter>i. A i)) \<subseteq> M" "(\<Inter>i. A i - (\<Inter>i. A i)) = {}"
       using A by auto
   qed
-  from INF_Lim[OF decseq_f this]
-  have "(INF n. f (A n - (\<Inter>i. A i))) = 0" .
+  with INF_Lim decseq_f have "(INF n. f (A n - (\<Inter>i. A i))) = 0" by metis
   moreover have "(INF n. f (\<Inter>i. A i)) = f (\<Inter>i. A i)"
     by auto
   ultimately have "(INF n. f (A n - (\<Inter>i. A i)) + f (\<Inter>i. A i)) = 0 + f (\<Inter>i. A i)"
     using A(4) f_fin f_Int_fin
-    by (subst INF_ennreal_add_const) (auto simp: decseq_f)
+    using INF_ennreal_add_const by presburger
   moreover {
     fix n
     have "f (A n - (\<Inter>i. A i)) + f (\<Inter>i. A i) = f ((A n - (\<Inter>i. A i)) \<union> (\<Inter>i. A i))"
@@ -424,7 +414,8 @@
     also have "((\<Union>i. A i) - A i) \<union> A i = (\<Union>i. A i)"
       by auto
     finally have "f ((\<Union>i. A i) - A i) = f (\<Union>i. A i) - f (A i)"
-      using f(3)[rule_format, of "A i"] A by (auto simp: ennreal_add_diff_cancel subset_eq) }
+      using assms f by fastforce
+  }
   moreover have "\<forall>\<^sub>F i in sequentially. f (A i) \<le> f (\<Union>i. A i)"
     using increasingD[OF additive_increasing[OF f(1, 2)], of "A _" "\<Union>i. A i"] A
     by (auto intro!: always_eventually simp: subset_eq)
@@ -502,17 +493,11 @@
   by (metis emeasure_mono emeasure_notin_sets sets.sets_into_space sets.top zero_le)
 
 lemma emeasure_Diff:
-  assumes finite: "emeasure M B \<noteq> \<infinity>"
-  and [measurable]: "A \<in> sets M" "B \<in> sets M" and "B \<subseteq> A"
+  assumes "emeasure M B \<noteq> \<infinity>"
+  and "A \<in> sets M" "B \<in> sets M" and "B \<subseteq> A"
   shows "emeasure M (A - B) = emeasure M A - emeasure M B"
-proof -
-  have "(A - B) \<union> B = A" using \<open>B \<subseteq> A\<close> by auto
-  then have "emeasure M A = emeasure M ((A - B) \<union> B)" by simp
-  also have "\<dots> = emeasure M (A - B) + emeasure M B"
-    by (subst plus_emeasure[symmetric]) auto
-  finally show "emeasure M (A - B) = emeasure M A - emeasure M B"
-    using finite by simp
-qed
+  by (smt (verit, best) add_diff_self_ennreal assms emeasure_Un emeasure_mono 
+      ennreal_add_left_cancel le_iff_sup)
 
 lemma emeasure_compl:
   "s \<in> sets M \<Longrightarrow> emeasure M s \<noteq> \<infinity> \<Longrightarrow> emeasure M (space M - s) = emeasure M (space M) - emeasure M s"
@@ -563,8 +548,7 @@
   also have "\<dots> = emeasure M (A 0) - emeasure M (\<Inter>i. A i)"
     using A finite * by (simp, subst emeasure_Diff) auto
   finally show ?thesis
-    by (rule ennreal_minus_cancel[rotated 3])
-       (insert finite A, auto intro: INF_lower emeasure_mono)
+    by (smt (verit, best) Inf_lower diff_diff_ennreal le_MI finite range_eqI)
 qed
 
 lemma INF_emeasure_decseq':
@@ -580,7 +564,7 @@
   have "(INF n. emeasure M (A n)) = (INF n. emeasure M (A (n + i)))"
   proof (rule INF_eq)
     show "\<exists>j\<in>UNIV. emeasure M (A (j + i)) \<le> emeasure M (A i')" for i'
-      by (intro bexI[of _ i'] emeasure_mono decseqD[OF \<open>decseq A\<close>] A) auto
+      by (meson A \<open>decseq A\<close> decseq_def emeasure_mono iso_tuple_UNIV_I nat_le_iff_add)
   qed auto
   also have "\<dots> = emeasure M (INF n. (A (n + i)))"
     using A \<open>decseq A\<close> fin by (intro INF_emeasure_decseq) (auto simp: decseq_def less_top)
@@ -1118,7 +1102,7 @@
 
 text \<open>The next lemma is convenient to combine with a lemma whose conclusion is of the
 form \<open>AE x in M. P x = Q x\<close>: for such a lemma, there is no \<open>[symmetric]\<close> variant,
-but using \<open>AE_symmetric[OF...]\<close> will replace it.\<close>
+but using \<open>AE_symmetric[OF\<dots>]\<close> will replace it.\<close>
 
 (* depricated replace by laws about eventually *)
 lemma
@@ -1645,11 +1629,9 @@
   have "emeasure M (A \<union> B) \<noteq> \<infinity>"
     using emeasure_subadditive[OF measurable] fin by (auto simp: top_unique)
   then show "(measure M (A \<union> B)) \<le> (measure M A) + (measure M B)"
-    using emeasure_subadditive[OF measurable] fin
-    apply simp
-    apply (subst (asm) (2 3 4) emeasure_eq_ennreal_measure)
-    apply (auto simp flip: ennreal_plus)
-    done
+    unfolding measure_def
+    by (metis emeasure_subadditive[OF measurable] fin   enn2real_mono enn2real_plus 
+        ennreal_add_less_top infinity_ennreal_def less_top)
 qed
 
 lemma measure_subadditive_finite:
@@ -1672,13 +1654,13 @@
   assumes A: "range A \<subseteq> sets M" and fin: "(\<Sum>i. emeasure M (A i)) \<noteq> \<infinity>"
   shows "measure M (\<Union>i. A i) \<le> (\<Sum>i. measure M (A i))"
 proof -
-  from fin have **: "\<And>i. emeasure M (A i) \<noteq> top"
-    using ennreal_suminf_lessD[of "\<lambda>i. emeasure M (A i)"] by (simp add: less_top)
-  { have "emeasure M (\<Union>i. A i) \<le> (\<Sum>i. emeasure M (A i))"
-      using emeasure_subadditive_countably[OF A] .
-    also have "\<dots> < \<infinity>"
-      using fin by (simp add: less_top)
-    finally have "emeasure M (\<Union>i. A i) \<noteq> top" by simp }
+  have **: "\<And>i. emeasure M (A i) \<noteq> top"
+    using fin ennreal_suminf_lessD[of "\<lambda>i. emeasure M (A i)"] by (simp add: less_top)
+  have ge0: "(\<Sum>i. Sigma_Algebra.measure M (A i)) \<ge> 0"
+    using fin emeasure_eq_ennreal_measure[OF **]
+    by (metis infinity_ennreal_def measure_nonneg suminf_cong suminf_nonneg summable_suminf_not_top)
+  have "emeasure M (\<Union>i. A i) \<noteq> top"
+    by (metis A emeasure_subadditive_countably fin infinity_ennreal_def neq_top_trans)
   then have "ennreal (measure M (\<Union>i. A i)) = emeasure M (\<Union>i. A i)"
     by (rule emeasure_eq_ennreal_measure[symmetric])
   also have "\<dots> \<le> (\<Sum>i. emeasure M (A i))"
@@ -1687,11 +1669,7 @@
     using fin unfolding emeasure_eq_ennreal_measure[OF **]
     by (subst suminf_ennreal) (auto simp: **)
   finally show ?thesis
-    apply (rule ennreal_le_iff[THEN iffD1, rotated])
-    apply (intro suminf_nonneg allI measure_nonneg summable_suminf_not_top)
-    using fin
-    apply (simp add: emeasure_eq_ennreal_measure[OF **])
-    done
+    using ge0 ennreal_le_iff by blast
 qed
 
 lemma measure_Un_null_set: "A \<in> sets M \<Longrightarrow> B \<in> null_sets M \<Longrightarrow> measure M (A \<union> B) = measure M A"
@@ -2038,11 +2016,11 @@
 
     have "emeasure M (B N) \<le> (\<Sum>n\<in>{..<N}. emeasure M (A n))"
       unfolding B_def by (rule emeasure_subadditive_finite, auto)
-    also have "... = (\<Sum>n\<in>{..<N}. ennreal(measure M (A n)))"
+    also have "\<dots> = (\<Sum>n\<in>{..<N}. ennreal(measure M (A n)))"
       using assms(2) by (simp add: emeasure_eq_ennreal_measure less_top)
-    also have "... = ennreal (\<Sum>n\<in>{..<N}. measure M (A n))"
+    also have "\<dots> = ennreal (\<Sum>n\<in>{..<N}. measure M (A n))"
       by auto
-    also have "... \<le> ennreal (\<Sum>n. measure M (A n))"
+    also have "\<dots> \<le> ennreal (\<Sum>n. measure M (A n))"
       using * by (auto simp: ennreal_leI)
     finally show ?thesis by simp
   qed
@@ -2069,9 +2047,9 @@
       have I: "(\<Union>k\<in>{n..}. A k) = (\<Union>k. A (k+n))" by (auto, metis le_add_diff_inverse2, fastforce)
       have "emeasure M (limsup A) \<le> emeasure M (\<Union>k\<in>{n..}. A k)"
         by (rule emeasure_mono, auto simp add: limsup_INF_SUP)
-      also have "... = emeasure M (\<Union>k. A (k+n))"
+      also have "\<dots> = emeasure M (\<Union>k. A (k+n))"
         using I by auto
-      also have "... \<le> (\<Sum>k. measure M (A (k+n)))"
+      also have "\<dots> \<le> (\<Sum>k. measure M (A (k+n)))"
         apply (rule emeasure_union_summable)
         using assms summable_ignore_initial_segment[OF assms(3), of n] by auto
       finally show ?thesis by simp