# HG changeset patch
# User wenzelm
# Date 1470083807 -7200
# Node ID ba972a7dbeba4c150c64d9f14988ffd57c227e30
# Parent  b9bd9e61fd633c07ee4dd6570d75ae4bb4754a14
tuned proof;

diff -r b9bd9e61fd63 -r ba972a7dbeba src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Mon Aug 01 22:11:29 2016 +0200
+++ b/src/HOL/Complete_Lattices.thy	Mon Aug 01 22:36:47 2016 +0200
@@ -1293,25 +1293,25 @@
     and bij: "\<And>i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)"
   shows "bij_betw f (\<Union>i \<in> I. A i) (\<Union>i \<in> I. A' i)"
   unfolding bij_betw_def
-proof auto  (* slow *)
+proof safe
   have "\<And>i. i \<in> I \<Longrightarrow> inj_on f (A i)"
     using bij bij_betw_def[of f] by auto
-  then show "inj_on f (\<Union>i \<in> I. A i)"
+  then show "inj_on f (UNION I A)"
     using chain inj_on_UNION_chain[of I A f] by auto
 next
   fix i x
   assume *: "i \<in> I" "x \<in> A i"
-  then have "f x \<in> A' i"
-    using bij bij_betw_def[of f] by auto
-  with * show "\<exists>j \<in> I. f x \<in> A' j" by blast
+  with bij have "f x \<in> A' i"
+    by (auto simp: bij_betw_def)
+  with * show "f x \<in> UNION I A'" by blast
 next
   fix i x'
   assume *: "i \<in> I" "x' \<in> A' i"
-  then have "\<exists>x \<in> A i. x' = f x"
-    using bij bij_betw_def[of f] by blast
+  with bij have "\<exists>x \<in> A i. x' = f x"
+    unfolding bij_betw_def by blast
   with * have "\<exists>j \<in> I. \<exists>x \<in> A j. x' = f x"
     by blast
-  then show "x' \<in> f ` (\<Union>x\<in>I. A x)"
+  then show "x' \<in> f ` UNION I A"
     by blast
 qed