# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1596982699 -3600
# Node ID 5de9a5fbf2ec135565576c87ab6cf200062a48ae
# Parent  cf8399df4d76bbdeb25de077aabf402f01f488f8
adjustments for fewer WO assumptions

diff -r cf8399df4d76 -r 5de9a5fbf2ec src/HOL/Cardinals/Cardinal_Order_Relation.thy
--- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Sun Aug 09 13:18:40 2020 +0100
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Sun Aug 09 15:18:19 2020 +0100
@@ -1124,7 +1124,7 @@
   then obtain f where "inj_on f {x. x < m} \<and> f ` {x. x < m} \<le> {x. x < n}"
   unfolding ordLeq_def using
     embed_inj_on[OF natLeq_on_Well_order[of m], of "natLeq_on n", unfolded Field_natLeq_on]
-     embed_Field[OF natLeq_on_Well_order[of m], of "natLeq_on n", unfolded Field_natLeq_on] by blast
+     embed_Field Field_natLeq_on by blast
   thus "m \<le> n" using atLeastLessThan_less_eq2
     unfolding atLeast_0 atLeastLessThan_def lessThan_def Int_UNIV_left by blast
 next
diff -r cf8399df4d76 -r 5de9a5fbf2ec src/HOL/Cardinals/Ordinal_Arithmetic.thy
--- a/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Sun Aug 09 13:18:40 2020 +0100
+++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Sun Aug 09 15:18:19 2020 +0100
@@ -1405,11 +1405,12 @@
       case False
       from assms obtain f where f: "embed r s f" unfolding ordLeq_def by blast
       hence f_underS: "\<forall>a\<in>Field r. f a \<in> Field s \<and> f ` underS r a \<subseteq> underS s (f a)"
-        using embed_in_Field[OF rt.rWELL f] embed_underS2[OF rt.rWELL st.rWELL f] by auto
+        using embed_in_Field embed_underS2 rt.rWELL by fastforce
       from f \<open>t \<noteq> {}\<close> False have *: "Field r \<noteq> {}" "Field s \<noteq> {}" "Field t \<noteq> {}"
         unfolding Field_def embed_def under_def bij_betw_def by auto
       with f obtain x where "s.zero = f x" "x \<in> Field r" unfolding embed_def bij_betw_def
-        using embed_in_Field[OF r.WELL f] s.zero_under subsetD[OF under_Field[of r]] by blast
+        using s.zero_under subsetD[OF under_Field[of r]]
+        by (metis (no_types, lifting) f_inv_into_f f_underS inv_into_into r.zero_in_Field)
       with f have fz: "f r.zero = s.zero" and inj: "inj_on f (Field r)" and compat: "compat r s f"
         unfolding embed_iff_compat_inj_on_ofilter[OF r s] compat_def
         by (fastforce intro: s.leq_zero_imp)+
diff -r cf8399df4d76 -r 5de9a5fbf2ec src/HOL/Cardinals/Wellorder_Constructions.thy
--- a/src/HOL/Cardinals/Wellorder_Constructions.thy	Sun Aug 09 13:18:40 2020 +0100
+++ b/src/HOL/Cardinals/Wellorder_Constructions.thy	Sun Aug 09 15:18:19 2020 +0100
@@ -441,9 +441,9 @@
 subsection \<open>Limit and succesor ordinals\<close>
 
 lemma embed_underS2:
-assumes r: "Well_order r" and s: "Well_order s"  and g: "embed r s g" and a: "a \<in> Field r"
+assumes r: "Well_order r" and g: "embed r s g" and a: "a \<in> Field r"
 shows "g ` underS r a = underS s (g a)"
-using embed_underS[OF assms] unfolding bij_betw_def by auto
+  by (meson a bij_betw_def embed_underS g r)
 
 lemma bij_betw_insert:
 assumes "b \<notin> A" and "f b \<notin> A'" and "bij_betw f A A'"
@@ -1071,8 +1071,8 @@
 qed
 
 corollary oproj_ordLeq:
-assumes r: "Well_order r" and s: "Well_order s" and f: "oproj r s f"
-shows "s \<le>o r"
-using oproj_embed[OF assms] r s unfolding ordLeq_def by auto
+  assumes r: "Well_order r" and s: "Well_order s" and f: "oproj r s f"
+  shows "s \<le>o r"
+  using oproj_embed[OF assms] r s unfolding ordLeq_def by auto
 
 end