src/HOL/Analysis/Measure_Space.thy

   shows "AE x in M. Q x = P x"
   using assms by auto
 
 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")
   shows "emeasure M {x\<in>space M. P x} = emeasure M (space M)"
 proof -

   by (cases "A \<in> M") (auto simp: measure_notin_sets emeasure_notin_sets)
 
 lemma enn2real_plus:"a < top \<Longrightarrow> b < top \<Longrightarrow> enn2real (a + b) = enn2real a + enn2real b"
   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"
   shows "measure M A = measure M B"