src/HOL/Cardinals/Constructions_on_Wellorders_Base.thy

 shows "r <o r'"
 proof-
   {assume "r' \<le>o r"
    then obtain h where "inj_on h (Field r') \<and> h ` (Field r') \<le> Field r"
    unfolding ordLeq_def using assms embed_inj_on embed_Field by blast
-   hence False using finite_imageD finite_subset FIN INF by blast
+   hence False using finite_imageD finite_subset FIN INF by metis
   }
   thus ?thesis using WELL WELL' ordLess_or_ordLeq by blast
 qed
 
 

   assume SUB: "A' \<le> Field(dir_image r f)" and NE: "A' \<noteq> {}"
   obtain A where A_def: "A = {a \<in> Field r. f a \<in> A'}" by blast
   have "A \<noteq> {} \<and> A \<le> Field r"
   using A_def dir_image_Field[of r f] SUB NE by blast
   then obtain a where 1: "a \<in> A \<and> (\<forall>b \<in> A. (b,a) \<notin> r)"
-  using WF unfolding wf_eq_minimal2 by blast
+  using WF unfolding wf_eq_minimal2 by metis
   have "\<forall>b' \<in> A'. (b',f a) \<notin> dir_image r f"
   proof(clarify)
     fix b' assume *: "b' \<in> A'" and **: "(b',f a) \<in> dir_image r f"
     obtain b1 a1 where 2: "b' = f b1 \<and> f a = f a1" and
                        3: "(b1,a1) \<in> r \<and> {a1,b1} \<le> Field r"

      {assume Case41: "b1 = c1 \<and> b2 = c2"
       hence ?thesis using * by simp
      }
      moreover
      {assume Case42: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id"
-      hence ?thesis using Case4 0 unfolding bsqr_def by auto
+      hence ?thesis using Case4 0 unfolding bsqr_def by force
      }
      moreover
      {assume Case43: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> (b1,c1) \<in> r - Id"
       hence ?thesis using Case4 0 unfolding bsqr_def by auto
      }