# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1673628240 0
# Node ID ec4c38e156c703c0920b1dc1c145221e9887c6bb
# Parent  f33df7529fede86bec0411829b927163a60de985
Fixed a broken proof

diff -r f33df7529fed -r ec4c38e156c7 src/HOL/Cardinals/Wellorder_Constructions.thy
--- a/src/HOL/Cardinals/Wellorder_Constructions.thy	Fri Jan 13 16:19:56 2023 +0000
+++ b/src/HOL/Cardinals/Wellorder_Constructions.thy	Fri Jan 13 16:44:00 2023 +0000
@@ -357,10 +357,9 @@
 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> {}"
+  assumes "j \<in> underS i" and "i \<in> A" and "A \<subseteq> Field r" and "Above A \<noteq> {}"
   shows "j \<in> underS (supr A)"
-  using supr_greater[OF A AA i]
-  by (metis FieldI1 j max2_equals1 max2_equals2 max2_iff underS_E underS_I)
+  by (meson assms LIN in_mono supr_greater supr_inField underS_incl_iff)
 
 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"