--- 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
--- 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)+
--- 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