# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1555534425 -3600
# Node ID 269dcea7426c6a12b1576990a7de8abf80e35d04
# Parent  4900351361b0df419fe1c413250918a9dbd68298
moved subset_image_inj into Hilbert_Choice

diff -r 4900351361b0 -r 269dcea7426c src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Wed Apr 17 17:48:28 2019 +0100
+++ b/src/HOL/Hilbert_Choice.thy	Wed Apr 17 21:53:45 2019 +0100
@@ -562,6 +562,27 @@
   shows "inv f = g"
   using fg gf inv_equality[of g f] by (auto simp add: fun_eq_iff)
 
+lemma subset_image_inj:
+  "S \<subseteq> f ` T \<longleftrightarrow> (\<exists>U. U \<subseteq> T \<and> inj_on f U \<and> S = f ` U)"
+proof safe
+  show "\<exists>U\<subseteq>T. inj_on f U \<and> S = f ` U"
+    if "S \<subseteq> f ` T"
+  proof -
+    from that [unfolded subset_image_iff subset_iff]
+    obtain g where g: "\<And>x. x \<in> S \<Longrightarrow> g x \<in> T \<and> x = f (g x)"
+      by (auto simp add: image_iff Bex_def choice_iff')
+    show ?thesis
+    proof (intro exI conjI)
+      show "g ` S \<subseteq> T"
+        by (simp add: g image_subsetI)
+      show "inj_on f (g ` S)"
+        using g by (auto simp: inj_on_def)
+      show "S = f ` (g ` S)"
+        using g image_subset_iff by auto
+    qed
+  qed
+qed blast
+
 
 subsection \<open>Other Consequences of Hilbert's Epsilon\<close>
 
diff -r 4900351361b0 -r 269dcea7426c src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Wed Apr 17 17:48:28 2019 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Wed Apr 17 21:53:45 2019 +0100
@@ -8,27 +8,6 @@
   imports Main
 begin
 
-lemma subset_image_inj:
-  "S \<subseteq> f ` T \<longleftrightarrow> (\<exists>U. U \<subseteq> T \<and> inj_on f U \<and> S = f ` U)"
-proof safe
-  show "\<exists>U\<subseteq>T. inj_on f U \<and> S = f ` U"
-    if "S \<subseteq> f ` T"
-  proof -
-    from that [unfolded subset_image_iff subset_iff]
-    obtain g where g: "\<And>x. x \<in> S \<Longrightarrow> g x \<in> T \<and> x = f (g x)"
-      unfolding image_iff by metis
-    show ?thesis
-    proof (intro exI conjI)
-      show "g ` S \<subseteq> T"
-        by (simp add: g image_subsetI)
-      show "inj_on f (g ` S)"
-        using g by (auto simp: inj_on_def)
-      show "S = f ` (g ` S)"
-        using g image_subset_iff by auto
-    qed
-  qed
-qed blast
-
 subsection \<open>The set of natural numbers is infinite\<close>
 
 lemma infinite_nat_iff_unbounded_le: "infinite S \<longleftrightarrow> (\<forall>m. \<exists>n\<ge>m. n \<in> S)"