# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1673626796 0
# Node ID f33df7529fede86bec0411829b927163a60de985
# Parent  20ab27bc1f3b38cdf19b074cc1d97bf66fc974fb
Substantial simplification of HOL-Cardinals

diff -r 20ab27bc1f3b -r f33df7529fed src/HOL/Cardinals/Order_Union.thy
--- a/src/HOL/Cardinals/Order_Union.thy	Fri Jan 13 11:05:48 2023 +0000
+++ b/src/HOL/Cardinals/Order_Union.thy	Fri Jan 13 16:19:56 2023 +0000
@@ -85,9 +85,7 @@
   assumes FLD: "Field r Int Field r' = {}" and
     TRANS: "trans r" and TRANS': "trans r'"
   shows "trans (r Osum r')"
-  using assms
-  apply (clarsimp simp: trans_def disjoint_iff)
-  by (smt (verit) Domain.DomainI Field_def Osum_def Pair_inject Range.intros Un_iff case_prodE case_prodI mem_Collect_eq)
+  using assms unfolding Osum_def trans_def disjoint_iff Field_iff by blast
 
 lemma Osum_Preorder:
   "\<lbrakk>Field r Int Field r' = {}; Preorder r; Preorder r'\<rbrakk> \<Longrightarrow> Preorder (r Osum r')"
@@ -97,66 +95,7 @@
   assumes FLD: "Field r Int Field r' = {}" and
     AN: "antisym r" and AN': "antisym r'"
   shows "antisym (r Osum r')"
-proof(unfold antisym_def, auto)
-  fix x y assume *: "(x, y) \<in> r \<union>o r'" and **: "(y, x) \<in> r \<union>o r'"
-  show  "x = y"
-  proof-
-    {assume Case1: "(x,y) \<in> r"
-      hence 1: "x \<in> Field r \<and> y \<in> Field r" unfolding Field_def by auto
-      have ?thesis
-      proof-
-        have "(y,x) \<in> r \<Longrightarrow> ?thesis"
-          using Case1 AN antisym_def[of r] by blast
-        moreover
-        {assume "(y,x) \<in> r'"
-          hence "y \<in> Field r'" unfolding Field_def by auto
-          hence False using FLD 1 by auto
-        }
-        moreover
-        have "x \<in> Field r' \<Longrightarrow> False" using FLD 1 by auto
-        ultimately show ?thesis using ** unfolding Osum_def by blast
-      qed
-    }
-    moreover
-    {assume Case2: "(x,y) \<in> r'"
-      hence 2: "x \<in> Field r' \<and> y \<in> Field r'" unfolding Field_def by auto
-      have ?thesis
-      proof-
-        {assume "(y,x) \<in> r"
-          hence "y \<in> Field r" unfolding Field_def by auto
-          hence False using FLD 2 by auto
-        }
-        moreover
-        have "(y,x) \<in> r' \<Longrightarrow> ?thesis"
-          using Case2 AN' antisym_def[of r'] by blast
-        moreover
-        {assume "y \<in> Field r"
-          hence False using FLD 2 by auto
-        }
-        ultimately show ?thesis using ** unfolding Osum_def by blast
-      qed
-    }
-    moreover
-    {assume Case3: "x \<in> Field r \<and> y \<in> Field r'"
-      have ?thesis
-      proof-
-        {assume "(y,x) \<in> r"
-          hence "y \<in> Field r" unfolding Field_def by auto
-          hence False using FLD Case3 by auto
-        }
-        moreover
-        {assume Case32: "(y,x) \<in> r'"
-          hence "x \<in> Field r'" unfolding Field_def by blast
-          hence False using FLD Case3 by auto
-        }
-        moreover
-        have "\<not> y \<in> Field r" using FLD Case3 by auto
-        ultimately show ?thesis using ** unfolding Osum_def by blast
-      qed
-    }
-    ultimately show ?thesis using * unfolding Osum_def by blast
-  qed
-qed
+  using assms by (auto simp: disjoint_iff antisym_def Osum_def Field_def)
 
 lemma Osum_Partial_order:
   "\<lbrakk>Field r Int Field r' = {}; Partial_order r; Partial_order r'\<rbrakk> \<Longrightarrow>
@@ -171,74 +110,24 @@
   unfolding total_on_def  Field_Osum unfolding Osum_def by blast
 
 lemma Osum_Linear_order:
-  "\<lbrakk>Field r Int Field r' = {}; Linear_order r; Linear_order r'\<rbrakk> \<Longrightarrow>
- Linear_order (r Osum r')"
-  unfolding linear_order_on_def using Osum_Partial_order Osum_Total by blast
+  "\<lbrakk>Field r Int Field r' = {}; Linear_order r; Linear_order r'\<rbrakk> \<Longrightarrow> Linear_order (r Osum r')"
+  by (simp add: Osum_Partial_order Osum_Total linear_order_on_def)
 
 lemma Osum_minus_Id1:
   assumes "r \<le> Id"
   shows "(r Osum r') - Id \<le> (r' - Id) \<union> (Field r \<times> Field r')"
-proof-
-  let ?Left = "(r Osum r') - Id"
-  let ?Right = "(r' - Id) \<union> (Field r \<times> Field r')"
-  {fix a::'a and b assume *: "(a,b) \<notin> Id"
-    {assume "(a,b) \<in> r"
-      with * have False using assms by auto
-    }
-    moreover
-    {assume "(a,b) \<in> r'"
-      with * have "(a,b) \<in> r' - Id" by auto
-    }
-    ultimately
-    have "(a,b) \<in> ?Left \<Longrightarrow> (a,b) \<in> ?Right"
-      unfolding Osum_def by auto
-  }
-  thus ?thesis by auto
-qed
+using assms by (force simp: Osum_def)
 
 lemma Osum_minus_Id2:
   assumes "r' \<le> Id"
   shows "(r Osum r') - Id \<le> (r - Id) \<union> (Field r \<times> Field r')"
-proof-
-  let ?Left = "(r Osum r') - Id"
-  let ?Right = "(r - Id) \<union> (Field r \<times> Field r')"
-  {fix a::'a and b assume *: "(a,b) \<notin> Id"
-    {assume "(a,b) \<in> r'"
-      with * have False using assms by auto
-    }
-    moreover
-    {assume "(a,b) \<in> r"
-      with * have "(a,b) \<in> r - Id" by auto
-    }
-    ultimately
-    have "(a,b) \<in> ?Left \<Longrightarrow> (a,b) \<in> ?Right"
-      unfolding Osum_def by auto
-  }
-  thus ?thesis by auto
-qed
+using assms by (force simp: Osum_def)
 
 lemma Osum_minus_Id:
   assumes TOT: "Total r" and TOT': "Total r'" and
     NID: "\<not> (r \<le> Id)" and NID': "\<not> (r' \<le> Id)"
   shows "(r Osum r') - Id \<le> (r - Id) Osum (r' - Id)"
-proof-
-  {fix a a' assume *: "(a,a') \<in> (r Osum r')" and **: "a \<noteq> a'"
-    have "(a,a') \<in> (r - Id) Osum (r' - Id)"
-    proof-
-      {assume "(a,a') \<in> r \<or> (a,a') \<in> r'"
-        with ** have ?thesis unfolding Osum_def by auto
-      }
-      moreover
-      {assume "a \<in> Field r \<and> a' \<in> Field r'"
-        hence "a \<in> Field(r - Id) \<and> a' \<in> Field (r' - Id)"
-          using assms Total_Id_Field by blast
-        hence ?thesis unfolding Osum_def by auto
-      }
-      ultimately show ?thesis using * unfolding Osum_def by fast
-    qed
-  }
-  thus ?thesis by(auto simp add: Osum_def)
-qed
+  using assms Total_Id_Field by (force simp: Osum_def)
 
 lemma wf_Int_Times:
   assumes "A Int B = {}"
@@ -253,11 +142,9 @@
 proof(cases "r \<le> Id \<or> r' \<le> Id")
   assume Case1: "\<not>(r \<le> Id \<or> r' \<le> Id)"
   have "Field(r - Id) Int Field(r' - Id) = {}"
