diff -r 9207ada0ca31 -r f443ec10447d src/HOL/Library/Countable_Set.thy
--- a/src/HOL/Library/Countable_Set.thy	Thu Aug 30 19:59:36 2018 +0200
+++ b/src/HOL/Library/Countable_Set.thy	Thu Aug 30 17:20:54 2018 +0200
@@ -69,6 +69,11 @@
   then show thesis ..
 qed
 
+lemma countable_infiniteE':
+  assumes "countable A" "infinite A"
+  obtains g where "bij_betw g (UNIV :: nat set) A"
+  using bij_betw_inv[OF countableE_infinite[OF assms]] that by blast
+
 lemma countable_enum_cases:
   assumes "countable S"
   obtains (finite) f :: "'a \<Rightarrow> nat" where "finite S" "bij_betw f S {..<card S}"