diff -r fba16c509af0 -r e8c96013ea8a src/HOL/BNF_Cardinal_Order_Relation.thy
--- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Wed Mar 05 18:28:57 2025 +0100
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Tue Mar 11 10:20:44 2025 +0100
@@ -1104,7 +1104,16 @@
 
 lemma natLeq_Preorder: "Preorder natLeq"
   unfolding preorder_on_def
-  by (auto simp add: natLeq_Refl natLeq_trans)
+proof (intro conjI)
+  show "natLeq \<subseteq> Field natLeq \<times> Field natLeq"
+    unfolding natLeq_def Field_def by blast
+next
+  show "Refl natLeq"
+    using natLeq_Refl .
+next
+  show "trans natLeq"
+    using natLeq_trans .
+qed
 
 lemma natLeq_antisym: "antisym natLeq"
   unfolding antisym_def natLeq_def by auto