-    using FLD mono_Field[of "r - Id" r]  mono_Field[of "r' - Id" r']
-      Diff_subset[of r Id] Diff_subset[of r' Id] by blast
+    using Case1 FLD TOT TOT' Total_Id_Field by blast
   thus ?thesis
-    using Case1 Osum_minus_Id[of r r'] assms Osum_wf[of "r - Id" "r' - Id"]
-      wf_subset[of "(r - Id) \<union>o (r' - Id)" "(r Osum r') - Id"] by auto
+    by (meson Case1 Osum_minus_Id Osum_wf TOT TOT' WF WF' wf_subset)
 next
   have 1: "wf(Field r \<times> Field r')"
     using FLD by (auto simp add: wf_Int_Times)
diff -r 20ab27bc1f3b -r f33df7529fed src/HOL/Cardinals/Ordinal_Arithmetic.thy
--- a/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Fri Jan 13 11:05:48 2023 +0000
+++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Fri Jan 13 16:19:56 2023 +0000
@@ -8,12 +8,12 @@
 section \<open>Ordinal Arithmetic\<close>
 
 theory Ordinal_Arithmetic
-imports Wellorder_Constructions
+  imports Wellorder_Constructions
 begin
 
 definition osum :: "'a rel \<Rightarrow> 'b rel \<Rightarrow> ('a + 'b) rel"  (infixr "+o" 70)
-where
-  "r +o r' = map_prod Inl Inl ` r \<union> map_prod Inr Inr ` r' \<union>
+  where
+    "r +o r' = map_prod Inl Inl ` r \<union> map_prod Inr Inr ` r' \<union>
      {(Inl a, Inr a') | a a' . a \<in> Field r \<and> a' \<in> Field r'}"
 
 lemma Field_osum: "Field(r +o r') = Inl ` Field r \<union> Inr ` Field r'"
@@ -24,9 +24,10 @@
   unfolding refl_on_def Field_osum unfolding osum_def by blast
 
 lemma osum_trans:
-assumes TRANS: "trans r" and TRANS': "trans r'"
-shows "trans (r +o r')"
-proof(unfold trans_def, safe)
+  assumes TRANS: "trans r" and TRANS': "trans r'"
+  shows "trans (r +o r')"
+  unfolding trans_def
+proof(safe)
   fix x y z assume *: "(x, y) \<in> r +o r'" "(y, z) \<in> r +o r'"
   thus "(x, z) \<in> r +o r'"
   proof (cases x y z rule: sum.exhaust[case_product sum.exhaust sum.exhaust])
@@ -66,9 +67,9 @@
   unfolding linear_order_on_def using osum_Partial_order osum_Total by blast
 
 lemma osum_wf:
-assumes WF: "wf r" and WF': "wf r'"
-shows "wf (r +o r')"
-unfolding wf_eq_minimal2 unfolding Field_osum
+  assumes WF: "wf r" and WF': "wf r'"
+  shows "wf (r +o r')"
+  unfolding wf_eq_minimal2 unfolding Field_osum
 proof(intro allI impI, elim conjE)
   fix A assume *: "A \<subseteq> Inl ` Field r \<union> Inr ` Field r'" and **: "A \<noteq> {}"
   obtain B where B_def: "B = A Int Inl ` Field r" by blast
@@ -113,8 +114,8 @@
 proof(cases "r \<le> Id \<or> r' \<le> Id")
   case False
   thus ?thesis
-  using osum_minus_Id[of r r'] assms osum_wf[of "r - Id" "r' - Id"]
-    wf_subset[of "(r - Id) +o (r' - Id)" "(r +o r') - Id"] by auto
+    using osum_minus_Id[of r r'] assms osum_wf[of "r - Id" "r' - Id"]
+      wf_subset[of "(r - Id) +o (r' - Id)" "(r +o r') - Id"] by auto
 next
   have 1: "wf (Inl ` Field r \<times> Inr ` Field r')" by (rule wf_Int_Times) auto
   case True
@@ -131,13 +132,9 @@
 qed
 
 lemma osum_Well_order:
-assumes WELL: "Well_order r" and WELL': "Well_order r'"
-shows "Well_order (r +o r')"
-proof-
-  have "Total r \<and> Total r'" using WELL WELL' by (auto simp add: order_on_defs)
-  thus ?thesis using assms unfolding well_order_on_def
-    using osum_Linear_order osum_wf_Id by blast
-qed
+  assumes WELL: "Well_order r" and WELL': "Well_order r'"
+  shows "Well_order (r +o r')"
+  by (meson WELL WELL' osum_Linear_order osum_wf_Id well_order_on_def wo_rel.TOTAL wo_rel.intro)
 
 lemma osum_embedL:
   assumes WELL: "Well_order r" and WELL': "Well_order r'"
@@ -162,10 +159,10 @@
   unfolding dir_image_def map_prod_def by auto
 
 lemma map_prod_ordIso: "\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> map_prod f f ` r =o r"
-  unfolding dir_image_alt[symmetric] by (rule ordIso_symmetric[OF dir_image_ordIso])
+  by (metis dir_image_alt dir_image_ordIso ordIso_symmetric)
 
 definition oprod :: "'a rel \<Rightarrow> 'b rel \<Rightarrow> ('a \<times> 'b) rel"  (infixr "*o" 80)
-where "r *o r' = {((x1, y1), (x2, y2)).
+  where "r *o r' = {((x1, y1), (x2, y2)).
   (((y1, y2) \<in> r' - Id \<and> x1 \<in> Field r \<and> x2 \<in> Field r) \<or>
    ((y1, y2) \<in> Restr Id (Field r') \<and> (x1, x2) \<in> r))}"
 
@@ -178,30 +175,7 @@
 lemma oprod_trans:
   assumes "trans r" "trans r'" "antisym r" "antisym r'"
   shows "trans (r *o r')"
-proof(unfold trans_def, safe)
-  fix x y z assume *: "(x, y) \<in> r *o r'" "(y, z) \<in> r *o r'"
-  thus "(x, z) \<in> r *o r'"
-  unfolding oprod_def
-  apply safe
-  apply (metis assms(2) transE)
-  apply (metis assms(2) transE)
-  apply (metis assms(2) transE)
-  apply (metis assms(4) antisymD)
-  apply (metis assms(4) antisymD)
-  apply (metis assms(2) transE)
-  apply (metis assms(4) antisymD)
-  apply (metis Field_def Range_iff Un_iff)
-  apply (metis Field_def Range_iff Un_iff)
-  apply (metis Field_def Range_iff Un_iff)
-  apply (metis Field_def Domain_iff Un_iff)
-  apply (metis Field_def Domain_iff Un_iff)
-  apply (metis Field_def Domain_iff Un_iff)
-  apply (metis assms(1) transE)
-  apply (metis assms(1) transE)
-  apply (metis assms(1) transE)
-  apply (metis assms(1) transE)
-  done
-qed
+  using assms by (clarsimp simp: trans_def antisym_def oprod_def) (metis FieldI1 FieldI2)
 
 lemma oprod_Preorder: "\<lbrakk>Preorder r; Preorder r'; antisym r; antisym r'\<rbrakk> \<Longrightarrow> Preorder (r *o r')"
   unfolding preorder_on_def using oprod_Refl oprod_trans by blast
@@ -219,9 +193,9 @@
   unfolding linear_order_on_def using oprod_Partial_order oprod_Total by blast
 
 lemma oprod_wf:
-assumes WF: "wf r" and WF': "wf r'"
-shows "wf (r *o r')"
-unfolding wf_eq_minimal2 unfolding Field_oprod
+  assumes WF: "wf r" and WF': "wf r'"
+  shows "wf (r *o r')"
+  unfolding wf_eq_minimal2 unfolding Field_oprod
 proof(intro allI impI, elim conjE)
   fix A assume *: "A \<subseteq> Field r \<times> Field r'" and **: "A \<noteq> {}"
   then obtain y where y: "y \<in> snd ` A" "\<forall>y'\<in>snd ` A. (y', y) \<notin> r'"
@@ -285,22 +259,17 @@
 proof(cases "r \<le> Id \<or> r' \<le> Id")
   case False
   thus ?thesis
-  using oprod_minus_Id[of r r'] assms oprod_wf[of "r - Id" "r' - Id"]
-    wf_subset[of "(r - Id) *o (r' - Id)" "(r *o r') - Id"] by auto
+    by (meson TOT TOT' WF WF' oprod_minus_Id oprod_wf wf_subset)
 next
   case True
   thus ?thesis using wf_subset[OF wf_extend_oprod1[OF WF'] oprod_minus_Id1]
-                     wf_subset[OF wf_extend_oprod2[OF WF] oprod_minus_Id2] by auto
+      wf_subset[OF wf_extend_oprod2[OF WF] oprod_minus_Id2] by auto
 qed
 
 lemma oprod_Well_order:
-assumes WELL: "Well_order r" and WELL': "Well_order r'"
-shows "Well_order (r *o r')"
-proof-
-  have "Total r \<and> Total r'" using WELL WELL' by (auto simp add: order_on_defs)
-  thus ?thesis using assms unfolding well_order_on_def
-    using oprod_Linear_order oprod_wf_Id by blast
-qed
+  assumes WELL: "Well_order r" and WELL': "Well_order r'"
+  shows "Well_order (r *o r')"
+  by (meson WELL WELL' linear_order_on_def oprod_Linear_order oprod_wf_Id well_order_on_def)
 
 lemma oprod_embed:
   assumes WELL: "Well_order r" and WELL': "Well_order r'" and "r' \<noteq> {}"
@@ -344,14 +313,8 @@
 
 lemma fun_unequal_in_support:
   assumes "f \<noteq> g" "f \<in> Func A B" "g \<in> Func A C"
-  shows "(support z A f \<union> support z A g) \<inter> {a. f a \<noteq> g a} \<noteq> {}" (is "?L \<inter> ?R \<noteq> {}")
-proof -
-  from assms(1) obtain x where x: "f x \<noteq> g x" by blast
-  hence "x \<in> ?R" by simp
-  moreover from assms(2-3) x have "x \<in> A" unfolding Func_def by fastforce
-  with x have "x \<in> ?L" unfolding support_def by auto
-  ultimately show ?thesis by auto
-qed
+  shows "(support z A f \<union> support z A g) \<inter> {a. f a \<noteq> g a} \<noteq> {}" 
+  using assms by (simp add: Func_def support_def disjoint_iff fun_eq_iff) metis
 
 definition fin_support where
   "fin_support z A = {f. finite (support z A f)}"
@@ -381,18 +344,18 @@
 begin
 
 definition isMaxim :: "'a set \<Rightarrow> 'a \<Rightarrow> bool"
-where "isMaxim A b \<equiv> b \<in> A \<and> (\<forall>a \<in> A. (a,b) \<in> r)"
+  where "isMaxim A b \<equiv> b \<in> A \<and> (\<forall>a \<in> A. (a,b) \<in> r)"
 
 definition maxim :: "'a set \<Rightarrow> 'a"
-where "maxim A \<equiv> THE b. isMaxim A b"
+  where "maxim A \<equiv> THE b. isMaxim A b"
 
 lemma isMaxim_unique[intro]: "\<lbrakk>isMaxim A x; isMaxim A y\<rbrakk> \<Longrightarrow> x = y"
   unfolding isMaxim_def using antisymD[OF ANTISYM, of x y] by auto
 
 lemma maxim_isMaxim: "\<lbrakk>finite A; A \<noteq> {}; A \<subseteq> Field r\<rbrakk> \<Longrightarrow> isMaxim A (maxim A)"
-unfolding maxim_def
+  unfolding maxim_def
 proof (rule theI', rule ex_ex1I[OF _ isMaxim_unique, rotated], assumption+,
-  induct A rule: finite_induct)
+    induct A rule: finite_induct)
   case (insert x A)
   thus ?case
   proof (cases "A = {}")
@@ -426,9 +389,10 @@
   show ?thesis
   proof (cases "(x, maxim A) \<in> r")
     case True
-    with *(2) have "isMaxim (insert x A) (maxim A)" unfolding isMaxim_def
-      using transD[OF TRANS, of _ x "maxim A"] by blast
-    with *(1) True show ?thesis unfolding max2_def by (metis isMaxim_unique)
+    with *(2) have "isMaxim (insert x A) (maxim A)"
+      by (simp add: isMaxim_def)
+    with *(1) True show ?thesis 
+      unfolding max2_def by (metis isMaxim_unique)
   next
     case False
     hence "(maxim A, x) \<in> r" by (metis *(2) assms(3,4) in_mono in_notinI isMaxim_def)
@@ -453,8 +417,8 @@
   next
     case False
     hence "(maxim B, maxim A) \<in> r" by (metis *(2,3) assms(3,6) in_mono in_notinI isMaxim_def)
-    with *(2,3) have "isMaxim (A \<union> B) (maxim A)" unfolding isMaxim_def
-      using transD[OF TRANS, of _ "maxim B" "maxim A"] by blast
+    with *(2,3) have "isMaxim (A \<union> B) (maxim A)"
+      by (metis "*"(1) False Un_iff isMaxim_def isMaxim_unique)
     with *(1) False show ?thesis unfolding max2_def by (metis isMaxim_unique)
   qed
 qed
@@ -462,7 +426,7 @@
 lemma maxim_insert_zero:
   assumes "finite A" "A \<noteq> {}" "A \<subseteq> Field r"
   shows "maxim (insert zero A) = maxim A"
-using assms zero_in_Field maxim_in[OF assms] by (subst maxim_insert[unfolded max2_def]) auto
+  using assms finite.cases in_mono max2_def maxim_in maxim_insert subset_empty zero_in_Field zero_smallest by fastforce
 
 lemma maxim_equality: "isMaxim A x \<Longrightarrow> maxim A = x"
   unfolding maxim_def by (rule the_equality) auto
@@ -495,7 +459,7 @@
 locale wo_rel2 =
   fixes r s
   assumes rWELL: "Well_order r"
-  and     sWELL: "Well_order s"
+    and     sWELL: "Well_order s"
 begin
 
 interpretation r: wo_rel r by unfold_locales (rule rWELL)
@@ -510,7 +474,7 @@
 
 lemma max_fun_diff_alt:
   "s.max_fun_diff f g = s.maxim ((SUPP f \<union> SUPP g) \<inter> {a. f a \<noteq> g a})"
-   unfolding s.max_fun_diff_def fun_diff_alt ..
+  unfolding s.max_fun_diff_def fun_diff_alt ..
 
 lemma isMaxim_max_fun_diff: "\<lbrakk>f \<noteq> g; f \<in> FINFUNC; g \<in> FINFUNC\<rbrakk> \<Longrightarrow>
   s.isMaxim {a \<in> Field s. f a \<noteq> g a} (s.max_fun_diff f g)"
@@ -552,13 +516,7 @@
     hence "(x, ?fg) \<in> s"
     proof (cases "x = ?fg")
       case False show ?thesis
-      proof (rule ccontr)
-        assume "(x, ?fg) \<notin> s"
-        with max_fun_diff_in[OF fg f g] x False have *: "(?fg, x) \<in> s" by (blast intro: s.in_notinI)
-        hence "f x = g x" by (rule max_fun_diff_le_eq[OF _ fg f g False])
-        moreover have "g x = h x" using max_fun_diff_le_eq[OF _ gh g h] False True * by simp
-        ultimately show False using x by simp
-      qed
+        by (metis (mono_tags, lifting) True assms(5-7) max_fun_diff_max mem_Collect_eq x)
     qed (simp add: refl_onD[OF s.REFL])
   }
   ultimately have "s.isMaxim {a \<in> Field s. f a \<noteq> h a} ?fg"
@@ -572,7 +530,7 @@
     case True
     hence *: "f ?gh = g ?gh" by (rule max_fun_diff_le_eq[OF _ fg f g *[symmetric]])
     hence "s.isMaxim {a \<in> Field s. f a \<noteq> h a} ?gh" using isMaxim_max_fun_diff[OF gh g h]
-      isMaxim_max_fun_diff[OF fg f g] transD[OF s.TRANS _ True]
+        isMaxim_max_fun_diff[OF fg f g] transD[OF s.TRANS _ True]
       unfolding s.isMaxim_def by auto
     hence "?fh = ?gh" using isMaxim_max_fun_diff[OF fh f h] by blast
     thus ?thesis using True unfolding s.max2_def by simp
@@ -582,7 +540,7 @@
       by (blast intro: s.in_notinI)
     hence *: "g ?fg = h ?fg" by (rule max_fun_diff_le_eq[OF _ gh g h *])
     hence "s.isMaxim {a \<in> Field s. f a \<noteq> h a} ?fg" using isMaxim_max_fun_diff[OF gh g h]
-      isMaxim_max_fun_diff[OF fg f g] True transD[OF s.TRANS, of _ _ ?fg]
+        isMaxim_max_fun_diff[OF fg f g] True transD[OF s.TRANS, of _ _ ?fg]
       unfolding s.isMaxim_def by auto
     hence "?fh = ?fg" using isMaxim_max_fun_diff[OF fh f h] by blast
     thus ?thesis using False unfolding s.max2_def by simp
@@ -603,8 +561,8 @@
 proof (unfold trans_def, safe)
   fix f g h :: "'b \<Rightarrow> 'a"
   let ?fg = "s.max_fun_diff f g"
-  and ?gh = "s.max_fun_diff g h"
-  and ?fh = "s.max_fun_diff f h"
+    and ?gh = "s.max_fun_diff g h"
+    and ?fh = "s.max_fun_diff f h"
   assume oexp: "(f, g) \<in> oexp" "(g, h) \<in> oexp"
   thus "(f, h) \<in> oexp"
   proof (cases "f = g \<or> g = h")
@@ -619,8 +577,8 @@
       proof (cases "?fg = ?gh \<longrightarrow> f ?fg \<noteq> h ?gh")
         case True
         show ?thesis using max_fun_diff_max2[of f g h, OF True] * \<open>f \<noteq> h\<close> max_fun_diff_in
-          r.max2_iff[OF FINFUNCD FINFUNCD] r.max2_equals1[OF FINFUNCD FINFUNCD] max_fun_diff_le_eq
-          s.in_notinI[OF disjI1] unfolding oexp_def Let_def s.max2_def mem_Collect_eq by safe metis
+            r.max2_iff[OF FINFUNCD FINFUNCD] r.max2_equals1[OF FINFUNCD FINFUNCD] max_fun_diff_le_eq
+            s.in_notinI[OF disjI1] unfolding oexp_def Let_def s.max2_def mem_Collect_eq by safe metis
       next
         case False with * show ?thesis unfolding oexp_def Let_def
           using antisymD[OF r.ANTISYM, of "g ?gh" "h ?gh"] max_fun_diff_in[of g h] by auto
@@ -667,13 +625,7 @@
 lemma const_least:
   assumes "Field r \<noteq> {}" "f \<in> FINFUNC"
   shows "(const, f) \<in> oexp"
-proof (cases "f = const")
-  case True thus ?thesis using refl_onD[OF oexp_Refl] assms(2) unfolding Field_oexp by auto
-next
-  case False
-  with assms show ?thesis using max_fun_diff_in[of f const]
-    unfolding oexp_def Let_def by (auto intro: r.zero_smallest FinFuncD simp: s.max_fun_diff_commute)
-qed
+  using assms const_FINFUNC max_fun_diff max_fun_diff_in oexp_def by fastforce
 
 lemma support_not_const:
   assumes "F \<subseteq> FINFUNC" and "const \<notin> F"
@@ -693,15 +645,15 @@
 qed
 
 lemma maxim_isMaxim_support:
-  assumes f: "F \<subseteq> FINFUNC" and "const \<notin> F"
+  assumes "F \<subseteq> FINFUNC" and "const \<notin> F"
   shows "\<forall>f \<in> F. s.isMaxim (SUPP f) (s.maxim (SUPP f))"
-  using support_not_const[OF assms] by (auto intro!: s.maxim_isMaxim)
+  using assms s.maxim_isMaxim support_not_const by force
 
 lemma oexp_empty2: "Field s = {} \<Longrightarrow> oexp = {(\<lambda>x. undefined, \<lambda>x. undefined)}"
   unfolding oexp_def FinFunc_def fin_support_def support_def by auto
 
 lemma oexp_empty: "\<lbrakk>Field r = {}; Field s \<noteq> {}\<rbrakk> \<Longrightarrow> oexp = {}"
-  unfolding oexp_def FinFunc_def Let_def by auto
+  using FINFUNCD oexp_def by auto
 
 lemma fun_upd_FINFUNC: "\<lbrakk>f \<in> FINFUNC; x \<in> Field s; y \<in> Field r\<rbrakk> \<Longrightarrow> f(x := y) \<in> FINFUNC"
   unfolding FinFunc_def Func_def fin_support_def
@@ -734,7 +686,7 @@
   have const[simp]: "\<And>F. \<lbrakk>const \<in> F; F \<subseteq> FINFUNC\<rbrakk> \<Longrightarrow> \<exists>f0\<in>F. \<forall>f\<in>F. (f0, f) \<in> oexp"
     using const_least[OF Fields(2)] by auto
   show ?thesis
-  unfolding Linear_order_wf_diff_Id[OF oexp_Linear_order] Field_oexp
+    unfolding Linear_order_wf_diff_Id[OF oexp_Linear_order] Field_oexp
   proof (intro allI impI)
     fix A assume A: "A \<subseteq> FINFUNC" "A \<noteq> {}"
     { fix y F
@@ -758,7 +710,7 @@
             hence zField: "z \<in> Field s" unfolding Field_def by auto
             define x0 where "x0 = r.minim {f z | f. f \<in> F \<and> z = s.maxim (SUPP f)}"
             from F(1,2) maxF(1) SUPPF zmin
-              have x0min: "r.isMinim {f z | f. f \<in> F \<and> z = s.maxim (SUPP f)} x0"
+            have x0min: "r.isMinim {f z | f. f \<in> F \<and> z = s.maxim (SUPP f)} x0"
               unfolding x0_def s.isMaxim_def s.isMinim_def
               by (blast intro!: r.minim_isMinim FinFuncD[of _ r s])
             with maxF(1) SUPPF F(1) have x0Field: "x0 \<in> Field r"
@@ -770,13 +722,8 @@
             from zmin x0min have "G \<noteq> {}" unfolding G_def z_def s.isMinim_def r.isMinim_def by blast
             have GF: "G \<subseteq> (\<lambda>f. f(z := r.zero)) ` F" unfolding G_def by auto
             have "G \<subseteq> fin_support r.zero (Field s)"
-            unfolding FinFunc_def fin_support_def proof safe
-              fix g assume "g \<in> G"
-              with GF obtain f where f: "f \<in> F" "g = f(z := r.zero)" by auto
-              with SUPPF have "finite (SUPP f)" by blast
-              with f show "finite (SUPP g)"
-                by (elim finite_subset[rotated]) (auto simp: support_def)
-            qed
+              unfolding FinFunc_def fin_support_def
+              using F(1) FinFunc_def G_def fin_support_def by fastforce
             moreover from F GF zField have "G \<subseteq> Func (Field s) (Field r)"
               using Func_upd[of _ "Field s" "Field r" z r.zero] unfolding FinFunc_def by auto
             ultimately have G: "G \<subseteq> FINFUNC" unfolding FinFunc_def by blast
@@ -799,7 +746,7 @@
                   unfolding z by (intro s.maxim_mono) auto
               }
               moreover from y'min have "\<And>g. g \<in> G \<Longrightarrow> (y', s.maxim (SUPP g)) \<in> s"
-                  unfolding s.isMinim_def by auto
+                unfolding s.isMinim_def by auto
               ultimately have "y' \<noteq> z" "(y', z) \<in> s" using maxG
                 unfolding s.isMinim_def s.isMaxim_def by auto
               with zy have "y' \<noteq> y" "(y', y) \<in> s" using antisymD[OF s.ANTISYM] transD[OF s.TRANS]
@@ -814,7 +761,7 @@
             with x0notzero zField have SUPP: "SUPP f0 = SUPP g0 \<union> {z}" unfolding support_def by auto
             from g0z have f0z: "f0(z := r.zero) = g0" unfolding f0_def fun_upd_upd by auto
             have f0: "f0 \<in> F" using x0min g0(1)
-              Func_elim[OF subsetD[OF subset_trans[OF F(1)[unfolded FinFunc_def] Int_lower1]] zField]
+                Func_elim[OF subsetD[OF subset_trans[OF F(1)[unfolded FinFunc_def] Int_lower1]] zField]
               unfolding f0_def r.isMinim_def G_def by (force simp: fun_upd_idem)
             from g0(1) maxF(1) have maxf0: "s.maxim (SUPP f0) = z" unfolding SUPP G_def
               by (intro s.maxim_equality) (auto simp: s.isMaxim_def)
@@ -834,7 +781,7 @@
                   hence oexp: "(f0(z := r.zero, z := x0), f(z := r.zero, z := x0)) \<in> oexp"
                     by (elim fun_upd_same_oexp[OF _ _ zField x0Field]) simp
                   with f F(1) x0min True
-                    have "(f(z := x0), f) \<in> oexp" unfolding G_def r.isMinim_def
+                  have "(f(z := x0), f) \<in> oexp" unfolding G_def r.isMinim_def
                     by (intro fun_upd_smaller_oexp[OF _ zField x0Field]) auto
                   with oexp show ?thesis using transD[OF oexp_trans, of f0 "f(z := x0)" f]
                     unfolding f0_def by auto
@@ -868,12 +815,12 @@
                     have "f (s.maxim (SUPP f)) \<noteq> r.zero"
                       using bspec[OF maxF(1) f, unfolded s.isMaxim_def] by (auto simp: support_def)
                     with f0f * f f0 maxf0 SUPPF
-                      have "s.max_fun_diff f0 f = s.maxim (SUPP f0 \<union> SUPP f)"
+                    have "s.max_fun_diff f0 f = s.maxim (SUPP f0 \<union> SUPP f)"
                       unfolding max_fun_diff_alt using s.maxim_Un[of "SUPP f0" "SUPP f"]
                       by (intro s.maxim_Int) (auto simp: s.max2_def)
                     moreover have "s.maxim (SUPP f0 \<union> SUPP f) = s.maxim (SUPP f)"
-                       using s.maxim_Un[of "SUPP f0" "SUPP f"] * maxf0 SUPPF f0 f
-                       by (auto simp: s.max2_def)
+                      using s.maxim_Un[of "SUPP f0" "SUPP f"] * maxf0 SUPPF f0 f
+                      by (auto simp: s.max2_def)
                     ultimately show ?thesis using f f0 F(1) maxF(1) SUPPF unfolding oexp_def Let_def
                       by (fastforce simp: s.isMaxim_def intro!: r.zero_smallest FINFUNCD)
                   qed
@@ -883,13 +830,9 @@
           qed simp
         qed
       qed
-    } note * = mp[OF this]
-    from A(2) obtain f where f: "f \<in> A" by blast
-    with A(1) show "\<exists>a\<in>A. \<forall>a'\<in>A. (a, a') \<in> oexp"
-    proof (cases "f = const")
-      case False with f A(1) show ?thesis using maxim_isMaxim_support[of "{f}"]
-        by (intro *[of _ "s.maxim (SUPP f)"]) (auto simp: s.isMaxim_def support_def)
-    qed simp
+    } 
+    with A show "\<exists>a\<in>A. \<forall>a'\<in>A. (a, a') \<in> oexp"
+      by blast
   qed
 qed
 
@@ -899,8 +842,7 @@
 interpretation o: wo_rel oexp by unfold_locales (rule oexp_Well_order)
 
 lemma zero_oexp: "Field r \<noteq> {} \<Longrightarrow> o.zero = const"
-  by (rule sym[OF o.leq_zero_imp[OF const_least]])
-    (auto intro!: o.zero_in_Field[unfolded Field_oexp] dest!: const_FINFUNC)
+  by (metis Field_oexp const_FINFUNC const_least o.Field_ofilter o.equals_minim o.ofilter_def o.zero_def)
 
 end
 
@@ -925,8 +867,8 @@
   by (auto dest: well_order_on_domain)
 
 lemma ozero_ordLeq:
-assumes "Well_order r"  shows "ozero \<le>o r"
-using assms unfolding ozero_def ordLeq_def embed_def[abs_def] under_def by auto
+  assumes "Well_order r"  shows "ozero \<le>o r"
+  using assms unfolding ozero_def ordLeq_def embed_def[abs_def] under_def by auto
 
 definition "oone = {((),())}"
 
@@ -985,8 +927,8 @@
 lemma osum_cong:
   assumes "t =o u" and "r =o s"
   shows "t +o r =o u +o s"
-using ordIso_transitive[OF osum_congL[OF assms(1)] osum_congR[OF assms(2)]]
-  assms[unfolded ordIso_def] by auto
+  using ordIso_transitive[OF osum_congL[OF assms(1)] osum_congR[OF assms(2)]]
+    assms[unfolded ordIso_def] by auto
 
 lemma Well_order_empty[simp]: "Well_order {}"
   unfolding Field_empty by (rule well_order_on_empty)
@@ -1005,8 +947,8 @@
   shows "{} ^o r = {}"
 proof -
   from assms(2) have "Field r \<noteq> {}" unfolding Field_def by auto
-  thus ?thesis unfolding oexp_def[OF Well_order_empty assms(1)] FinFunc_def fin_support_def support_def
-    by auto
+  thus ?thesis
+    by (simp add: assms(1) wo_rel2.intro wo_rel2.oexp_empty)
 qed
 
 lemma oprod_zero[simp]: "{} *o r = {}" "r *o {} = {}"
@@ -1051,8 +993,8 @@
 lemma oprod_cong:
   assumes "t =o u" and "r =o s"
   shows "t *o r =o u *o s"
-using ordIso_transitive[OF oprod_congL[OF assms(1)] oprod_congR[OF assms(2)]]
-  assms[unfolded ordIso_def] by auto
+  using ordIso_transitive[OF oprod_congL[OF assms(1)] oprod_congR[OF assms(2)]]
+    assms[unfolded ordIso_def] by auto
 
 lemma Field_singleton[simp]: "Field {(z,z)} = {z}"
   by (metis well_order_on_Field well_order_on_singleton)
@@ -1155,7 +1097,7 @@
   let ?f = "map_sum f id"
   from f have "\<forall>a\<in>Field (r +o t).
      ?f a \<in> Field (s +o t) \<and> ?f ` underS (r +o t) a \<subseteq> underS (s +o t) (?f a)"
-     unfolding Field_osum underS_def by (fastforce simp: osum_def)
+    unfolding Field_osum underS_def by (fastforce simp: osum_def)
   thus ?thesis unfolding ordLeq_def2 by (auto intro: osum_Well_order r s t)
 qed
 
@@ -1224,7 +1166,7 @@
   let ?f = "map_prod f id"
   from f have "\<forall>a\<in>Field (r *o t).
      ?f a \<in> Field (s *o t) \<and> ?f ` underS (r *o t) a \<subseteq> underS (s *o t) (?f a)"
-     unfolding Field_oprod underS_def unfolding map_prod_def oprod_def by auto
+    unfolding Field_oprod underS_def unfolding map_prod_def oprod_def by auto
   thus ?thesis unfolding ordLeq_def2 by (auto intro: oprod_Well_order r s t)
 qed
 
@@ -1266,8 +1208,7 @@
 qed
 
 lemma ozero_oexp: "\<not> (s =o ozero) \<Longrightarrow> ozero ^o s =o ozero"
-  unfolding oexp_def[OF ozero_Well_order s] FinFunc_def
-  by simp (metis Func_emp2 bot.extremum_uniqueI emptyE well_order_on_domain s subrelI)
+  by (fastforce simp add: oexp_def[OF ozero_Well_order s] FinFunc_def Func_def intro: FieldI1)
 
 lemma oone_oexp: "oone ^o s =o oone" (is "?L =o ?R")
   by (rule oone_ordIso_oexp[OF ordIso_reflexive[OF oone_Well_order] s])
@@ -1315,17 +1256,17 @@
       "let m = s.max_fun_diff g h in (g m, h m) \<in> r"
     hence "g \<noteq> h" by auto
     note max_fun_diff_in = rs.max_fun_diff_in[OF \<open>g \<noteq> h\<close> gh(1,2)]
-    and max_fun_diff_max = rs.max_fun_diff_max[OF \<open>g \<noteq> h\<close> gh(1,2)]
+      and max_fun_diff_max = rs.max_fun_diff_max[OF \<open>g \<noteq> h\<close> gh(1,2)]
     with *(4) invff *(2) have "t.max_fun_diff (F g) (F h) = f (s.max_fun_diff g h)"
       unfolding t.max_fun_diff_def compat_def
       by (intro t.maxim_equality) (auto simp: t.isMaxim_def F_def dest: injfD)
     with gh invff max_fun_diff_in
-      show "let m = t.max_fun_diff (F g) (F h) in (F g m, F h m) \<in> r"
+    show "let m = t.max_fun_diff (F g) (F h) in (F g m, F h m) \<in> r"
       unfolding F_def Let_def by (auto simp: dest: injfD)
   qed
   moreover
   from FLR have "ofilter ?R (F ` Field ?L)"
-  unfolding rexpt.ofilter_def under_def rs.Field_oexp rt.Field_oexp unfolding rt.oexp_def
+    unfolding rexpt.ofilter_def under_def rs.Field_oexp rt.Field_oexp unfolding rt.oexp_def
   proof (safe elim!: imageI)
     fix g h assume gh: "g \<in> FinFunc r s" "h \<in> FinFunc r t" "F g \<in> FinFunc r t"
       "let m = t.max_fun_diff h (F g) in (h m, F g m) \<in> r"
@@ -1345,13 +1286,13 @@
         proof (rule ccontr)
           assume "(t.max_fun_diff h (F g), z) \<notin> t"
           hence "(z, t.max_fun_diff h (F g)) \<in> t" using t.in_notinI[of "t.max_fun_diff h (F g)" z]
-            z max_Field by auto
+              z max_Field by auto
           hence "z \<in> f ` Field s" using *(3) max_f_Field unfolding t.ofilter_def under_def
             by fastforce
           with z show False by blast
         qed
         hence "h z = r.zero" using rt.max_fun_diff_le_eq[OF _ False gh(2,3), of z]
-          z max_f_Field unfolding F_def by auto
+            z max_f_Field unfolding F_def by auto
       } note ** = this
       with *(3) gh(2) have "h = F (\<lambda>x. if x \<in> Field s then h (f x) else undefined)" using invff
         unfolding F_def fun_eq_iff FinFunc_def Func_def Let_def t.ofilter_def under_def by auto
@@ -1437,8 +1378,8 @@
             by (subst t.max_fun_diff_def, intro t.maxim_equality)
               (auto simp: t.isMaxim_def intro: inj_onD[OF inj] intro!: rt.max_fun_diff_max)
           with Field_fg Field_fh hg fz f_underS compat neq have "(?f h, ?f g) \<in> st.oexp"
-             using rt.max_fun_diff[OF \<open>h \<noteq> g\<close>] rt.max_fun_diff_in[OF \<open>h \<noteq> g\<close>] unfolding st.Field_oexp
-             unfolding rt.oexp_def st.oexp_def Let_def compat_def by auto
+            using rt.max_fun_diff[OF \<open>h \<noteq> g\<close>] rt.max_fun_diff_in[OF \<open>h \<noteq> g\<close>] unfolding st.Field_oexp
+            unfolding rt.oexp_def st.oexp_def Let_def compat_def by auto
           with neq show "?f h \<in> underS (s ^o t) (?f g)" unfolding underS_def by auto
         qed
         ultimately have "?f g \<in> Field (s ^o t) \<and> ?f ` underS (r ^o t) g \<subseteq> underS (s ^o t) (?f g)"
@@ -1460,7 +1401,7 @@
     x: "x \<in> Field r" "r.zero \<in> Field r" "x \<noteq> r.zero"
     unfolding ordLess_def oone_def embedS_def[abs_def] bij_betw_def embed_def under_def
     by (auto simp: image_def)
-       (metis (lifting) equals0D mem_Collect_eq r.zero_in_Field singletonI)
+      (metis (lifting) equals0D mem_Collect_eq r.zero_in_Field singletonI)
   let ?f = "\<lambda>a b. if b \<in> Field s then if b = a then x else r.zero else undefined"
   from x(3) have SUPP: "\<And>y. y \<in> Field s \<Longrightarrow> rs.SUPP (?f y) = {y}" unfolding support_def by auto
   { fix y assume y: "y \<in> Field s"
@@ -1553,7 +1494,7 @@
   interpret rt: wo_rel2 r t by unfold_locales (rule r, rule t)
   let ?f = "\<lambda>(f, g). case_sum f g"
   have "bij_betw ?f (Field ?L) (Field ?R)"
-  unfolding bij_betw_def rst.Field_oexp rs.Field_oexp rt.Field_oexp Field_oprod proof (intro conjI)
+    unfolding bij_betw_def rst.Field_oexp rs.Field_oexp rt.Field_oexp Field_oprod proof (intro conjI)
     show "inj_on ?f (FinFunc r s \<times> FinFunc r t)" unfolding inj_on_def
       by (auto simp: fun_eq_iff split: sum.splits)
     show "?f ` (FinFunc r s \<times> FinFunc r t) = FinFunc r (s +o t)"
@@ -1567,7 +1508,7 @@
   moreover have "compat ?L ?R ?f"
     unfolding compat_def rst.Field_oexp rs.Field_oexp rt.Field_oexp oprod_def
     unfolding rst.oexp_def Let_def rs.oexp_def rt.oexp_def
-      by (fastforce simp: Field_osum FinFunc_osum o_def split: sum.splits
+    by (fastforce simp: Field_osum FinFunc_osum o_def split: sum.splits
         dest: max_fun_diff_eq_Inl max_fun_diff_eq_Inr)
   ultimately have "iso ?L ?R ?f" using r s t
     by (subst iso_iff3) (auto intro: oexp_Well_order oprod_Well_order osum_Well_order)
@@ -1638,8 +1579,8 @@
   interpret rs: wo_rel2 r s by unfold_locales (rule r, rule s)
   interpret rst: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
   from fun_unequal_in_support[OF assms(2), of "Field (s *o t)" "Field r" "Field r"] assms(3,4)
-    have diff1: "rev_curr f \<noteq> rev_curr g"
-      "rev_curr f \<in> FinFunc (r ^o s) t" "rev_curr g \<in> FinFunc (r ^o s) t" using rev_curr_FinFunc[OF Field]
+  have diff1: "rev_curr f \<noteq> rev_curr g"
+    "rev_curr f \<in> FinFunc (r ^o s) t" "rev_curr g \<in> FinFunc (r ^o s) t" using rev_curr_FinFunc[OF Field]
     unfolding fun_eq_iff rev_curr_def[abs_def] FinFunc_def support_def Field_oprod
     by auto fast
   hence diff2: "rev_curr f m \<noteq> rev_curr g m" "rev_curr f m \<in> FinFunc r s" "rev_curr g m \<in> FinFunc r s"
@@ -1653,7 +1594,7 @@
   next
     assume "f (s.max_fun_diff (rev_curr f m) (rev_curr g m), m) =
             g (s.max_fun_diff (rev_curr f m) (rev_curr g m), m)"
-           (is "f (?x, m) = g (?x, m)")
+      (is "f (?x, m) = g (?x, m)")
     hence "rev_curr f m ?x = rev_curr g m ?x" unfolding rev_curr_def by auto
     with rs.max_fun_diff[OF diff2] show False by auto
   next
@@ -1674,14 +1615,14 @@
   proof (cases "s = {} \<or> t = {}")
     case True with \<open>r = {}\<close> show ?thesis
       by (auto simp: oexp_empty[OF oexp_Well_order[OF Well_order_empty s]]
-        intro!: ordIso_transitive[OF ordIso_symmetric[OF oone_ordIso] oone_ordIso]
+          intro!: ordIso_transitive[OF ordIso_symmetric[OF oone_ordIso] oone_ordIso]
           ordIso_transitive[OF oone_ordIso_oexp[OF ordIso_symmetric[OF oone_ordIso] t] oone_ordIso])
   next
-     case False
-     hence "s *o t \<noteq> {}" unfolding oprod_def Field_def by fastforce
-     with False show ?thesis
-       using \<open>r = {}\<close> ozero_ordIso
-       by (auto simp add: s t oprod_Well_order ozero_def)
+    case False
+    hence "s *o t \<noteq> {}" unfolding oprod_def Field_def by fastforce
+    with False show ?thesis
+      using \<open>r = {}\<close> ozero_ordIso
+      by (auto simp add: s t oprod_Well_order ozero_def)
   qed
 next
   case False
@@ -1692,7 +1633,7 @@
     interpret rs: wo_rel2 r s by unfold_locales (rule r, rule s)
     interpret rst: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
     have bij: "bij_betw rev_curr (Field ?L) (Field ?R)"
-    unfolding bij_betw_def r_st.Field_oexp rst.Field_oexp Field_oprod proof (intro conjI)
+      unfolding bij_betw_def r_st.Field_oexp rst.Field_oexp Field_oprod proof (intro conjI)
       show "inj_on rev_curr (FinFunc r (s *o t))"
         unfolding inj_on_def FinFunc_def Func_def Field_oprod rs.Field_oexp rev_curr_def[abs_def]
         by (auto simp: fun_eq_iff) metis
@@ -1700,16 +1641,16 @@
     qed
     moreover
     have "compat ?L ?R rev_curr"
-    unfolding compat_def proof safe
+      unfolding compat_def proof safe
       fix fg1 fg2 assume fg: "(fg1, fg2) \<in> r ^o (s *o t)"
       show "(rev_curr fg1, rev_curr fg2) \<in> r ^o s ^o t"
       proof (cases "fg1 = fg2")
         assume "fg1 \<noteq> fg2"
         with fg show ?thesis
-        using rst.max_fun_diff_in[of "rev_curr fg1" "rev_curr fg2"]
-          max_fun_diff_oprod[OF Field, of fg1 fg2]  rev_curr_FinFunc[OF Field, symmetric]
-        unfolding r_st.Field_oexp rs.Field_oexp rst.Field_oexp unfolding r_st.oexp_def rst.oexp_def
-        by (auto simp: rs.oexp_def Let_def) (auto simp: rev_curr_def[abs_def])
+          using rst.max_fun_diff_in[of "rev_curr fg1" "rev_curr fg2"]
+            max_fun_diff_oprod[OF Field, of fg1 fg2]  rev_curr_FinFunc[OF Field, symmetric]
+          unfolding r_st.Field_oexp rs.Field_oexp rst.Field_oexp unfolding r_st.oexp_def rst.oexp_def
+          by (auto simp: rs.oexp_def Let_def) (auto simp: rev_curr_def[abs_def])
       next
         assume "fg1 = fg2"
         with fg bij show ?thesis unfolding r_st.Field_oexp rs.Field_oexp rst.Field_oexp bij_betw_def
diff -r 20ab27bc1f3b -r f33df7529fed src/HOL/Cardinals/Wellorder_Constructions.thy
--- a/src/HOL/Cardinals/Wellorder_Constructions.thy	Fri Jan 13 11:05:48 2023 +0000
+++ b/src/HOL/Cardinals/Wellorder_Constructions.thy	Fri Jan 13 16:19:56 2023 +0000
@@ -93,12 +93,7 @@
 lemma ofilter_ordLeq:
   assumes "Well_order r" and "ofilter r A"
   shows "Restr r A \<le>o r"
-proof-
-  have "A \<le> Field r" using assms by (auto simp add: wo_rel_def wo_rel.ofilter_def)
-  thus ?thesis using assms
-    by (simp add: ofilter_subset_ordLeq wo_rel.Field_ofilter
-        wo_rel_def Restr_Field)
-qed
+by (metis assms inf.orderE ofilter_embed ofilter_subset_ordLeq refl_on_def wo_rel.Field_ofilter wo_rel.REFL wo_rel.intro)
 
 corollary under_Restr_ordLeq:
   "Well_order r \<Longrightarrow> Restr r (under r a) \<le>o r"
@@ -122,20 +117,7 @@
     using assms unfolding dir_image_def inj_on_def by auto
 next
   show "(dir_image r1 f) Int (dir_image r2 f) \<le> dir_image (r1 Int r2) f"
-  proof(clarify)
-    fix a' b'
-    assume "(a',b') \<in> dir_image r1 f" "(a',b') \<in> dir_image r2 f"
-    then obtain a1 b1 a2 b2
-      where 1: "a' = f a1 \<and> b' = f b1 \<and> a' = f a2 \<and> b' = f b2" and
-        2: "(a1,b1) \<in> r1 \<and> (a2,b2) \<in> r2" and
-        3: "{a1,b1} \<le> Field r1 \<and> {a2,b2} \<le> Field r2"
-      unfolding dir_image_def Field_def by blast
-    hence "a1 = a2 \<and> b1 = b2" using assms unfolding inj_on_def by auto
-    hence "a' = f a1 \<and> b' = f b1 \<and> (a1,b1) \<in> r1 Int r2 \<and> (a2,b2) \<in> r1 Int r2"
-      using 1 2 by auto
-    thus "(a',b') \<in> dir_image (r1 \<inter> r2) f"
-      unfolding dir_image_def by blast
-  qed
+    by (clarsimp simp: dir_image_def) (metis FieldI1 FieldI2 UnCI assms inj_on_def)
 qed
 
 (* More facts on ordinal sum: *)
@@ -154,21 +136,8 @@
   have "inj_on id (Field r)" by simp
   moreover
   have "ofilter (r Osum r') (Field r)"
-    using 1 proof(auto simp add: wo_rel_def wo_rel.ofilter_def
-      Field_Osum under_def)
-    fix a b assume 2: "a \<in> Field r" and 3: "(b,a) \<in> r Osum r'"
-    moreover
-    {assume "(b,a) \<in> r'"
-      hence "a \<in> Field r'" using Field_def[of r'] by blast
-      hence False using 2 FLD by blast
-    }
-    moreover
-    {assume "a \<in> Field r'"
-      hence False using 2 FLD by blast
-    }
-    ultimately
-    show "b \<in> Field r" by (auto simp add: Osum_def Field_def)
-  qed
+    using 1 FLD
+    by (auto simp add: wo_rel_def wo_rel.ofilter_def Osum_def under_def Field_iff disjoint_iff)
   ultimately show ?thesis
     using assms by (auto simp add: embed_iff_compat_inj_on_ofilter)
 qed
@@ -237,8 +206,8 @@
     show "\<exists>p'. (isOmax ?R' p')"
     proof(cases "R = {}")
       case True
-      thus ?thesis unfolding isOmax_def using ***
-        by (simp add: ordLeq_reflexive)
+      thus ?thesis
+        by (simp add: "***" isOmax_def ordLeq_reflexive)
     next
       case False
       then obtain p where p: "isOmax R p" using IH by auto
@@ -249,14 +218,9 @@
       }
       moreover
       {assume Case22: "p \<le>o r"
-        {fix r' assume "r' \<in> ?R'"
-          moreover
-          {assume "r' \<in> R"
-            hence "r' \<le>o p" using p unfolding isOmax_def by simp
-            hence "r' \<le>o r" using Case22 by(rule ordLeq_transitive)
-          }
-          moreover have "r \<le>o r" using *** by(rule ordLeq_reflexive)
-          ultimately have "r' \<le>o r" by auto
+        { fix r' assume "r' \<in> ?R'"
+          then have "r' \<le>o r"
+            by (metis "***" Case22 insert_iff isOmax_def ordLeq_transitive p ordLeq_reflexive)
         }
         hence "isOmax ?R' r" unfolding isOmax_def by simp
         hence ?thesis by auto
@@ -374,7 +338,8 @@
     by simp (metis REFL in_mono max2_def max2_greater refl_on_domain)
   have "(supr A, b) \<in> r"
     by (simp add: "0" A bb supr_least)
-  thus False using bA unfolding underS_def by simp (metis ANTISYM antisymD)
+  thus False
+    by (metis antisymD bA underS_E wo_rel.ANTISYM wo_rel_axioms)
 qed
 
 lemma underS_suc:
@@ -387,17 +352,15 @@
     by (metis bb in_mono max2_def max2_greater mem_Collect_eq underS_I under_def)
   have "(suc A, b) \<in> r"
     by (metis "0" A bb suc_least underS_E)
-  thus False using bA unfolding underS_def by simp (metis ANTISYM antisymD)
+  thus False
+    by (metis antisymD bA underS_E wo_rel.ANTISYM wo_rel_axioms)
 qed
 
 lemma (in wo_rel) in_underS_supr:
   assumes j: "j \<in> underS i" and i: "i \<in> A" and A: "A \<subseteq> Field r" and AA: "Above A \<noteq> {}"
   shows "j \<in> underS (supr A)"
-proof-
-  have "(i,supr A) \<in> r" using supr_greater[OF A AA i] .
-  thus ?thesis using j unfolding underS_def
-    by simp (metis REFL TRANS max2_def max2_equals1 refl_on_domain transD)
-qed
+  using supr_greater[OF A AA i]
+  by (metis FieldI1 j max2_equals1 max2_equals2 max2_iff underS_E underS_I)
 
 lemma inj_on_Field:
   assumes A: "A \<subseteq> Field r" and f: "\<And> a b. \<lbrakk>a \<in> A; b \<in> A; a \<in> underS b\<rbrakk> \<Longrightarrow> f a \<noteq> f b"
@@ -412,29 +375,13 @@
 lemma underS_init_seg_of_Collect:
   assumes "\<And>j1 j2. \<lbrakk>j2 \<in> underS i; (j1, j2) \<in> r\<rbrakk> \<Longrightarrow> R j1 initial_segment_of R j2"
   shows "{R j |j. j \<in> underS i} \<in> Chains init_seg_of"
-  unfolding Chains_def proof safe
-  fix j ja assume jS: "j \<in> underS i" and jaS: "ja \<in> underS i"
-    and init: "(R ja, R j) \<notin> init_seg_of"
-  hence jja: "{j,ja} \<subseteq> Field r" and j: "j \<in> Field r" and ja: "ja \<in> Field r"
-    and jjai: "(j,i) \<in> r" "(ja,i) \<in> r"
-    and i: "i \<notin> {j,ja}" unfolding Field_def underS_def by auto
-  have jj: "(j,j) \<in> r" and jaja: "(ja,ja) \<in> r" using j ja by (metis in_notinI)+
-  show "R j initial_segment_of R ja"
-    using jja init TOTALS assms jS jaS by auto
-qed
+  using TOTALS assms 
+  by (clarsimp simp: Chains_def) (meson BNF_Least_Fixpoint.underS_Field)
 
 lemma (in wo_rel) Field_init_seg_of_Collect:
   assumes "\<And>j1 j2. \<lbrakk>j2 \<in> Field r; (j1, j2) \<in> r\<rbrakk> \<Longrightarrow> R j1 initial_segment_of R j2"
   shows "{R j |j. j \<in> Field r} \<in> Chains init_seg_of"
-  unfolding Chains_def proof safe
-  fix j ja assume jS: "j \<in> Field r" and jaS: "ja \<in> Field r"
-    and init: "(R ja, R j) \<notin> init_seg_of"
-  hence jja: "{j,ja} \<subseteq> Field r" and j: "j \<in> Field r" and ja: "ja \<in> Field r"
-    unfolding Field_def underS_def by auto
-  have jj: "(j,j) \<in> r" and jaja: "(ja,ja) \<in> r" using j ja by (metis in_notinI)+
-  show "R j initial_segment_of R ja"
-    using TOTALS assms init jS jaS by blast
-qed
+  using TOTALS assms by (auto simp: Chains_def)
 
 subsubsection \<open>Successor and limit elements of an ordinal\<close>
 
@@ -448,8 +395,7 @@
 
 lemma zero_smallest[simp]:
   assumes "j \<in> Field r" shows "(zero, j) \<in> r"
-  unfolding zero_def
-  by (metis AboveS_Field assms subset_AboveS_UnderS subset_antisym subset_refl suc_def suc_least_AboveS)
+  by (simp add: assms wo_rel.ofilter_linord wo_rel_axioms zero_def)
 
 lemma zero_in_Field: assumes "Field r \<noteq> {}"  shows "zero \<in> Field r"
   using assms unfolding zero_def by (metis Field_ofilter minim_in ofilter_def)
@@ -496,8 +442,7 @@
 lemma succ_smallest:
   assumes "(i,j) \<in> r" and "i \<noteq> j"
   shows "(succ i, j) \<in> r"
-  unfolding succ_def apply(rule suc_least)
-  using assms unfolding Field_def by auto
+  by (metis Field_iff assms empty_subsetI insert_subset singletonD suc_least succ_def)
 
 lemma isLim_supr:
   assumes f: "i \<in> Field r" and l: "isLim i"
@@ -755,44 +700,19 @@
         moreover have "f a1 \<in> underS s (f a)" using f[OF a] a1 by auto
         ultimately have "g a1 \<in> underS s (f a)" by (metis s.ANTISYM s.TRANS under_underS_trans)
       }
-      hence "f a \<in> AboveS s (g ` underS r a)" unfolding AboveS_def
+      hence fa_in: "f a \<in> AboveS s (g ` underS r a)" unfolding AboveS_def
         using fa by simp (metis (lifting, full_types) mem_Collect_eq underS_def)
       hence A: "AboveS s (g ` underS r a) \<noteq> {}" by auto
-      have B: "\<And> a1. a1 \<in> underS r a \<Longrightarrow> g a1 \<in> underS s (g a)"
-        unfolding g apply(rule s.suc_underS[OF A0 A]) by auto
-      {fix a1 a2 assume a2: "a2 \<in> underS r a" and 1: "a1 \<in> underS r a2"
-        hence a12: "{a1,a2} \<subseteq> under r a2" and "a1 \<noteq> a2" using r.REFL a
-          unfolding underS_def under_def refl_on_def Field_def by auto
-        hence "g a1 \<noteq> g a2" using IH1a[OF a2] unfolding inj_on_def by auto
-        hence "g a1 \<in> underS s (g a2)" using IH1b[OF a2] a12
-          unfolding underS_def under_def by auto
-      } note C = this
       have ga: "g a \<in> Field s" unfolding g using s.suc_inField[OF A0 A] .
-      have aa: "a \<in> under r a"
-        using a r.REFL unfolding under_def underS_def refl_on_def by auto
-      show ?case proof safe
-        show "bij_betw g (under r a) (under s (g a))" unfolding bij_betw_def proof safe
-          show "inj_on g (under r a)"
-            by (metis A IH1a IH1b a bij_betw_def g ga r s s.suc_greater subsetI wellorders_totally_ordered_aux) 
-        next
-          fix a1 assume a1: "a1 \<in> under r a"
-          show "g a1 \<in> under s (g a)"
-            by (metis (mono_tags, lifting) B a1 ga mem_Collect_eq s.in_notinI underS_def under_def)
-        next
-          fix b1 assume b1: "b1 \<in> under s (g a)"
-          show "b1 \<in> g ` under r a"
-          proof(cases "b1 = g a")
-            case True thus ?thesis using aa by auto
-          next
-            case False
-            show ?thesis 
-              by (metis b1 A IH1a IH1b a bij_betw_def g ga r s s.suc_greater subsetI wellorders_totally_ordered_aux)
-          qed
-        qed
-      next
-        have "(g a, f a) \<in> s" unfolding g
-          using \<open>f a \<in> s.AboveS (g ` r.underS a)\<close> s.suc_least_AboveS by blast 
-        thus "g a \<in> under s (f a)" unfolding under_def by auto
+      show ?case
+        unfolding bij_betw_def
+      proof (intro conjI)
+        show "inj_on g (r.under a)"
+          by (metis A IH1a IH1b a bij_betw_def g ga r s s.suc_greater subsetI wellorders_totally_ordered_aux)
+        show "g ` r.under a = s.under (g a)"
+          by (metis A A0 IH1a IH1b a bij_betw_def g ga r s s.suc_greater wellorders_totally_ordered_aux)
+        show "g a \<in> s.under (f a)"
+          by (simp add: fa_in g s.suc_least_AboveS under_def)
       qed
     qed
   }
@@ -808,8 +728,7 @@
 lemma iso_oproj:
   assumes r: "Well_order r" and s: "Well_order s" and f: "iso r s f"
   shows "oproj r s f"
-  using assms unfolding oproj_def
-  by (metis iso_Field iso_iff3 order_refl)
+  by (metis embed_Field f iso_Field iso_iff iso_iff3 oproj_def r s)
 
 theorem oproj_embed:
   assumes r: "Well_order r" and s: "Well_order s" and f: "oproj r s f"
@@ -843,6 +762,6 @@
 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
+  using f oproj_embed ordLess_iff ordLess_or_ordLeq r s by blast
 
 end
diff -r 20ab27bc1f3b -r f33df7529fed src/HOL/Cardinals/Wellorder_Embedding.thy
--- a/src/HOL/Cardinals/Wellorder_Embedding.thy	Fri Jan 13 11:05:48 2023 +0000
+++ b/src/HOL/Cardinals/Wellorder_Embedding.thy	Fri Jan 13 16:19:56 2023 +0000
@@ -8,22 +8,22 @@
 section \<open>Well-Order Embeddings\<close>
 
 theory Wellorder_Embedding
-imports Fun_More Wellorder_Relation
+  imports Fun_More Wellorder_Relation
 begin
 
 subsection \<open>Auxiliaries\<close>
 
 lemma UNION_bij_betw_ofilter:
-assumes WELL: "Well_order r" and
-        OF: "\<And> i. i \<in> I \<Longrightarrow> ofilter r (A i)" and
-       BIJ: "\<And> i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)"
-shows "bij_betw f (\<Union>i \<in> I. A i) (\<Union>i \<in> I. A' i)"
+  assumes WELL: "Well_order r" and
+    OF: "\<And> i. i \<in> I \<Longrightarrow> ofilter r (A i)" and
+    BIJ: "\<And> i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)"
+  shows "bij_betw f (\<Union>i \<in> I. A i) (\<Union>i \<in> I. A' i)"
 proof-
   have "wo_rel r" using WELL by (simp add: wo_rel_def)
   hence "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i"
-  using wo_rel.ofilter_linord[of r] OF by blast
+    using wo_rel.ofilter_linord[of r] OF by blast
   with WELL BIJ show ?thesis
-  by (auto simp add: bij_betw_UNION_chain)
+    by (auto simp add: bij_betw_UNION_chain)
 qed
 
 
@@ -31,144 +31,98 @@
 functions\<close>
 
 lemma embed_halfcong:
-assumes EQ: "\<And> a. a \<in> Field r \<Longrightarrow> f a = g a" and
-        EMB: "embed r r' f"
-shows "embed r r' g"
-proof(unfold embed_def, auto)
-  fix a assume *: "a \<in> Field r"
-  hence "bij_betw f (under r a) (under r' (f a))"
-  using EMB unfolding embed_def by simp
-  moreover
-  {have "under r a \<le> Field r"
-   by (auto simp add: under_Field)
-   hence "\<And> b. b \<in> under r a \<Longrightarrow> f b = g b"
-   using EQ by blast
-  }
-  moreover have "f a = g a" using * EQ by auto
-  ultimately show "bij_betw g (under r a) (under r' (g a))"
-  using bij_betw_cong[of "under r a" f g "under r' (f a)"] by auto
-qed
+  assumes "\<And> a. a \<in> Field r \<Longrightarrow> f a = g a" and "embed r r' f"
+  shows "embed r r' g"
+  by (smt (verit, del_insts) assms bij_betw_cong embed_def in_mono under_Field)
 
 lemma embed_cong[fundef_cong]:
-assumes "\<And> a. a \<in> Field r \<Longrightarrow> f a = g a"
-shows "embed r r' f = embed r r' g"
-using assms embed_halfcong[of r f g r']
-            embed_halfcong[of r g f r'] by auto
+  assumes "\<And> a. a \<in> Field r \<Longrightarrow> f a = g a"
+  shows "embed r r' f = embed r r' g"
+  by (metis assms embed_halfcong)
 
 lemma embedS_cong[fundef_cong]:
-assumes "\<And> a. a \<in> Field r \<Longrightarrow> f a = g a"
-shows "embedS r r' f = embedS r r' g"
-unfolding embedS_def using assms
-embed_cong[of r f g r'] bij_betw_cong[of "Field r" f g "Field r'"] by blast
+  assumes "\<And> a. a \<in> Field r \<Longrightarrow> f a = g a"
+  shows "embedS r r' f = embedS r r' g"
+  unfolding embedS_def using assms
+    embed_cong[of r f g r'] bij_betw_cong[of "Field r" f g "Field r'"] by blast
 
 lemma iso_cong[fundef_cong]:
-assumes "\<And> a. a \<in> Field r \<Longrightarrow> f a = g a"
-shows "iso r r' f = iso r r' g"
-unfolding iso_def using assms
-embed_cong[of r f g r'] bij_betw_cong[of "Field r" f g "Field r'"] by blast
+  assumes "\<And> a. a \<in> Field r \<Longrightarrow> f a = g a"
+  shows "iso r r' f = iso r r' g"
+  unfolding iso_def using assms
+    embed_cong[of r f g r'] bij_betw_cong[of "Field r" f g "Field r'"] by blast
 
 lemma id_compat: "compat r r id"
-by(auto simp add: id_def compat_def)
+  by(auto simp add: id_def compat_def)
 
 lemma comp_compat:
-"\<lbrakk>compat r r' f; compat r' r'' f'\<rbrakk> \<Longrightarrow> compat r r'' (f' o f)"
-by(auto simp add: comp_def compat_def)
+  "\<lbrakk>compat r r' f; compat r' r'' f'\<rbrakk> \<Longrightarrow> compat r r'' (f' o f)"
+  by(auto simp add: comp_def compat_def)
 
 corollary one_set_greater:
-"(\<exists>f::'a \<Rightarrow> 'a'. f ` A \<le> A' \<and> inj_on f A) \<or> (\<exists>g::'a' \<Rightarrow> 'a. g ` A' \<le> A \<and> inj_on g A')"
+  "(\<exists>f::'a \<Rightarrow> 'a'. f ` A \<le> A' \<and> inj_on f A) \<or> (\<exists>g::'a' \<Rightarrow> 'a. g ` A' \<le> A \<and> inj_on g A')"
 proof-
   obtain r where "well_order_on A r" by (fastforce simp add: well_order_on)
   hence 1: "A = Field r \<and> Well_order r"
-  using well_order_on_Well_order by auto
+    using well_order_on_Well_order by auto
   obtain r' where 2: "well_order_on A' r'" by (fastforce simp add: well_order_on)
   hence 2: "A' = Field r' \<and> Well_order r'"
-  using well_order_on_Well_order by auto
+    using well_order_on_Well_order by auto
   hence "(\<exists>f. embed r r' f) \<or> (\<exists>g. embed r' r g)"
-  using 1 2 by (auto simp add: wellorders_totally_ordered)
+    using 1 2 by (auto simp add: wellorders_totally_ordered)
   moreover
   {fix f assume "embed r r' f"
-   hence "f`A \<le> A' \<and> inj_on f A"
-   using 1 2 by (auto simp add: embed_Field embed_inj_on)
+    hence "f`A \<le> A' \<and> inj_on f A"
+      using 1 2 by (auto simp add: embed_Field embed_inj_on)
   }
   moreover
   {fix g assume "embed r' r g"
-   hence "g`A' \<le> A \<and> inj_on g A'"
-   using 1 2 by (auto simp add: embed_Field embed_inj_on)
+    hence "g`A' \<le> A \<and> inj_on g A'"
+      using 1 2 by (auto simp add: embed_Field embed_inj_on)
   }
   ultimately show ?thesis by blast
 qed
 
 corollary one_type_greater:
-"(\<exists>f::'a \<Rightarrow> 'a'. inj f) \<or> (\<exists>g::'a' \<Rightarrow> 'a. inj g)"
-using one_set_greater[of UNIV UNIV] by auto
+  "(\<exists>f::'a \<Rightarrow> 'a'. inj f) \<or> (\<exists>g::'a' \<Rightarrow> 'a. inj g)"
+  using one_set_greater[of UNIV UNIV] by auto
 
 
 subsection \<open>Uniqueness of embeddings\<close>
 
 lemma comp_embedS:
-assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
-        and  EMB: "embedS r r' f" and EMB': "embedS r' r'' f'"
-shows "embedS r r'' (f' o f)"
-proof-
-  have "embed r' r'' f'" using EMB' unfolding embedS_def by simp
-  thus ?thesis using assms by (auto simp add: embedS_comp_embed)
-qed
+  assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
+    and  EMB: "embedS r r' f" and EMB': "embedS r' r'' f'"
+  shows "embedS r r'' (f' o f)"
+  using EMB EMB' WELL WELL' embedS_comp_embed embedS_def by blast
 
 lemma iso_iff4:
-assumes WELL: "Well_order r"  and WELL': "Well_order r'"
-shows "iso r r' f = (embed r r' f \<and> embed r' r (inv_into (Field r) f))"
-using assms embed_bothWays_iso
-by(unfold iso_def, auto simp add: inv_into_Field_embed_bij_betw)
+  assumes WELL: "Well_order r"  and WELL': "Well_order r'"
+  shows "iso r r' f = (embed r r' f \<and> embed r' r (inv_into (Field r) f))"
+  using assms embed_bothWays_iso
+  by(unfold iso_def, auto simp add: inv_into_Field_embed_bij_betw)
 
 lemma embed_embedS_iso:
-"embed r r' f = (embedS r r' f \<or> iso r r' f)"
-unfolding embedS_def iso_def by blast
+  "embed r r' f = (embedS r r' f \<or> iso r r' f)"
+  unfolding embedS_def iso_def by blast
 
 lemma not_embedS_iso:
-"\<not> (embedS r r' f \<and> iso r r' f)"
-unfolding embedS_def iso_def by blast
+  "\<not> (embedS r r' f \<and> iso r r' f)"
+  unfolding embedS_def iso_def by blast
 
 lemma embed_embedS_iff_not_iso:
-assumes "embed r r' f"
-shows "embedS r r' f = (\<not> iso r r' f)"
-using assms unfolding embedS_def iso_def by blast
+  assumes "embed r r' f"
+  shows "embedS r r' f = (\<not> iso r r' f)"
+  using assms unfolding embedS_def iso_def by blast
 
 lemma iso_inv_into:
-assumes WELL: "Well_order r" and ISO: "iso r r' f"
-shows "iso r' r (inv_into (Field r) f)"
-using assms unfolding iso_def
-using bij_betw_inv_into inv_into_Field_embed_bij_betw by blast
+  assumes WELL: "Well_order r" and ISO: "iso r r' f"
+  shows "iso r' r (inv_into (Field r) f)"
+  by (meson ISO WELL bij_betw_inv_into inv_into_Field_embed_bij_betw iso_def iso_iff iso_iff2)
 
 lemma embedS_or_iso:
-assumes WELL: "Well_order r" and WELL': "Well_order r'"
-shows "(\<exists>g. embedS r r' g) \<or> (\<exists>h. embedS r' r h) \<or> (\<exists>f. iso r r' f)"
-proof-
-  {fix f assume *: "embed r r' f"
-   {assume "bij_betw f (Field r) (Field r')"
-    hence ?thesis using * by (auto simp add: iso_def)
-   }
-   moreover
-   {assume "\<not> bij_betw f (Field r) (Field r')"
-    hence ?thesis using * by (auto simp add: embedS_def)
-   }
-   ultimately have ?thesis by auto
-  }
-  moreover
-  {fix f assume *: "embed r' r f"
-   {assume "bij_betw f (Field r') (Field r)"
-    hence "iso r' r f" using * by (auto simp add: iso_def)
-    hence "iso r r' (inv_into (Field r') f)"
-    using WELL' by (auto simp add: iso_inv_into)
-    hence ?thesis by blast
-   }
-   moreover
-   {assume "\<not> bij_betw f (Field r') (Field r)"
-    hence ?thesis using * by (auto simp add: embedS_def)
-   }
-   ultimately have ?thesis by auto
-  }
-  ultimately show ?thesis using WELL WELL'
-  wellorders_totally_ordered[of r r'] by blast
-qed
+  assumes WELL: "Well_order r" and WELL': "Well_order r'"
+  shows "(\<exists>g. embedS r r' g) \<or> (\<exists>h. embedS r' r h) \<or> (\<exists>f. iso r r' f)"
+  by (metis WELL WELL' embed_embedS_iso embed_embedS_iso iso_iff4 wellorders_totally_ordered)
 
 end
diff -r 20ab27bc1f3b -r f33df7529fed src/HOL/Cardinals/Wellorder_Relation.thy
--- a/src/HOL/Cardinals/Wellorder_Relation.thy	Fri Jan 13 11:05:48 2023 +0000
+++ b/src/HOL/Cardinals/Wellorder_Relation.thy	Fri Jan 13 16:19:56 2023 +0000
@@ -8,7 +8,7 @@
 section \<open>Well-Order Relations\<close>
 
 theory Wellorder_Relation
-imports Wellfounded_More
+  imports Wellfounded_More
 begin
 
 context wo_rel
@@ -17,29 +17,29 @@
 subsection \<open>Auxiliaries\<close>
 
 lemma PREORD: "Preorder r"
-using WELL order_on_defs[of _ r] by auto
+  using WELL order_on_defs[of _ r] by auto
 
 lemma PARORD: "Partial_order r"
-using WELL order_on_defs[of _ r] by auto
+  using WELL order_on_defs[of _ r] by auto
 
 lemma cases_Total2:
-"\<And> phi a b. \<lbrakk>{a,b} \<le> Field r; ((a,b) \<in> r - Id \<Longrightarrow> phi a b);
+  "\<And> phi a b. \<lbrakk>{a,b} \<le> Field r; ((a,b) \<in> r - Id \<Longrightarrow> phi a b);
               ((b,a) \<in> r - Id \<Longrightarrow> phi a b); (a = b \<Longrightarrow> phi a b)\<rbrakk>
              \<Longrightarrow> phi a b"
-using TOTALS by auto
+  using TOTALS by auto
 
 
 subsection \<open>Well-founded induction and recursion adapted to non-strict well-order relations\<close>
 
 lemma worec_unique_fixpoint:
-assumes ADM: "adm_wo H" and fp: "f = H f"
-shows "f = worec H"
+  assumes ADM: "adm_wo H" and fp: "f = H f"
+  shows "f = worec H"
 proof-
   have "adm_wf (r - Id) H"
-  unfolding adm_wf_def
-  using ADM adm_wo_def[of H] underS_def[of r] by auto
+    unfolding adm_wf_def
+    using ADM adm_wo_def[of H] underS_def[of r] by auto
   hence "f = wfrec (r - Id) H"
-  using fp WF wfrec_unique_fixpoint[of "r - Id" H] by simp
+    using fp WF wfrec_unique_fixpoint[of "r - Id" H] by simp
   thus ?thesis unfolding worec_def .
 qed
 
@@ -47,121 +47,66 @@
 subsubsection \<open>Properties of max2\<close>
 
 lemma max2_iff:
-assumes "a \<in> Field r" and "b \<in> Field r"
-shows "((max2 a b, c) \<in> r) = ((a,c) \<in> r \<and> (b,c) \<in> r)"
+  assumes "a \<in> Field r" and "b \<in> Field r"
+  shows "((max2 a b, c) \<in> r) = ((a,c) \<in> r \<and> (b,c) \<in> r)"
 proof
   assume "(max2 a b, c) \<in> r"
   thus "(a,c) \<in> r \<and> (b,c) \<in> r"
-  using assms max2_greater[of a b] TRANS trans_def[of r] by blast
+    using assms max2_greater[of a b] TRANS trans_def[of r] by blast
 next
   assume "(a,c) \<in> r \<and> (b,c) \<in> r"
   thus "(max2 a b, c) \<in> r"
-  using assms max2_among[of a b] by auto
+    using assms max2_among[of a b] by auto
 qed
 
 
 subsubsection \<open>Properties of minim\<close>
 
 lemma minim_Under:
-"\<lbrakk>B \<le> Field r; B \<noteq> {}\<rbrakk> \<Longrightarrow> minim B \<in> Under B"
-by(auto simp add: Under_def minim_inField minim_least)
+  "\<lbrakk>B \<le> Field r; B \<noteq> {}\<rbrakk> \<Longrightarrow> minim B \<in> Under B"
+  by(auto simp add: Under_def minim_inField minim_least)
 
 lemma equals_minim_Under:
-"\<lbrakk>B \<le> Field r; a \<in> B; a \<in> Under B\<rbrakk>
+  "\<lbrakk>B \<le> Field r; a \<in> B; a \<in> Under B\<rbrakk>
  \<Longrightarrow> a = minim B"
-by(auto simp add: Under_def equals_minim)
+  by(auto simp add: Under_def equals_minim)
 
 lemma minim_iff_In_Under:
-assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
-shows "(a = minim B) = (a \<in> B \<and> a \<in> Under B)"
+  assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
+  shows "(a = minim B) = (a \<in> B \<and> a \<in> Under B)"
 proof
   assume "a = minim B"
   thus "a \<in> B \<and> a \<in> Under B"
-  using assms minim_in minim_Under by simp
+    using assms minim_in minim_Under by simp
 next
   assume "a \<in> B \<and> a \<in> Under B"
   thus "a = minim B"
-  using assms equals_minim_Under by simp
+    using assms equals_minim_Under by simp
 qed
 
 lemma minim_Under_under:
-assumes NE: "A \<noteq> {}" and SUB: "A \<le> Field r"
-shows "Under A = under (minim A)"
+  assumes NE: "A \<noteq> {}" and SUB: "A \<le> Field r"
+  shows "Under A = under (minim A)"
 proof-
-  (* Preliminary facts *)
-  have 1: "minim A \<in> A"
-  using assms minim_in by auto
-  have 2: "\<forall>x \<in> A. (minim A, x) \<in> r"
-  using assms minim_least by auto
-  (* Main proof *)
-  have "Under A \<le> under (minim A)"
-  proof
-    fix x assume "x \<in> Under A"
-    with 1 Under_def[of r] have "(x,minim A) \<in> r" by auto
-    thus "x \<in> under(minim A)" unfolding under_def by simp
-  qed
-  (*  *)
-  moreover
-  (*  *)
-  have "under (minim A) \<le> Under A"
-  proof
-    fix x assume "x \<in> under(minim A)"
-    hence 11: "(x,minim A) \<in> r" unfolding under_def by simp
-    hence "x \<in> Field r" unfolding Field_def by auto
-    moreover
-    {fix a assume "a \<in> A"
-     with 2 have "(minim A, a) \<in> r" by simp
-     with 11 have "(x,a) \<in> r"
-     using TRANS trans_def[of r] by blast
-    }
-    ultimately show "x \<in> Under A" by (unfold Under_def, auto)
-  qed
-  (*  *)
+  have "minim A \<in> A"
+    using assms minim_in by auto
+  then have "Under A \<le> under (minim A)"
+    by (simp add: Under_decr under_Under_singl)
+  moreover have "under (minim A) \<le> Under A"
+    by (meson NE SUB TRANS minim_Under subset_eq under_Under_trans)
   ultimately show ?thesis by blast
 qed
 
 lemma minim_UnderS_underS:
-assumes NE: "A \<noteq> {}" and SUB: "A \<le> Field r"
-shows "UnderS A = underS (minim A)"
+  assumes NE: "A \<noteq> {}" and SUB: "A \<le> Field r"
+  shows "UnderS A = underS (minim A)"
 proof-
-  (* Preliminary facts *)
-  have 1: "minim A \<in> A"
-  using assms minim_in by auto
-  have 2: "\<forall>x \<in> A. (minim A, x) \<in> r"
-  using assms minim_least by auto
-  (* Main proof *)
-  have "UnderS A \<le> underS (minim A)"
-  proof
-    fix x assume "x \<in> UnderS A"
-    with 1 UnderS_def[of r] have "x \<noteq> minim A \<and> (x,minim A) \<in> r" by auto
-    thus "x \<in> underS(minim A)" unfolding underS_def by simp
-  qed
-  (*  *)
-  moreover
-  (*  *)
-  have "underS (minim A) \<le> UnderS A"
-  proof
-    fix x assume "x \<in> underS(minim A)"
-    hence 11: "x \<noteq> minim A \<and> (x,minim A) \<in> r" unfolding underS_def by simp
-    hence "x \<in> Field r" unfolding Field_def by auto
-    moreover
-    {fix a assume "a \<in> A"
-     with 2 have 3: "(minim A, a) \<in> r" by simp
-     with 11 have "(x,a) \<in> r"
-     using TRANS trans_def[of r] by blast
-     moreover
-     have "x \<noteq> a"
-     proof
-       assume "x = a"
-       with 11 3 ANTISYM antisym_def[of r]
-       show False by auto
-     qed
-     ultimately
-     have "x \<noteq> a \<and> (x,a) \<in> r" by simp
-    }
-    ultimately show "x \<in> UnderS A" by (unfold UnderS_def, auto)
-  qed
-  (*  *)
+  have "minim A \<in> A"
+    using assms minim_in by auto
+  then have "UnderS A \<le> underS (minim A)"
+    by (simp add: UnderS_decr underS_UnderS_singl)
+  moreover have "underS (minim A) \<le> UnderS A"
+    by (meson ANTISYM NE SUB TRANS minim_Under subset_eq underS_Under_trans)
   ultimately show ?thesis by blast
 qed
 
@@ -169,150 +114,103 @@
 subsubsection \<open>Properties of supr\<close>
 
 lemma supr_Above:
-assumes SUB: "B \<le> Field r" and ABOVE: "Above B \<noteq> {}"
-shows "supr B \<in> Above B"
-proof(unfold supr_def)
-  have "Above B \<le> Field r"
-  using Above_Field[of r] by auto
-  thus "minim (Above B) \<in> Above B"
-  using assms by (simp add: minim_in)
-qed
+  assumes "Above B \<noteq> {}"
+  shows "supr B \<in> Above B"
+  by (simp add: assms Above_Field minim_in supr_def)
 
 lemma supr_greater:
-assumes SUB: "B \<le> Field r" and ABOVE: "Above B \<noteq> {}" and
-        IN: "b \<in> B"
-shows "(b, supr B) \<in> r"
-proof-
-  from assms supr_Above
-  have "supr B \<in> Above B" by simp
-  with IN Above_def[of r] show ?thesis by simp
-qed
+  assumes "Above B \<noteq> {}" "b \<in> B"
+  shows "(b, supr B) \<in> r"
+  using assms Above_def supr_Above by fastforce
 
 lemma supr_least_Above:
-assumes SUB: "B \<le> Field r" and
-        ABOVE: "a \<in> Above B"
-shows "(supr B, a) \<in> r"
-proof(unfold supr_def)
-  have "Above B \<le> Field r"
-  using Above_Field[of r] by auto
-  thus "(minim (Above B), a) \<in> r"
-  using assms minim_least
-  by simp
-qed
+  assumes "a \<in> Above B"
+  shows "(supr B, a) \<in> r"
+  by (simp add: assms Above_Field minim_least supr_def)
 
 lemma supr_least:
-"\<lbrakk>B \<le> Field r; a \<in> Field r; (\<And> b. b \<in> B \<Longrightarrow> (b,a) \<in> r)\<rbrakk>
+  "\<lbrakk>B \<le> Field r; a \<in> Field r; (\<And> b. b \<in> B \<Longrightarrow> (b,a) \<in> r)\<rbrakk>
  \<Longrightarrow> (supr B, a) \<in> r"
-by(auto simp add: supr_least_Above Above_def)
+  by(auto simp add: supr_least_Above Above_def)
 
 lemma equals_supr_Above:
-assumes SUB: "B \<le> Field r" and ABV: "a \<in> Above B" and
-        MINIM: "\<And> a'. a' \<in> Above B \<Longrightarrow> (a,a') \<in> r"
-shows "a = supr B"
-proof(unfold supr_def)
-  have "Above B \<le> Field r"
-  using Above_Field[of r] by auto
-  thus "a = minim (Above B)"
-  using assms equals_minim by simp
-qed
+  assumes "a \<in> Above B" "\<And> a'. a' \<in> Above B \<Longrightarrow> (a,a') \<in> r"
+  shows "a = supr B"
+  by (simp add: assms Above_Field equals_minim supr_def)
 
 lemma equals_supr:
-assumes SUB: "B \<le> Field r" and IN: "a \<in> Field r" and
-        ABV: "\<And> b. b \<in> B \<Longrightarrow> (b,a) \<in> r" and
-        MINIM: "\<And> a'. \<lbrakk> a' \<in> Field r; \<And> b. b \<in> B \<Longrightarrow> (b,a') \<in> r\<rbrakk> \<Longrightarrow> (a,a') \<in> r"
-shows "a = supr B"
+  assumes SUB: "B \<le> Field r" and IN: "a \<in> Field r" and
+    ABV: "\<And> b. b \<in> B \<Longrightarrow> (b,a) \<in> r" and
+    MINIM: "\<And> a'. \<lbrakk> a' \<in> Field r; \<And> b. b \<in> B \<Longrightarrow> (b,a') \<in> r\<rbrakk> \<Longrightarrow> (a,a') \<in> r"
+  shows "a = supr B"
 proof-
   have "a \<in> Above B"
-  unfolding Above_def using ABV IN by simp
+    unfolding Above_def using ABV IN by simp
   moreover
   have "\<And> a'. a' \<in> Above B \<Longrightarrow> (a,a') \<in> r"
-  unfolding Above_def using MINIM by simp
+    unfolding Above_def using MINIM by simp
   ultimately show ?thesis
-  using equals_supr_Above SUB by auto
+    using equals_supr_Above SUB by auto
 qed
 
 lemma supr_inField:
-assumes "B \<le> Field r" and  "Above B \<noteq> {}"
-shows "supr B \<in> Field r"
-proof-
-  have "supr B \<in> Above B" using supr_Above assms by simp
-  thus ?thesis using assms Above_Field[of r] by auto
-qed
+  assumes "Above B \<noteq> {}"
+  shows "supr B \<in> Field r"
+  by (simp add: Above_Field assms minim_inField supr_def)
 
 lemma supr_above_Above:
-assumes SUB: "B \<le> Field r" and  ABOVE: "Above B \<noteq> {}"
-shows "Above B = above (supr B)"
-proof(unfold Above_def above_def, auto)
-  fix a assume "a \<in> Field r" "\<forall>b \<in> B. (b,a) \<in> r"
-  with supr_least assms
-  show "(supr B, a) \<in> r" by auto
-next
-  fix b assume "(supr B, b) \<in> r"
-  thus "b \<in> Field r"
-  using REFL refl_on_def[of _ r] by auto
-next
-  fix a b
-  assume 1: "(supr B, b) \<in> r" and 2: "a \<in> B"
-  with assms supr_greater
-  have "(a,supr B) \<in> r" by auto
-  thus "(a,b) \<in> r"
-  using 1 TRANS trans_def[of r] by blast
-qed
+  assumes SUB: "B \<le> Field r" and  ABOVE: "Above B \<noteq> {}"
+  shows "Above B = above (supr B)"
+  apply (clarsimp simp: Above_def above_def set_eq_iff)
+  by (meson ABOVE FieldI2 SUB TRANS supr_greater supr_least transD)
 
 lemma supr_under:
-assumes IN: "a \<in> Field r"
-shows "a = supr (under a)"
+  assumes "a \<in> Field r"
+  shows "a = supr (under a)"
 proof-
   have "under a \<le> Field r"
-  using under_Field[of r] by auto
+    using under_Field[of r] by auto
   moreover
   have "under a \<noteq> {}"
-  using IN Refl_under_in[of r] REFL by auto
+    using assms Refl_under_in[of r] REFL by auto
   moreover
   have "a \<in> Above (under a)"
-  using in_Above_under[of _ r] IN by auto
+    using in_Above_under[of _ r] assms by auto
   moreover
   have "\<forall>a' \<in> Above (under a). (a,a') \<in> r"
-  proof(unfold Above_def under_def, auto)
-    fix a'
-    assume "\<forall>aa. (aa, a) \<in> r \<longrightarrow> (aa, a') \<in> r"
-    hence "(a,a) \<in> r \<longrightarrow> (a,a') \<in> r" by blast
-    moreover have "(a,a) \<in> r"
-    using REFL IN by (auto simp add: refl_on_def)
-    ultimately
-    show  "(a, a') \<in> r" by (rule mp)
-  qed
+    by (auto simp: Above_def above_def REFL Refl_under_in assms)
   ultimately show ?thesis
-  using equals_supr_Above by auto
+    using equals_supr_Above by auto
 qed
 
 
 subsubsection \<open>Properties of successor\<close>
 
 lemma suc_least:
-"\<lbrakk>B \<le> Field r; a \<in> Field r; (\<And> b. b \<in> B \<Longrightarrow> a \<noteq> b \<and> (b,a) \<in> r)\<rbrakk>
+  "\<lbrakk>B \<le> Field r; a \<in> Field r; (\<And> b. b \<in> B \<Longrightarrow> a \<noteq> b \<and> (b,a) \<in> r)\<rbrakk>
  \<Longrightarrow> (suc B, a) \<in> r"
-by(auto simp add: suc_least_AboveS AboveS_def)
+  by(auto simp add: suc_least_AboveS AboveS_def)
 
 lemma equals_suc:
-assumes SUB: "B \<le> Field r" and IN: "a \<in> Field r" and
- ABVS: "\<And> b. b \<in> B \<Longrightarrow> a \<noteq> b \<and> (b,a) \<in> r" and
- MINIM: "\<And> a'. \<lbrakk>a' \<in> Field r; \<And> b. b \<in> B \<Longrightarrow> a' \<noteq> b \<and> (b,a') \<in> r\<rbrakk> \<Longrightarrow> (a,a') \<in> r"
-shows "a = suc B"
+  assumes SUB: "B \<le> Field r" and IN: "a \<in> Field r" and
+    ABVS: "\<And> b. b \<in> B \<Longrightarrow> a \<noteq> b \<and> (b,a) \<in> r" and
+    MINIM: "\<And> a'. \<lbrakk>a' \<in> Field r; \<And> b. b \<in> B \<Longrightarrow> a' \<noteq> b \<and> (b,a') \<in> r\<rbrakk> \<Longrightarrow> (a,a') \<in> r"
+  shows "a = suc B"
 proof-
   have "a \<in> AboveS B"
-  unfolding AboveS_def using ABVS IN by simp
+    unfolding AboveS_def using ABVS IN by simp
   moreover
   have "\<And> a'. a' \<in> AboveS B \<Longrightarrow> (a,a') \<in> r"
-  unfolding AboveS_def using MINIM by simp
+    unfolding AboveS_def using MINIM by simp
   ultimately show ?thesis
-  using equals_suc_AboveS SUB by auto
+    using equals_suc_AboveS SUB by auto
 qed
 
 lemma suc_above_AboveS:
-assumes SUB: "B \<le> Field r" and
-        ABOVE: "AboveS B \<noteq> {}"
-shows "AboveS B = above (suc B)"
+  assumes SUB: "B \<le> Field r" and
+    ABOVE: "AboveS B \<noteq> {}"
+  shows "AboveS B = above (suc B)"
+  using assms
 proof(unfold AboveS_def above_def, auto)
   fix a assume "a \<in> Field r" "\<forall>b \<in> B. a \<noteq> b \<and> (b,a) \<in> r"
   with suc_least assms
@@ -320,82 +218,57 @@
 next
   fix b assume "(suc B, b) \<in> r"
   thus "b \<in> Field r"
-  using REFL refl_on_def[of _ r] by auto
+    using REFL refl_on_def[of _ r] by auto
 next
   fix a b
   assume 1: "(suc B, b) \<in> r" and 2: "a \<in> B"
   with assms suc_greater[of B a]
   have "(a,suc B) \<in> r" by auto
   thus "(a,b) \<in> r"
-  using 1 TRANS trans_def[of r] by blast
+    using 1 TRANS trans_def[of r] by blast
 next
   fix a
-  assume 1: "(suc B, a) \<in> r" and 2: "a \<in> B"
-  with assms suc_greater[of B a]
-  have "(a,suc B) \<in> r" by auto
-  moreover have "suc B \<in> Field r"
-  using assms suc_inField by simp
-  ultimately have "a = suc B"
-  using 1 2 SUB ANTISYM antisym_def[of r] by auto
+  assume "(suc B, a) \<in> r" and 2: "a \<in> B"
   thus False
-  using assms suc_greater[of B a] 2 by auto
+    by (metis ABOVE ANTISYM SUB antisymD suc_greater)
 qed
 
 lemma suc_singl_pred:
-assumes IN: "a \<in> Field r" and ABOVE_NE: "aboveS a \<noteq> {}" and
-        REL: "(a',suc {a}) \<in> r" and DIFF: "a' \<noteq> suc {a}"
-shows "a' = a \<or> (a',a) \<in> r"
+  assumes IN: "a \<in> Field r" and ABOVE_NE: "aboveS a \<noteq> {}" and
+    REL: "(a',suc {a}) \<in> r" and DIFF: "a' \<noteq> suc {a}"
+  shows "a' = a \<or> (a',a) \<in> r"
 proof-
   have *: "suc {a} \<in> Field r \<and> a' \<in> Field r"
-  using WELL REL well_order_on_domain by metis
+    using WELL REL well_order_on_domain by metis
   {assume **: "a' \<noteq> a"
-   hence "(a,a') \<in> r \<or> (a',a) \<in> r"
-   using TOTAL IN * by (auto simp add: total_on_def)
-   moreover
-   {assume "(a,a') \<in> r"
-    with ** * assms WELL suc_least[of "{a}" a']
-    have "(suc {a},a') \<in> r" by auto
-    with REL DIFF * ANTISYM antisym_def[of r]
-    have False by simp
-   }
-   ultimately have "(a',a) \<in> r"
-   by blast
+    hence "(a,a') \<in> r \<or> (a',a) \<in> r"
+      using TOTAL IN * by (auto simp add: total_on_def)
+    moreover
+    {assume "(a,a') \<in> r"
+      with ** * assms WELL suc_least[of "{a}" a']
+      have "(suc {a},a') \<in> r" by auto
+      with REL DIFF * ANTISYM antisym_def[of r]
+      have False by simp
+    }
+    ultimately have "(a',a) \<in> r"
+      by blast
   }
   thus ?thesis by blast
 qed
 
 lemma under_underS_suc:
-assumes IN: "a \<in> Field r" and ABV: "aboveS a \<noteq> {}"
-shows "underS (suc {a}) = under a"
-proof-
-  have 1: "AboveS {a} \<noteq> {}"
-  using ABV aboveS_AboveS_singl[of r] by auto
-  have 2: "a \<noteq> suc {a} \<and> (a,suc {a}) \<in> r"
-  using suc_greater[of "{a}" a] IN 1 by auto
-  (*   *)
+  assumes IN: "a \<in> Field r" and ABV: "aboveS a \<noteq> {}"
+  shows "underS (suc {a}) = under a"
+proof -
+  have "AboveS {a} \<noteq> {}"
+    using ABV aboveS_AboveS_singl[of r] by auto
+  then have 2: "a \<noteq> suc {a} \<and> (a,suc {a}) \<in> r"
+    using suc_greater[of "{a}" a] IN  by auto
   have "underS (suc {a}) \<le> under a"
-  proof(unfold underS_def under_def, auto)
-    fix x assume *: "x \<noteq> suc {a}" and **: "(x,suc {a}) \<in> r"
-    with suc_singl_pred[of a x] IN ABV
-    have "x = a \<or> (x,a) \<in> r" by auto
-    with REFL refl_on_def[of _ r] IN
-    show "(x,a) \<in> r" by auto
-  qed
-  (*  *)
+    using ABV IN REFL Refl_under_in underS_E under_def wo_rel.suc_singl_pred wo_rel_axioms by fastforce
   moreover
-  (*   *)
   have "under a \<le> underS (suc {a})"
-  proof(unfold underS_def under_def, auto)
-    assume "(suc {a}, a) \<in> r"
-    with 2 ANTISYM antisym_def[of r]
-    show False by auto
-  next
-    fix x assume *: "(x,a) \<in> r"
-    with 2 TRANS trans_def[of r]
-    show "(x,suc {a}) \<in> r" by blast
-  (*  blast is often better than auto/auto for transitivity-like properties *)
-  qed
-  (*  *)
+    by (simp add: "2" ANTISYM TRANS subsetI underS_I under_underS_trans)
   ultimately show ?thesis by blast
 qed
 
@@ -403,113 +276,49 @@
 subsubsection \<open>Properties of order filters\<close>
 
 lemma ofilter_Under[simp]:
-assumes "A \<le> Field r"
-shows "ofilter(Under A)"
-proof(unfold ofilter_def, auto)
-  fix x assume "x \<in> Under A"
-  thus "x \<in> Field r"
-  using Under_Field[of r] assms by auto
-next
-  fix a x
-  assume "a \<in> Under A" and "x \<in> under a"
-  thus "x \<in> Under A"
-  using TRANS under_Under_trans[of r] by auto
-qed
+  assumes "A \<le> Field r"
+  shows "ofilter(Under A)"
+  by (clarsimp simp: ofilter_def) (meson TRANS Under_Field subset_eq under_Under_trans)
 
 lemma ofilter_UnderS[simp]:
-assumes "A \<le> Field r"
-shows "ofilter(UnderS A)"
-proof(unfold ofilter_def, auto)
-  fix x assume "x \<in> UnderS A"
-  thus "x \<in> Field r"
-  using UnderS_Field[of r] assms by auto
-next
-  fix a x
-  assume "a \<in> UnderS A" and "x \<in> under a"
-  thus "x \<in> UnderS A"
-  using TRANS ANTISYM under_UnderS_trans[of r] by auto
-qed
+  assumes "A \<le> Field r"
+  shows "ofilter(UnderS A)"
+  by (clarsimp simp: ofilter_def) (meson ANTISYM TRANS UnderS_Field subset_eq under_UnderS_trans)
 
 lemma ofilter_Int[simp]: "\<lbrakk>ofilter A; ofilter B\<rbrakk> \<Longrightarrow> ofilter(A Int B)"
-unfolding ofilter_def by blast
+  unfolding ofilter_def by blast
 
 lemma ofilter_Un[simp]: "\<lbrakk>ofilter A; ofilter B\<rbrakk> \<Longrightarrow> ofilter(A \<union> B)"
-unfolding ofilter_def by blast
+  unfolding ofilter_def by blast
 
 lemma ofilter_INTER:
-"\<lbrakk>I \<noteq> {}; \<And> i. i \<in> I \<Longrightarrow> ofilter(A i)\<rbrakk> \<Longrightarrow> ofilter (\<Inter>i \<in> I. A i)"
-unfolding ofilter_def by blast
+  "\<lbrakk>I \<noteq> {}; \<And> i. i \<in> I \<Longrightarrow> ofilter(A i)\<rbrakk> \<Longrightarrow> ofilter (\<Inter>i \<in> I. A i)"
+  unfolding ofilter_def by blast
 
 lemma ofilter_Inter:
-"\<lbrakk>S \<noteq> {}; \<And> A. A \<in> S \<Longrightarrow> ofilter A\<rbrakk> \<Longrightarrow> ofilter (\<Inter>S)"
-unfolding ofilter_def by blast
+  "\<lbrakk>S \<noteq> {}; \<And> A. A \<in> S \<Longrightarrow> ofilter A\<rbrakk> \<Longrightarrow> ofilter (\<Inter>S)"
+  unfolding ofilter_def by blast
 
 lemma ofilter_Union:
-"(\<And> A. A \<in> S \<Longrightarrow> ofilter A) \<Longrightarrow> ofilter (\<Union>S)"
-unfolding ofilter_def by blast
+  "(\<And> A. A \<in> S \<Longrightarrow> ofilter A) \<Longrightarrow> ofilter (\<Union>S)"
+  unfolding ofilter_def by blast
 
 lemma ofilter_under_Union:
-"ofilter A \<Longrightarrow> A = \<Union>{under a| a. a \<in> A}"
-using ofilter_under_UNION [of A] by auto
+  "ofilter A \<Longrightarrow> A = \<Union>{under a| a. a \<in> A}"
+  using ofilter_under_UNION [of A] by auto
 
 
 subsubsection \<open>Other properties\<close>
 
 lemma Trans_Under_regressive:
-assumes NE: "A \<noteq> {}" and SUB: "A \<le> Field r"
-shows "Under(Under A) \<le> Under A"
-proof
-  let ?a = "minim A"
-  (*  Preliminary facts *)
-  have 1: "minim A \<in> Under A"
-  using assms minim_Under by auto
-  have 2: "\<forall>y \<in> A. (minim A, y) \<in> r"
-  using assms minim_least by auto
-  (* Main proof *)
-  fix x assume "x \<in> Under(Under A)"
-  with 1 have 1: "(x,minim A) \<in> r"
-  using Under_def[of r] by auto
-  with Field_def have "x \<in> Field r" by fastforce
-  moreover
-  {fix y assume *: "y \<in> A"
-   hence "(x,y) \<in> r"
-   using 1 2 TRANS trans_def[of r] by blast
-   with Field_def have "(x,y) \<in> r" by auto
-  }
-  ultimately
-  show "x \<in> Under A" unfolding Under_def by auto
-qed
+  assumes NE: "A \<noteq> {}" and SUB: "A \<le> Field r"
+  shows "Under(Under A) \<le> Under A"
+  by (metis INT_E NE REFL Refl_under_Under SUB empty_iff minim_Under minim_Under_under subsetI)
 
 lemma ofilter_suc_Field:
-assumes OF: "ofilter A" and NE: "A \<noteq> Field r"
-shows "ofilter (A \<union> {suc A})"
-proof-
-  (* Preliminary facts *)
-  have 1: "A \<le> Field r" using OF ofilter_def by auto
-  hence 2: "AboveS A \<noteq> {}"
-  using ofilter_AboveS_Field NE OF by blast
-  from 1 2 suc_inField
-  have 3: "suc A \<in> Field r" by auto
-  (* Main proof *)
-  show ?thesis
-  proof(unfold ofilter_def, auto simp add: 1 3)
-    fix a x
-    assume "a \<in> A" "x \<in> under a" "x \<notin> A"
-    with OF ofilter_def have False by auto
-    thus "x = suc A" by simp
-  next
-    fix x assume *: "x \<in> under (suc A)" and **: "x \<notin> A"
-    hence "x \<in> Field r" using under_def Field_def by fastforce
-    with ** have "x \<in> AboveS A"
-    using ofilter_AboveS_Field[of A] OF by auto
-    hence "(suc A,x) \<in> r"
-    using suc_least_AboveS by auto
-    moreover
-    have "(x,suc A) \<in> r" using * under_def[of r] by auto
-    ultimately show "x = suc A"
-    using ANTISYM antisym_def[of r] by auto
-  qed
-qed
+  assumes OF: "ofilter A" and NE: "A \<noteq> Field r"
+  shows "ofilter (A \<union> {suc A})"
+  by (metis NE OF REFL Refl_under_underS ofilter_underS_Field suc_underS under_ofilter)
 
 (* FIXME: needed? *)
 declare
diff -r 20ab27bc1f3b -r f33df7529fed src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Fri Jan 13 11:05:48 2023 +0000
+++ b/src/HOL/Relation.thy	Fri Jan 13 16:19:56 2023 +0000
@@ -1247,6 +1247,9 @@
 definition Field :: "'a rel \<Rightarrow> 'a set"
   where "Field r = Domain r \<union> Range r"
 
+lemma Field_iff: "x \<in> Field r \<longleftrightarrow> (\<exists>y. (x,y) \<in> r \<or> (y,x) \<in> r)"
+  by (auto simp: Field_def)
+
 lemma FieldI1: "(i, j) \<in> R \<Longrightarrow> i \<in> Field R"
   unfolding Field_def by blast