# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1519383151 0
# Node ID 4fa9d5ef95bc661c5892cb1728392bef5e7858eb
# Parent  19c77698a48dfadaa6945baf817ad83f5c487355
fixed the proof of pair_measure_count_space

diff -r 19c77698a48d -r 4fa9d5ef95bc src/HOL/Analysis/Binary_Product_Measure.thy
--- a/src/HOL/Analysis/Binary_Product_Measure.thy	Fri Feb 23 09:28:26 2018 +0000
+++ b/src/HOL/Analysis/Binary_Product_Measure.thy	Fri Feb 23 10:52:31 2018 +0000
@@ -759,18 +759,20 @@
   with A B have fin_Pair: "\<And>x. finite (Pair x -` X)"
     by (intro finite_subset[OF _ B]) auto
   have fin_X: "finite X" using X_subset by (rule finite_subset) (auto simp: A B)
-  have pos_card: "(0::ennreal) < of_nat (card (Pair x -` X)) \<longleftrightarrow> Pair x -` X \<noteq> {}" for x
-    by (auto simp: card_eq_0_iff fin_Pair) blast
-
-  show "emeasure ?P X = emeasure ?C X"
-    using X_subset A fin_Pair fin_X
-    apply (subst B.emeasure_pair_measure_alt[OF X])
+  have card: "0 < card (Pair a -` X)" if "(a, b) \<in> X" for a b
+    using card_gt_0_iff fin_Pair that by auto
+  then have "emeasure ?P X = \<integral>\<^sup>+ x. emeasure (count_space B) (Pair x -` X)
+            \<partial>count_space A"
+    by (simp add: B.emeasure_pair_measure_alt X)
+  also have "... = emeasure ?C X"
     apply (subst emeasure_count_space)
-    apply (auto simp add: emeasure_count_space nn_integral_count_space
-                          pos_card of_nat_sum[symmetric] card_SigmaI[symmetric]
-                simp del: of_nat_sum card_SigmaI
+    using card X_subset A fin_Pair fin_X
+    apply (auto simp add: nn_integral_count_space
+                           of_nat_sum[symmetric] card_SigmaI[symmetric]
+                simp del:  card_SigmaI
                 intro!: arg_cong[where f=card])
     done
+  finally show "emeasure ?P X = emeasure ?C X" .
 qed