# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1672484959 0
# Node ID 8d8af7e92c5e676c88f0e9c8c3885ffedee0ca4f
# Parent  4645ca4457db53ea5b61ed32bc9074e1caea60e6
repaired a proof

diff -r 4645ca4457db -r 8d8af7e92c5e src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy	Fri Dec 30 23:21:37 2022 +0000
+++ b/src/HOL/Analysis/Measure_Space.thy	Sat Dec 31 11:09:19 2022 +0000
@@ -3611,7 +3611,7 @@
   proof (intro less_eq_measure.intros(3))
     show "space (sigma \<Omega> (\<Union>M)) = space (SUP m\<in>M. sigma \<Omega> m)"
          "sets (sigma \<Omega> (\<Union>M)) = sets (SUP m\<in>M. sigma \<Omega> m)"
-      by (auto simp add: M sets_Sup_sigma sets_eq_imp_space_eq)
+      by (auto simp add: M sets_Sup_sigma sets_eq_imp_space_eq space_measure_of_conv)
   qed (simp add: emeasure_sigma le_fun_def)
   fix m assume "m \<in> M" then show "sigma \<Omega> m \<le> sigma \<Omega> (\<Union>M)"
     by (subst sigma_le_iff) (auto simp add: M *)