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