
diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Library/Infinite_Set.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -64,12 +64,17 @@
 
 lemma infinite_int_iff_infinite_nat_abs: "infinite S \<longleftrightarrow> infinite ((nat \<circ> abs) ` S)"
   for S :: "int set"
-proof -
-  have "inj_on nat (abs ` A)" for A
+proof (unfold Not_eq_iff, rule iffI)
+  assume "finite ((nat \<circ> abs) ` S)"
+  then have "finite (nat ` (abs ` S))"
+    by (simp add: image_image cong: image_cong)
+  moreover have "inj_on nat (abs ` S)"
     by (rule inj_onI) auto
-  then show ?thesis
-    by (auto simp flip: image_comp dest: finite_image_absD finite_imageD)
-qed
+  ultimately have "finite (abs ` S)"
+    by (rule finite_imageD)
+  then show "finite S"
+    by (rule finite_image_absD)
+qed simp
 
 proposition infinite_int_iff_unbounded_le: "infinite S \<longleftrightarrow> (\<forall>m. \<exists>n. \<bar>n\<bar> \<ge> m \<and> n \<in> S)"
   for S :: "int set"




