diff -r 8a7053892d8e -r 2b0dca68c3ee src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy	Thu Jul 18 14:08:44 2019 +0100
+++ b/src/HOL/Analysis/Measure_Space.thy	Thu Jul 18 15:40:15 2019 +0100
@@ -1112,7 +1112,7 @@
 
 lemma AE_impI:
   "(P \<Longrightarrow> AE x in M. Q x) \<Longrightarrow> AE x in M. P \<longrightarrow> Q x"
-  by (cases P) auto
+  by fastforce
 
 lemma AE_measure:
   assumes AE: "AE x in M. P x" and sets: "{x\<in>space M. P x} \<in> sets M" (is "?P \<in> sets M")
@@ -1562,6 +1562,9 @@
   by (simp add: enn2real_def plus_ennreal.rep_eq real_of_ereal_add less_top
            del: real_of_ereal_enn2ereal)
 
+lemma enn2real_sum:"(\<And>i. i \<in> I \<Longrightarrow> f i < top) \<Longrightarrow> enn2real (sum f I) = sum (enn2real \<circ> f) I"
+  by (induction I rule: infinite_finite_induct) (auto simp: enn2real_plus)
+
 lemma measure_eq_AE:
   assumes iff: "AE x in M. x \<in> A \<longleftrightarrow> x \<in> B"
   assumes A: "A \<in> sets M" and B: "B \<in> sets M"