# HG changeset patch
# User wenzelm
# Date 1470677640 -7200
# Node ID b2a6a1a49d39a88e1ce2ee1da1717aa7b40bf163
# Parent  3b3ab467427451bfb7856b4c67d6b677d6584364
tuned proof;

diff -r 3b3ab4674274 -r b2a6a1a49d39 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Mon Aug 08 18:55:12 2016 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Mon Aug 08 19:34:00 2016 +0200
@@ -269,17 +269,18 @@
     and card: "card (UNIV :: 'b set) \<noteq> Suc 0"
   shows "finite (UNIV :: 'a set)"
 proof -
-  from fin have finb: "finite (UNIV :: 'b set)"
+  let ?UNIV_b = "UNIV :: 'b set"
+  from fin have "finite ?UNIV_b"
     by (rule finite_fun_UNIVD2)
-  with card have "card (UNIV :: 'b set) \<ge> Suc (Suc 0)"
-    by (cases "card (UNIV :: 'b set)") (auto simp add: card_eq_0_iff)
-  then obtain n where "card (UNIV :: 'b set) = Suc (Suc n)" "n = card (UNIV :: 'b set) - Suc (Suc 0)"
-    by auto
+  with card have "card ?UNIV_b \<ge> Suc (Suc 0)"
+    by (cases "card ?UNIV_b") (auto simp: card_eq_0_iff)
+  then have "card ?UNIV_b = Suc (Suc (card ?UNIV_b - Suc (Suc 0)))"
+    by simp
   then obtain b1 b2 :: 'b where b1b2: "b1 \<noteq> b2"
     by (auto simp: card_Suc_eq)
-  from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1))"
+  from fin have fin': "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1))"
     by (rule finite_imageI)
-  moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1)"
+  have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1)"
   proof (rule UNIV_eq_I)
     fix x :: 'a
     from b1b2 have "x = inv (\<lambda>y. if y = x then b1 else b2) b1"
@@ -287,7 +288,7 @@
     then show "x \<in> range (\<lambda>f::'a \<Rightarrow> 'b. inv f b1)"
       by blast
   qed
-  ultimately show "finite (UNIV :: 'a set)"
+  with fin' show ?thesis
     by simp
 qed